//! Structural properties and no-go theorems.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Properties
//! Paper: Aambø, arXiv:2603.04188, Theorems 3.6–3.8, Corollary 3.9
//!
//! Impossibility theorems proving which axiom combinations are inconsistent,
//! and the uniqueness of PT among idempotent epistemic calculi on total orders.

/// No-go: strongly conservative (E5) + unit as top → trivial.
///
/// If fusion is inflationary (x ≤ x ⊗ y) and unit is top (∀x, x ≤ unit),
/// then every element equals unit, contradicting nontriviality.
// Theorem preserved: no_stronglyConservative_of_unit_top
pub fn no_strongly_conservative_of_unit_top(
    is_strongly_conservative: bool,
    unit_is_top: bool,
) -> bool {
    // Returns false if the combination is inconsistent
    !(is_strongly_conservative && unit_is_top)
}

/// On a total order with idempotent fusion and unit = top,
/// fusion(x, y) = min(x, y).
///
/// This proves PT is the unique such calculus (Theorem 3.8 / Corollary 3.9).
// Theorem preserved: idempotent_is_min
pub fn idempotent_is_min(x: f64, y: f64) -> f64 {
    x.min(y)
}

/// Check that a given fusion function matches min on specific inputs.
pub fn idempotent_is_min_check(fusion: &dyn Fn(f64, f64) -> f64, x: f64, y: f64) -> bool {
    let result = fusion(x, y);
    let expected = x.min(y);
    (result - expected).abs() < 1e-12
}

// Theorem preserved: closed_implies_fallible_of_self_below_ihom
// If ∀x y, x ≤ ihom(ihom(x,y), y), then the calculus is fallible.

// Theorem preserved: closed_iff_fallible_of_quantale
// For complete calculi: closedness ↔ fallibility.

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

    #[test]
    fn no_go_both_true() {
        assert!(!no_strongly_conservative_of_unit_top(true, true));
    }

    #[test]
    fn no_go_one_true() {
        assert!(no_strongly_conservative_of_unit_top(true, false));
        assert!(no_strongly_conservative_of_unit_top(false, true));
    }

    #[test]
    fn no_go_both_false() {
        assert!(no_strongly_conservative_of_unit_top(false, false));
    }

    #[test]
    fn pt_fusion_is_min() {
        let pt_fusion = |x: f64, y: f64| x.min(y);
        assert!(idempotent_is_min_check(&pt_fusion, 0.3, 0.7));
        assert!(idempotent_is_min_check(&pt_fusion, 0.9, 0.1));
        assert!(idempotent_is_min_check(&pt_fusion, 0.5, 0.5));
    }

    #[test]
    fn idempotent_is_min_values() {
        assert!((idempotent_is_min(0.3, 0.7) - 0.3).abs() < 1e-12);
        assert!((idempotent_is_min(0.9, 0.1) - 0.1).abs() < 1e-12);
    }
}