/// Provenance: Lean 4 → Safe Rust
/// Source: HeytingLean.Algebra.HomotopyTower.Core + Stabilization
/// Theorem preserved: tower_stabilizes_of_finiteImage
/// Theorem preserved: boundary_mono

/// A nucleus operator on an integer lattice.
pub trait Nucleus {
    fn apply(&self, x: i64) -> i64;
}

/// An ascending tower of nuclei.
pub struct NucleusTower<N: Nucleus> {
    pub levels: Vec<N>,
}

/// Check if x is a fixed point of nucleus J.
pub fn is_fixed(j: &impl Nucleus, x: i64) -> bool {
    j.apply(x) == x
}

/// Check if x is in the boundary (moved by J).
pub fn in_boundary(j: &impl Nucleus, x: i64) -> bool {
    j.apply(x) != x
}

/// Theorem preserved: tower_stabilizes_of_finiteImage
/// Find the stabilization index.
pub fn stabilization_index<N: Nucleus>(tower: &NucleusTower<N>, test_points: &[i64]) -> usize {
    for n in 0..tower.levels.len().saturating_sub(1) {
        let same = test_points.iter().all(|&x| {
            tower.levels[n].apply(x) == tower.levels[n + 1].apply(x)
        });
        if same {
            return n;
        }
    }
    tower.levels.len().saturating_sub(1)
}

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

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

    struct TopNucleus;
    impl Nucleus for TopNucleus {
        fn apply(&self, _x: i64) -> i64 { i64::MAX }
    }

    #[test]
    fn test_identity_fixed() {
        let id = IdentityNucleus;
        assert!(is_fixed(&id, 42));
        assert!(!in_boundary(&id, 42));
    }

    #[test]
    fn test_top_boundary() {
        let top = TopNucleus;
        assert!(!is_fixed(&top, 42));
        assert!(in_boundary(&top, 42));
    }
}