/// Penumbra: Heyting Gap Non-Zero — Layer 2
/// Provenance: Lean 4 → LambdaIR → MiniC → C → Safe Rust
/// Source: HeytingLean/HossenfelderNoGo/HeytingBoundary/GapNonZero.lean

/// Certificate witnessing a positive gap: R(a) - a > 0
pub struct GapCertificate {
    pub non_boolean_witness: f64,
    pub gap_value: f64,
}

/// Compute the gap for a lattice element under nucleus R.
/// Returns gap > 0 iff element is in the boundary.
pub fn compute_gap(r: impl Fn(f64) -> f64, x: f64) -> f64 {
    r(x) - x
}

/// Verify non-Boolean property: ∃ a, a ∨ ¬a ≠ ⊤
pub fn is_non_boolean(elements: &[bool], join: impl Fn(bool, bool) -> bool,
                      neg: impl Fn(bool) -> bool, top: bool) -> bool {
    elements.iter().any(|&a| join(a, neg(a)) != top)
}

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

    #[test]
    fn ceil_nucleus_has_gap() {
        let gap = compute_gap(|x| x.ceil(), 0.5);
        assert!(gap > 0.0, "Gap should be positive for non-fixed element");
    }

    #[test]
    fn ceil_nucleus_no_gap_at_integer() {
        let gap = compute_gap(|x| x.ceil(), 1.0);
        assert!((gap).abs() < 1e-10, "No gap at fixed point");
    }
}