//! Discrete lattice operations: qRelu nucleus and product witness
//! Source: HeytingLean.NucleusGrafting.DiscreteLattice
//!
//! Theorem preserved: qRelu_extensive
//! Theorem preserved: qRelu_idempotent
//! Theorem preserved: qRelu_meet_preserving
//! Theorem preserved: qRelu_fixed_iff
//! Theorem preserved: productWitness_exists

/// qRelu(z, q) = max(q, z) — the nucleus gate operator
pub fn q_relu(z: i32, q: i32) -> i32 {
    q.max(z)
}

/// Theorem: qRelu_extensive — q <= qRelu(z, q)
pub fn q_relu_extensive(z: i32, q: i32) -> bool {
    q <= q_relu(z, q)
}

/// Theorem: qRelu_idempotent — qRelu(z, qRelu(z, q)) == qRelu(z, q)
pub fn q_relu_idempotent(z: i32, q: i32) -> bool {
    q_relu(z, q_relu(z, q)) == q_relu(z, q)
}

/// Theorem: qRelu_meet_preserving — qRelu(z, min(a,b)) == min(qRelu(z,a), qRelu(z,b))
pub fn q_relu_meet_preserving(z: i32, a: i32, b: i32) -> bool {
    q_relu(z, a.min(b)) == q_relu(z, a).min(q_relu(z, b))
}

/// Theorem: qRelu_fixed_iff — qRelu(z, q) == q iff z <= q
pub fn q_relu_fixed_iff(z: i32, q: i32) -> bool {
    (q_relu(z, q) == q) == (z <= q)
}

/// Product witness: canonical incomparable pair proving non-Booleanity
pub struct ProductWitness {
    pub a: [i32; 2],
    pub b: [i32; 2],
}

pub fn canonical_product_witness() -> ProductWitness {
    ProductWitness {
        a: [0, 1],
        b: [1, 0],
    }
}

/// Exhaustive INT8 nucleus axiom verification
pub struct NucleusAxiomReport {
    pub extensive: bool,
    pub idempotent: bool,
    pub meet_preserving: bool,
    pub all_satisfied: bool,
    pub pair_checks: u32,
    pub fixed_point_count: u32,
    pub fixed_fraction: f64,
    pub heyting_gap: f64,
}

pub fn characterize_int8_nucleus(zero_point: i32) -> NucleusAxiomReport {
    let mut extensive = true;
    let mut idempotent = true;
    let mut meet_preserving = true;
    let mut pair_checks: u32 = 0;
    let mut fixed_point_count: u32 = 0;

    for q in -128i32..128 {
        let rq = q_relu(zero_point, q);
        if q > rq { extensive = false; }
        if q_relu(zero_point, rq) != rq { idempotent = false; }
        if rq == q { fixed_point_count += 1; }
    }

    for a in -128i32..128 {
        for b in -128i32..128 {
            pair_checks += 1;
            let lhs = q_relu(zero_point, a.min(b));
            let rhs = q_relu(zero_point, a).min(q_relu(zero_point, b));
            if lhs != rhs { meet_preserving = false; }
        }
    }

    let fixed_fraction = fixed_point_count as f64 / 256.0;
    NucleusAxiomReport {
        extensive,
        idempotent,
        meet_preserving,
        all_satisfied: extensive && idempotent && meet_preserving,
        pair_checks,
        fixed_point_count,
        fixed_fraction,
        heyting_gap: 1.0 - fixed_fraction,
    }
}

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

    #[test]
    fn test_q_relu_axioms_exhaustive() {
        for z in [-128i32, -1, 0, 1, 42, 127] {
            for q in -128i32..128 {
                assert!(q_relu_extensive(z, q), "extensive failed z={z} q={q}");
                assert!(q_relu_idempotent(z, q), "idempotent failed z={z} q={q}");
                assert!(q_relu_fixed_iff(z, q), "fixed_iff failed z={z} q={q}");
            }
        }
    }

    #[test]
    fn test_meet_preserving_exhaustive() {
        let z = 0;
        for a in -128i32..128 {
            for b in -128i32..128 {
                assert!(q_relu_meet_preserving(z, a, b));
            }
        }
    }

    #[test]
    fn test_characterize_zp0() {
        let r = characterize_int8_nucleus(0);
        assert!(r.all_satisfied);
        assert_eq!(r.pair_checks, 65536);
        assert_eq!(r.fixed_point_count, 128);
        assert!((r.fixed_fraction - 0.5).abs() < 1e-9);
    }

    #[test]
    fn test_product_witness() {
        let w = canonical_product_witness();
        let a_le_b = w.a[0] <= w.b[0] && w.a[1] <= w.b[1];
        let b_le_a = w.b[0] <= w.a[0] && w.b[1] <= w.a[1];
        assert!(!a_le_b && !b_le_a, "pair must be incomparable");
    }
}