/// Penumbra: Nucleus Operator — Core Foundation
/// Provenance: Lean 4 → LambdaIR → MiniC → C → Safe Rust
/// Source: HeytingLean/Core/Nucleus.lean

/// A nucleus on a Heyting algebra: monotone, inflationary, idempotent, meet-preserving.
pub struct Nucleus<F: Fn(f64) -> f64> {
    pub apply: F,
}

impl<F: Fn(f64) -> f64> Nucleus<F> {
    pub fn new(apply: F) -> Self {
        Self { apply }
    }

    /// Theorem preserved: nucleus_le_apply — x ≤ R(x)
    pub fn is_inflationary(&self, x: f64) -> bool {
        x <= (self.apply)(x)
    }

    /// Theorem preserved: nucleus_idempotent — R(R(x)) = R(x)
    pub fn is_idempotent(&self, x: f64, eps: f64) -> bool {
        let rx = (self.apply)(x);
        let rrx = (self.apply)(rx);
        (rrx - rx).abs() < eps
    }

    /// Fixed-point set membership: x ∈ Ω_R iff R(x) = x
    pub fn in_fixed_point_set(&self, x: f64, eps: f64) -> bool {
        let rx = (self.apply)(x);
        (rx - x).abs() < eps
    }

    /// Boundary membership: x ∈ ∂Ω_R iff R(x) ≠ x
    pub fn in_boundary(&self, x: f64, eps: f64) -> bool {
        !self.in_fixed_point_set(x, eps)
    }
}

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

    #[test]
    fn identity_nucleus_all_fixed() {
        let n = Nucleus::new(|x| x);
        for &x in &[0.0, 1.0, -1.0, 42.0] {
            assert!(n.in_fixed_point_set(x, 1e-10));
            assert!(!n.in_boundary(x, 1e-10));
        }
    }

    #[test]
    fn ceil_nucleus_inflationary() {
        let n = Nucleus::new(|x| x.ceil());
        for &x in &[0.5, 1.3, -0.7, 2.9] {
            assert!(n.is_inflationary(x));
        }
    }
}