//! Rank-Nullity Premises — Certified Provability Oracle Templates
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.Discovery.RankNullityPremises
//!
//! Five formally verified theorem templates encoding relationships between
//! boundary-matrix dimensions over GF(2) chain complexes. These templates
//! form the certified provability oracle used by the multi-agent discovery
//! system to validate conjectured formulas.

/// Chain complex dimensions from boundary matrices d1 and d2.
///
/// ```text
/// C₂ --d2--> C₁ --d1--> C₀
///
/// height_d1 = V    width_d1 = E    rank_d1    null_d1 = E - rank_d1
/// height_d2 = E    width_d2 = F    rank_d2    null_d2 = F - rank_d2
/// ```
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct ChainDimensions {
    pub v: i64,         // dim(V0) = vertices
    pub e: i64,         // dim(V1) = edges
    pub f: i64,         // dim(V2) = faces
    pub rank_d1: i64,   // rank of boundary map d1
    pub null_d1: i64,   // nullity of d1 = E - rank_d1
    pub rank_d2: i64,   // rank of boundary map d2
    pub null_d2: i64,   // nullity of d2 = F - rank_d2
}

impl ChainDimensions {
    /// Construct from vertex/edge/face counts and ranks.
    /// Nullities are computed automatically.
    pub fn new(v: i64, e: i64, f: i64, rank_d1: i64, rank_d2: i64) -> Self {
        Self {
            v,
            e,
            f,
            rank_d1,
            null_d1: e - rank_d1,
            rank_d2,
            null_d2: f - rank_d2,
        }
    }

    /// Theorem preserved: rankNullityD1
    /// rank(D1) + null(D1) = dim(V1)
    pub fn rank_nullity_d1(&self) -> bool {
        self.rank_d1 + self.null_d1 == self.e
    }

    /// Theorem preserved: rankNullityD2
    /// rank(D2) + null(D2) = dim(V2)
    pub fn rank_nullity_d2(&self) -> bool {
        self.rank_d2 + self.null_d2 == self.f
    }

    /// Theorem preserved: connectedSurface
    /// rank(D1) = dim(V0) - 1  (b0 = 1)
    pub fn connected_surface(&self) -> bool {
        self.rank_d1 == self.v - 1
    }

    /// Theorem preserved: orientableSurface
    /// null(D2) = 1  (b2 = 1 over GF(2))
    pub fn orientable_surface(&self) -> bool {
        self.null_d2 == 1
    }

    /// Theorem preserved: vanishingMiddleBetti
    /// null(D1) - rank(D2) = 0  (b1 = 0: sphere)
    pub fn vanishing_middle_betti(&self) -> bool {
        self.null_d1 - self.rank_d2 == 0
    }

    /// Theorem preserved: bettiOneValue2
    /// null(D1) - rank(D2) = 2  (b1 = 2: torus/Klein over GF(2))
    pub fn betti_one_value2(&self) -> bool {
        self.null_d1 - self.rank_d2 == 2
    }

    /// Theorem preserved: twoComponents
    /// dim(V0) - rank(D1) = 2  (b0 = 2)
    pub fn two_components(&self) -> bool {
        self.v - self.rank_d1 == 2
    }

    /// Euler characteristic: V - E + F
    pub fn euler_characteristic(&self) -> i64 {
        self.v - self.e + self.f
    }

    /// Betti number b0 = dim(V0) - rank(D1)
    pub fn b0(&self) -> i64 {
        self.v - self.rank_d1
    }

    /// Betti number b1 = null(D1) - rank(D2)
    pub fn b1(&self) -> i64 {
        self.null_d1 - self.rank_d2
    }

    /// Betti number b2 = null(D2)
    pub fn b2(&self) -> i64 {
        self.null_d2
    }
}

/// Theorem preserved: sphereEuler
///
/// Given rank-nullity for D1 and D2, connected (b0=1), orientable (b2=1),
/// vanishing middle Betti (b1=0): V - E + F = 2.
///
/// Lean proof: omega (after unfolding all abbreviations)
pub fn sphere_euler(dims: &ChainDimensions) -> bool {
    dims.rank_nullity_d1()
        && dims.rank_nullity_d2()
        && dims.connected_surface()
        && dims.orientable_surface()
        && dims.vanishing_middle_betti()
        && dims.euler_characteristic() == 2
}

/// Theorem preserved: torusEuler
///
/// Given rank-nullity for D1 and D2, connected, orientable, b1=2:
/// V - E + F = 0.
///
/// Lean proof: omega
pub fn torus_euler(dims: &ChainDimensions) -> bool {
    dims.rank_nullity_d1()
        && dims.rank_nullity_d2()
        && dims.connected_surface()
        && dims.orientable_surface()
        && dims.betti_one_value2()
        && dims.euler_characteristic() == 0
}

/// Theorem preserved: twoComponentB0
///
/// Given dim(V0) - rank(D1) = 2: b0 = 2.
///
/// Lean proof: simpa
pub fn two_component_b0(dims: &ChainDimensions) -> bool {
    dims.two_components() && dims.b0() == 2
}

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

    // Octahedron (sphere): V=6, E=12, F=8, rank_d1=5, rank_d2=7
    fn octahedron() -> ChainDimensions {
        ChainDimensions::new(6, 12, 8, 5, 7)
    }

    // Torus (4x4 grid): V=16, E=48, F=32, rank_d1=15, rank_d2=31
    // b0 = V - rank_d1 = 1, b1 = null_d1 - rank_d2 = 33 - 31 = 2, b2 = null_d2 = 1
    fn torus_4x4() -> ChainDimensions {
        ChainDimensions::new(16, 48, 32, 15, 31)
    }

    // Disjoint union of two octahedra
    fn two_spheres() -> ChainDimensions {
        ChainDimensions::new(12, 24, 16, 10, 14)
    }

    #[test]
    fn test_sphere_betti() {
        let s = octahedron();
        assert_eq!(s.b0(), 1);
        assert_eq!(s.b1(), 0);
        assert_eq!(s.b2(), 1);
        assert_eq!(s.euler_characteristic(), 2);
    }

    #[test]
    fn test_torus_betti() {
        let t = torus_4x4();
        assert_eq!(t.b0(), 1);
        assert_eq!(t.b1(), 2);
        assert_eq!(t.b2(), 1);
        assert_eq!(t.euler_characteristic(), 0);
    }

    #[test]
    fn test_sphere_euler_theorem() {
        assert!(sphere_euler(&octahedron()));
    }

    #[test]
    fn test_torus_euler_theorem() {
        assert!(torus_euler(&torus_4x4()));
    }

    #[test]
    fn test_two_component_theorem() {
        assert!(two_component_b0(&two_spheres()));
    }

    #[test]
    fn test_sphere_not_torus() {
        assert!(!torus_euler(&octahedron()));
    }

    #[test]
    fn test_torus_not_sphere() {
        assert!(!sphere_euler(&torus_4x4()));
    }
}