/// Provenance: Lean 4 → Safe Rust
/// Source: HeytingLean.Algebra.HomotopyTower.PenumbraBridge + SpectralBridge
/// Theorem preserved: stableBoundary_not_boolean_of_bridge
/// Theorem preserved: stableBoundaryGap_nonempty_of_moved
/// Theorem preserved: spectralConverges_of_finiteImage

/// A boundary nucleus: a nucleus viewed through the Hossenfelder gap interface.
pub trait BoundaryNucleus {
    fn apply(&self, x: i64) -> i64;
}

/// Check if the boundary gap at point a is nonempty.
pub fn boundary_gap_nonempty(n: &impl BoundaryNucleus, a: i64) -> bool {
    n.apply(a) != a
}

/// Theorem preserved: stableBoundary_not_boolean_of_bridge
/// If a BooleanBoundaryBridge exists, find a witness that the nucleus is not Boolean.
pub fn stable_boundary_not_boolean(n: &impl BoundaryNucleus, test_points: &[i64]) -> bool {
    test_points.iter().any(|&x| n.apply(x) != x)
}

/// Rank profile of a tower: rank(level(n)) for each n.
pub struct RankProfile {
    pub ranks: Vec<usize>,
}

/// Theorem preserved: spectralConverges_of_finiteImage
/// Find spectral convergence index: first N where rank stabilizes permanently.
pub fn spectral_convergence_index(profile: &RankProfile) -> usize {
    for n in 0..profile.ranks.len().saturating_sub(1) {
        if profile.ranks[n] == profile.ranks[n + 1] {
            let stable = (n + 1..profile.ranks.len().saturating_sub(1))
                .all(|m| profile.ranks[m] == profile.ranks[m + 1]);
            if stable {
                return n;
            }
        }
    }
    profile.ranks.len().saturating_sub(1)
}

#[cfg(test)]
mod tests {
    use super::*;

    struct IdentityBoundary;
    impl BoundaryNucleus for IdentityBoundary {
        fn apply(&self, x: i64) -> i64 { x }
    }

    struct ShiftBoundary;
    impl BoundaryNucleus for ShiftBoundary {
        fn apply(&self, x: i64) -> i64 { x + 1 }
    }

    #[test]
    fn test_identity_is_boolean() {
        let id = IdentityBoundary;
        assert!(!boundary_gap_nonempty(&id, 42));
        assert!(!stable_boundary_not_boolean(&id, &[1, 2, 3]));
    }

    #[test]
    fn test_shift_is_not_boolean() {
        let shift = ShiftBoundary;
        assert!(boundary_gap_nonempty(&shift, 0));
        assert!(stable_boundary_not_boolean(&shift, &[0]));
    }

    #[test]
    fn test_spectral_convergence() {
        let profile = RankProfile { ranks: vec![5, 3, 2, 2, 2] };
        assert_eq!(spectral_convergence_index(&profile), 2);
    }

    #[test]
    fn test_spectral_already_stable() {
        let profile = RankProfile { ranks: vec![4, 4, 4] };
        assert_eq!(spectral_convergence_index(&profile), 0);
    }
}