/// Lean 4 → Safe Rust transpilation
/// Source: HeytingLean.HossenfelderNoGo.HeytingBoundary
/// Provenance: Apoth3osis verified transpilation pipeline

/// Theorem preserved: boundary_necessarily_non_boolean
/// Theorem preserved: gap_nonzero_at_boundary
/// Theorem preserved: eichhorn_nucleus_not_boolean

/// A boundary nucleus on a finite lattice, represented as a closure function.
pub struct BoundaryNucleus {
    /// The closure operator R: maps element indices to element indices.
    pub apply: Box<dyn Fn(usize) -> usize>,
    pub element_count: usize,
}

impl BoundaryNucleus {
    /// isBoolean: R acts as identity on every element.
    pub fn is_boolean(&self) -> bool {
        (0..self.element_count).all(|i| (self.apply)(i) == i)
    }

    /// boundaryGap at element a: nonempty iff R(a) != a.
    pub fn boundary_gap_nonempty(&self, a: usize) -> bool {
        (self.apply)(a) != a
    }

    /// Find any element with nonempty boundary gap.
    pub fn find_gap_witness(&self) -> Option<usize> {
        (0..self.element_count).find(|&a| self.boundary_gap_nonempty(a))
    }
}

/// The Eichhorn benchmark UV-safe projection.
/// Demonstrates non-Booleanity: topYukawa=1 is projected to topYukawa=0.
pub fn eichhorn_uv_safe_projection(top_yukawa: f64) -> f64 {
    // Screening condition: critical topYukawa (-1.0) + yukawaGravityShift (-0.03) = -1.03 <= 0
    // Therefore topYukawa is screened: projected to fixed-point value 0.
    let screening_sum = -1.0 + (-0.03);
    if screening_sum <= 0.0 {
        0.0 // gravitationalFixedPoint.topYukawa = 0
    } else {
        top_yukawa
    }
}

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

    #[test]
    fn test_boolean_nucleus() {
        let identity = BoundaryNucleus {
            apply: Box::new(|x| x),
            element_count: 10,
        };
        assert!(identity.is_boolean());
    }

    #[test]
    fn test_non_boolean_nucleus() {
        // R maps 0 -> 1, everything else identity
        let non_id = BoundaryNucleus {
            apply: Box::new(|x| if x == 0 { 1 } else { x }),
            element_count: 10,
        };
        assert!(!non_id.is_boolean());
        assert!(non_id.boundary_gap_nonempty(0));
        assert!(!non_id.boundary_gap_nonempty(1));
        assert_eq!(non_id.find_gap_witness(), Some(0));
    }

    #[test]
    fn test_eichhorn_screening() {
        // topYukawa=1 should be projected to 0 under screening
        assert!((eichhorn_uv_safe_projection(1.0) - 0.0).abs() < 1e-12);
        // topYukawa=0 is already at fixed point
        assert!((eichhorn_uv_safe_projection(0.0) - 0.0).abs() < 1e-12);
    }
}