logicaffeine-proof 0.10.1

//! Polynomial Calculus / Nullstellensatz over `GF(2)` — the algebraic proof system that **subsumes the
//! linear cuts** (parity is its degree-1 fragment) and, at higher degree, refutes strictly more.
//!
//! A CNF is unsatisfiable iff the constant polynomial `1` lies in the ideal generated by the clause
//! polynomials over the *multilinear* `GF(2)` ring (where `x² = x`, so every monomial is squarefree).
//! At a **fixed degree `d`** this is a finite linear-algebra question — is `1` in the `GF(2)`-span of
//! `{ m · p_C : clause C, monomial m, deg(m·p_C) ≤ d }`? — answered by Gaussian elimination. So degree-`d`
//! Nullstellensatz is polynomial, and the **degree is the power dial**: `d = 1` recovers parity, larger
//! `d` reaches counting-style and beyond. The genuinely hard residue (random) needs degree `Θ(n)`, which
//! is exactly why it stays hard — there is no low-degree algebraic certificate, just as there is no small
//! symmetry quotient. The two are the same wall seen from two sides.
//!
//! Symmetry meets this engine at the monomial basis: an automorphism of the formula permutes monomials,
//! so the Nullstellensatz system has the family's symmetry and its solution can be sought on the orbit
//! quotient of the basis — the algebraic form of "decide on the quotient."

use crate::cdcl::Lit;
use std::collections::{BTreeSet, HashMap, HashSet};

/// A multilinear monomial: the bitmask of the variables it contains (`x² = x` ⟹ squarefree). The `u64`
/// mask carries up to 63 variables; the *clause* engine's explicit cube enumeration stops at 20, the
/// degree-bounded polynomial engine ([`monomials_up_to_degree`]) uses the full range.
pub type Mono = u64;
/// A multilinear polynomial over `GF(2)`: the set of monomials with coefficient 1 (XOR/symmetric-
/// difference semantics).
pub type Poly = BTreeSet<Mono>;

fn toggle(p: &mut Poly, m: Mono) {
    if !p.remove(&m) {
        p.insert(m);
    }
}

pub(crate) fn poly_mul_mono(p: &Poly, m: Mono) -> Poly {
    let mut r = Poly::new();
    for &t in p {
        toggle(&mut r, t | m); // multilinear product: x·x = x ⟹ OR the masks
    }
    r
}

fn poly_mul(a: &Poly, b: &Poly) -> Poly {
    let mut r = Poly::new();
    for &s in a {
        for &t in b {
            toggle(&mut r, s | t);
        }
    }
    r
}

/// The clause polynomial: `1` exactly on the clause's falsifying assignment. The false-indicator of a
/// positive literal `x` is `1 + x` (`{∅, {x}}`), of a negative literal `¬x` is `x` (`{{x}}`); the clause
/// polynomial is their product. Degree = clause width.
pub fn clause_polynomial(clause: &[Lit]) -> Poly {
    let mut p: Poly = [0u64].into_iter().collect(); // the polynomial "1" (the empty monomial)
    for l in clause {
        let bit = 1u64 << l.var();
        let indicator: Poly = if l.is_positive() {
            [0u64, bit].into_iter().collect() // 1 + x
        } else {
            [bit].into_iter().collect() // x
        };
        p = poly_mul(&p, &indicator);
    }
    p
}

/// Is `target` in the `GF(2)`-span of `rows`? Gaussian elimination over packed bit-rows: reduce the rows
/// to an echelon basis (one pivot bit each), then reduce `target` by it and check it vanishes.
fn in_gf2_span(mut rows: Vec<Vec<u64>>, target: &[u64]) -> bool {
    let words = target.len();
    let high_bit = |r: &[u64]| -> Option<usize> {
        for w in (0..words).rev() {
            if r[w] != 0 {
                return Some(w * 64 + (63 - r[w].leading_zeros() as usize));
            }
        }
        None
    };
    let xor_into = |dst: &mut [u64], src: &[u64]| {
        for w in 0..words {
            dst[w] ^= src[w];
        }
    };
    // Build an echelon basis keyed by pivot bit.
    let mut basis: HashMap<usize, Vec<u64>> = HashMap::new();
    for mut r in rows.drain(..) {
        while let Some(p) = high_bit(&r) {
            match basis.get(&p) {
                Some(b) => xor_into(&mut r, b),
                None => break,
            }
        }
        if let Some(p) = high_bit(&r) {
            basis.insert(p, r);
        }
    }
    // Reduce the target.
    let mut t = target.to_vec();
    while let Some(p) = high_bit(&t) {
        match basis.get(&p) {
            Some(b) => xor_into(&mut t, b),
            None => break,
        }
    }
    t.iter().all(|&w| w == 0)
}

/// Does a **degree-`d` Nullstellensatz refutation** exist over `GF(2)`? Sound: such a certificate exists
/// only when the formula is unsatisfiable. Complete at `d = num_vars` (full degree decides any instance).
/// Bounded to `num_vars ≤ 20` (the explicit monomial basis).
pub fn nullstellensatz_refutes(num_vars: usize, clauses: &[Vec<Lit>], degree: usize) -> bool {
    if num_vars > 20 {
        return false;
    }
    // Monomial basis: every squarefree monomial of degree ≤ `degree`.
    let mut index: HashMap<Mono, usize> = HashMap::new();
    for m in 0u64..(1u64 << num_vars) {
        if m.count_ones() as usize <= degree {
            let n = index.len();
            index.insert(m, n);
        }
    }
    let nb = index.len();
    let words = nb.div_ceil(64).max(1);
    let to_bits = |p: &Poly| -> Vec<u64> {
        let mut b = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                b[i / 64] |= 1 << (i % 64);
            }
        }
        b
    };
    let monos: Vec<Mono> = index.keys().copied().collect();

    // Generators: m · p_C for every clause C and monomial m with deg(m · p_C) ≤ degree.
    let mut rows: Vec<Vec<u64>> = Vec::new();
    for c in clauses {
        if c.is_empty() {
            return true; // an empty clause is `1 = 0` outright
        }
        let width = c.len();
        if width > degree {
            continue;
        }
        let pc = clause_polynomial(c);
        for &m in &monos {
            if m.count_ones() as usize <= degree - width {
                rows.push(to_bits(&poly_mul_mono(&pc, m)));
            }
        }
    }
    // Target: the constant polynomial `1` — the empty monomial.
    let mut target = vec![0u64; words];
    let t0 = index[&0u64];
    target[t0 / 64] |= 1 << (t0 % 64);
    in_gf2_span(rows, &target)
}

/// Reduce a polynomial against an echelon basis keyed by leading (largest) monomial: while its leading
/// monomial is a pivot, XOR (symmetric-difference) that basis row in. The leading monomial strictly
/// decreases each step, so this terminates; the result is `p` modulo the span.
fn pc_reduce(basis: &HashMap<Mono, Poly>, mut p: Poly) -> Poly {
    while let Some(&lm) = p.iter().next_back() {
        match basis.get(&lm) {
            Some(b) => {
                for &m in b {
                    toggle(&mut p, m);
                }
            }
            None => break,
        }
    }
    p
}

/// Does a **degree-`d` Polynomial Calculus refutation** exist over `GF(2)`? PC is the *dynamic*
/// strengthening of Nullstellensatz: start from the clause polynomials and close under (i) `GF(2)` linear
/// combination and (ii) multiplication by a single variable, keeping every *derived* polynomial
/// multilinear of degree ≤ `d`; the system is refuted iff the constant `1` is derived. Because an
/// intermediate linear combination can cancel high-degree terms *before* the next multiply, degree-`d` PC
/// certifies a superset of what degree-`d` Nullstellensatz can (which must hit each axiom with a single
/// monomial in one shot). Sound — `1` is derivable only from an unsatisfiable system — and `PC ⊇ NS`, so
/// it never refutes fewer. Complete at `d = num_vars`. Bounded to `num_vars ≤ 20`.
pub fn polynomial_calculus_refutes(num_vars: usize, clauses: &[Vec<Lit>], degree: usize) -> bool {
    if num_vars > 20 {
        return false;
    }
    let poly_deg = |p: &Poly| p.iter().map(|&m| m.count_ones() as usize).max().unwrap_or(0);
    let mut basis: HashMap<Mono, Poly> = HashMap::new();
    let one: Poly = [0u64].into_iter().collect();

    // Seed the worklist with the clause polynomials usable at this degree (width ≤ d).
    let mut worklist: Vec<Poly> = Vec::new();
    for c in clauses {
        if c.is_empty() {
            return true; // an empty clause is `1 = 0` outright
        }
        if c.len() <= degree {
            worklist.push(clause_polynomial(c));
        }
    }
    // Saturate: each newly-independent polynomial joins the basis and is multiplied by every variable
    // (staying within degree), feeding the closure back into the worklist.
    while let Some(p) = worklist.pop() {
        let r = pc_reduce(&basis, p);
        let Some(&lm) = r.iter().next_back() else { continue }; // reduced to 0 — no new information
        for i in 0..num_vars as u64 {
            let q = poly_mul_mono(&r, 1u64 << i);
            if !q.is_empty() && poly_deg(&q) <= degree {
                worklist.push(q);
            }
        }
        basis.insert(lm, r);
        if pc_reduce(&basis, one.clone()).is_empty() {
            return true; // the constant 1 is in the span — refuted
        }
    }
    false
}

/// A **constructive Nullstellensatz certificate** over the multilinear `GF(2)` ring: one coefficient
/// polynomial `g_C` per input clause such that `Σ_C p_C · g_C = 1`, where `p_C = clause_polynomial(C)` is the
/// clause's false-indicator. The identity is a re-checkable proof of UNSAT — evaluate it at any assignment
/// `a`: the right side is `1`, so some `p_C(a) = 1`, i.e. *every* assignment falsifies some clause. Where
/// [`nullstellensatz_refutes`] only *decides* whether such a certificate exists, this one carries the witness.
#[derive(Clone, Debug)]
pub struct NsCertificate {
    num_vars: usize,
    /// `coeffs[i]` is `g_{C_i}` for the `i`-th input clause (parallel indexing to the clause list).
    coeffs: Vec<Poly>,
}

impl NsCertificate {
    /// The variable count the certificate lives over.
    pub fn num_vars(&self) -> usize {
        self.num_vars
    }

    /// The maximum monomial degree among the coefficient polynomials. Multilinear over `num_vars`
    /// variables, so `≤ num_vars` unconditionally — the content is not this (trivial for a multilinear
    /// certificate) but that the certificate *exists and is built by one uniform construction at every `n`*.
    pub fn degree(&self) -> usize {
        self.coeffs.iter().flatten().map(|m| m.count_ones() as usize).max().unwrap_or(0)
    }

    /// **Re-check against the original clauses** (zero trust in the producer): recompute
    /// `Σ_C clause_polynomial(C) · g_C` and confirm it is the constant `1` (the empty monomial). A `true`
    /// verdict is an independent proof that `clauses` is unsatisfiable; it fails closed if the certificate's
    /// clause count does not match the formula it is checked against.
    pub fn verify(&self, clauses: &[Vec<Lit>]) -> bool {
        if self.coeffs.len() != clauses.len() {
            return false;
        }
        let mut sum = Poly::new();
        for (c, g) in clauses.iter().zip(&self.coeffs) {
            if g.is_empty() {
                continue;
            }
            for m in poly_mul(&clause_polynomial(c), g) {
                toggle(&mut sum, m);
            }
        }
        sum.len() == 1 && sum.contains(&0u64)
    }
}

/// The single-point indicator `δ_a` — the multilinear function that is `1` at assignment `a` and `0` at every
/// other corner: `Π_{a_i=1} x_i · Π_{a_i=0} (1 + x_i)`. Its monomials are `ones(a) ∪ T` over every subset `T`
/// of the zero-coordinates (top degree `n`); the `Σ_a δ_a = 1` identity over all corners is the partition of
/// unity the certificate construction rests on.
fn point_indicator(a: u64, num_vars: usize) -> Poly {
    let mask = (1u64 << num_vars).wrapping_sub(1);
    let ones = a & mask;
    let zeros = !a & mask;
    let mut p = Poly::new();
    let mut sub = zeros;
    loop {
        p.insert(ones | sub); // masks are distinct (T ⊆ zeros, disjoint from ones) — no cancellation
        if sub == 0 {
            break;
        }
        sub = (sub - 1) & zeros;
    }
    p
}

/// **The uniform Nullstellensatz completeness construction.** For any CNF over `num_vars ≤ 20` variables,
/// return either a constructive [`NsCertificate`] proving UNSAT, or a satisfying assignment proving SAT — a
/// *total, certifying* decision. The construction is the partition of unity `Σ_a δ_a = 1`: every corner `a`
/// is charged to one clause it falsifies (a corner that falsifies none *is* a model — SAT), and the
/// coefficient of clause `C` is `g_C = Σ_{a charged to C} δ_a`. Then `Σ_C p_C · g_C = Σ_a p_{sel(a)} · δ_a =
/// Σ_a δ_a = 1`, because `p_{sel(a)}(a) = 1` collapses `p·δ_a` to `δ_a` on the cube (multilinear
/// representations are unique). Because this succeeds *identically at every `n`*, it does not merely measure
/// but **proves** that every unsatisfiable formula has a degree-`≤ n` `GF(2)` Nullstellensatz refutation — no
/// minimal-UNSAT family is structureless, at any `n`. This is the census's `max_ns_degree = n` ceiling as a
/// construction, settling `n = 5, 6, …` where the orbit census is infeasible.
pub fn build_ns_certificate(num_vars: usize, clauses: &[Vec<Lit>]) -> Result<NsCertificate, Vec<bool>> {
    assert!(num_vars <= 20, "the explicit-corner construction is bounded to num_vars ≤ 20");
    let mut coeffs: Vec<Poly> = vec![Poly::new(); clauses.len()];
    for a in 0u64..(1u64 << num_vars) {
        let sel = clauses
            .iter()
            .position(|c| !c.iter().any(|l| ((a >> l.var()) & 1 == 1) == l.is_positive()));
        match sel {
            None => return Err((0..num_vars).map(|i| (a >> i) & 1 == 1).collect()),
            Some(ci) => {
                for m in point_indicator(a, num_vars) {
                    toggle(&mut coeffs[ci], m);
                }
            }
        }
    }
    Ok(NsCertificate { num_vars, coeffs })
}

/// The closure of a permutation group under composition (BFS), for small groups. Elements keyed by their
/// image vector so the group is deduplicated.
pub(crate) fn close_perm_group(gens: &[crate::proof::Perm], num_vars: usize) -> Vec<crate::proof::Perm> {
    use crate::proof::Perm;
    let key = |p: &Perm| -> Vec<u32> { (0..num_vars).map(|v| p.apply(Lit::pos(v as u32)).var()).collect() };
    let id = Perm::identity(num_vars);
    let mut seen: std::collections::BTreeSet<Vec<u32>> = [key(&id)].into_iter().collect();
    let mut group = vec![id.clone()];
    let mut frontier = vec![id];
    while let Some(p) = frontier.pop() {
        for g in gens {
            let q = p.compose(g);
            if seen.insert(key(&q)) {
                group.push(q.clone());
                frontier.push(q);
            }
        }
    }
    group
}

/// The **symmetrization** of a `GF(2)` functional `L` (given as the monomials where it is `1`) over a group:
/// `Σ_{g∈G} g·L` (mod 2). The Reynolds/averaging operator of characteristic 0 — but *without the `1/|G|`*,
/// because that division is unavailable over `GF(2)`.
fn symmetrize(l: &[Mono], group: &[crate::proof::Perm]) -> BTreeSet<Mono> {
    let mut sym: BTreeSet<Mono> = BTreeSet::new();
    for &m in l {
        for g in group {
            let img = apply_perm_to_mono(g, m);
            if !sym.remove(&img) {
                sym.insert(img);
            }
        }
    }
    sym
}

/// Exact binomial coefficient `C(n, k)` in `u128` (small `n`; the running-product form stays integral).
fn binom(n: usize, k: usize) -> u128 {
    if k > n {
        return 0;
    }
    let k = k.min(n - k);
    let mut c = 1u128;
    for i in 0..k {
        c = c * (n - i) as u128 / (i + 1) as u128;
    }
    c
}

/// The width of the degree-`d` Nullstellensatz system over `n` variables: the count of multilinear monomials
/// of degree `≤ d`, `Σ_{k≤d} C(n,k)`. At `d = n` this is exactly `2ⁿ` — so the degree-`n` certificate that
/// [`build_ns_certificate`] always produces (completeness: no unsatisfiable formula over `n` variables is
/// "structureless") lives in an **exponentially large** space. The certificate's *existence* is an
/// information-theoretic fact about the finite cube; it is not an efficient algorithm, and it says nothing
/// about P vs NP — which is a statement about the asymptotic growth of a *family* of instances, not any fixed
/// finite `n` (a fixed finite problem is decidable by table lookup, vacuously).
pub fn nullstellensatz_basis_size(n: usize, d: usize) -> u128 {
    (0..=d.min(n)).map(|k| binom(n, k)).sum()
}

/// All squarefree monomials of degree `≤ degree` over `num_vars ≤ 63` variables, ascending as `u64`s —
/// enumerated directly (Gosper's next-`k`-subset walk per degree class), never touching the `2ⁿ` cube.
/// This is the basis walk that lifts fixed-degree Nullstellensatz work past the clause engine's
/// 20-variable cap: the count is `Σ_{k≤d} C(n,k)` ([`nullstellensatz_basis_size`]), not `2ⁿ`.
pub fn monomials_up_to_degree(num_vars: usize, degree: usize) -> Vec<Mono> {
    assert!(num_vars <= 63, "the u64 monomial mask carries ≤ 63 variables");
    let mut out: Vec<Mono> = vec![0];
    for k in 1..=degree.min(num_vars) {
        let limit: Mono = 1u64 << num_vars;
        let mut m: Mono = (1u64 << k) - 1; // the least k-subset
        while m < limit {
            out.push(m);
            let c = m & m.wrapping_neg(); // Gosper's hack: next integer with the same popcount
            let r = m + c;
            m = (((r ^ m) >> 2) / c) | r;
        }
    }
    out.sort_unstable();
    out
}

/// The degree of a multilinear `GF(2)` polynomial: its largest monomial's popcount (`0` for the zero
/// polynomial and for the constant `1`).
pub fn poly_degree(p: &Poly) -> usize {
    p.iter().map(|&m| m.count_ones() as usize).max().unwrap_or(0)
}

/// Does a **degree-`d` Nullstellensatz refutation** exist over `GF(2)` for an arbitrary polynomial
/// generator system — is `1` in the `GF(2)`-span of `{ m·g : deg(m·g) ≤ d }`? The clause engine's
/// question asked of *any* generators, not just clause polynomials: the substrate for the linear
/// encoding ([`exactly_one_linear_generators`]) and the symmetric-family machinery. The multiplier rule
/// is exact — a product is admitted by its degree *after* multilinear collapse. (For clause polynomials
/// this span equals the clause engine's: a multiplier overlapping a positive literal kills the product,
/// one overlapping a negative literal absorbs into a smaller multiplier — pinned by the differential
/// test.) Degree-bounded enumeration, so it scales to `num_vars ≤ 63`.
pub fn ns_refutes_polys(num_vars: usize, gens: &[Poly], degree: usize) -> bool {
    let basis = monomials_up_to_degree(num_vars, degree);
    let index: HashMap<Mono, usize> = basis.iter().enumerate().map(|(i, &m)| (m, i)).collect();
    let words = basis.len().div_ceil(64).max(1);
    let to_bits = |p: &Poly| -> Vec<u64> {
        let mut b = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                b[i / 64] |= 1 << (i % 64);
            }
        }
        b
    };
    let mut rows: Vec<Vec<u64>> = Vec::new();
    for g in gens {
        if g.is_empty() {
            continue; // the zero polynomial generates nothing
        }
        for &m in &basis {
            let prod = poly_mul_mono(g, m);
            if !prod.is_empty() && poly_degree(&prod) <= degree {
                rows.push(to_bits(&prod));
            }
        }
    }
    let t0 = index[&0u64];
    let mut target = vec![0u64; words];
    target[t0 / 64] |= 1 << (t0 % 64);
    in_gf2_span(rows, &target)
}

/// [`ns_lower_bound_witness`] for an arbitrary polynomial generator system: a degree-`d`
/// pseudo-expectation `L` with `L(1) = 1` and `L(m·g) = 0` for every admitted generator, returned as the
/// monomials where `L = 1`. `Some(L)` certifies `NS-degree > d` for the system (re-checkable by
/// [`check_ns_lower_bound_polys`], zero trust in the solver); `None` means a degree-`d` refutation
/// exists. Degree-bounded enumeration — `num_vars ≤ 63`.
pub fn ns_lower_bound_witness_polys(num_vars: usize, gens: &[Poly], degree: usize) -> Option<Vec<Mono>> {
    let basis = monomials_up_to_degree(num_vars, degree);
    let index: HashMap<Mono, usize> = basis.iter().enumerate().map(|(i, &m)| (m, i)).collect();
    let nb = basis.len();
    let words = nb.div_ceil(64).max(1);
    let mask_of = |p: &Poly| -> Vec<u64> {
        let mut mask = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                mask[i / 64] |= 1u64 << (i % 64);
            }
        }
        mask
    };
    let mut eqs: Vec<(Vec<u64>, bool)> = Vec::new();
    for g in gens {
        if g.is_empty() {
            continue;
        }
        for &m in &basis {
            let prod = poly_mul_mono(g, m);
            if !prod.is_empty() && poly_degree(&prod) <= degree {
                eqs.push((mask_of(&prod), false)); // ⟨L, m·g⟩ = 0
            }
        }
    }
    let t0 = index[&0u64];
    let mut target = vec![0u64; words];
    target[t0 / 64] |= 1u64 << (t0 % 64);
    eqs.push((target, true)); // L(1) = 1
    let l = gf2_solve(&eqs, nb)?;
    Some((0..nb).filter(|&i| (l[i / 64] >> (i % 64)) & 1 == 1).map(|i| basis[i]).collect())
}

/// [`ns_lower_bound_witness_polys`] restricted to a **sub-basis**: the functional `L` is sought only on
/// monomials passing `in_basis` (`L = 0` elsewhere), while the constraints `⟨L, m·g⟩ = 0` still range
/// over *all* admitted generators — so any `Some` is a fully valid,
/// [`check_ns_lower_bound_polys`]-verifiable witness, and `None` means only "no witness on this
/// sub-basis". The structure probe: which candidate supports carry a family's lower bound (for
/// pigeonhole this is how the hole-injective support was found and the classical partial-matching
/// support was ruled out over `GF(2)`). Degree-bounded enumeration — `num_vars ≤ 63`.
pub fn ns_lower_bound_witness_polys_on_basis(
    num_vars: usize,
    gens: &[Poly],
    degree: usize,
    in_basis: &dyn Fn(Mono) -> bool,
) -> Option<Vec<Mono>> {
    let all = monomials_up_to_degree(num_vars, degree);
    let basis: Vec<Mono> = all.iter().copied().filter(|&m| in_basis(m)).collect();
    let index: HashMap<Mono, usize> = basis.iter().enumerate().map(|(i, &m)| (m, i)).collect();
    index.get(&0u64)?; // the empty monomial must be in the sub-basis for L(1) = 1
    let nb = basis.len();
    let words = nb.div_ceil(64).max(1);
    let mask_of = |p: &Poly| -> Vec<u64> {
        let mut mask = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                mask[i / 64] |= 1u64 << (i % 64);
            }
        }
        mask
    };
    let mut eqs: Vec<(Vec<u64>, bool)> = Vec::new();
    for g in gens {
        if g.is_empty() {
            continue;
        }
        for &m in &all {
            let prod = poly_mul_mono(g, m);
            if !prod.is_empty() && poly_degree(&prod) <= degree {
                eqs.push((mask_of(&prod), false));
            }
        }
    }
    let t0 = index[&0u64];
    let mut target = vec![0u64; words];
    target[t0 / 64] |= 1u64 << (t0 % 64);
    eqs.push((target, true));
    let l = gf2_solve(&eqs, nb)?;
    Some((0..nb).filter(|&i| (l[i / 64] >> (i % 64)) & 1 == 1).map(|i| basis[i]).collect())
}

/// Re-check a [`ns_lower_bound_witness_polys`] certificate (zero trust in the producer): `L(1) = 1` and
/// `L(m·g) = 0` for every admitted generator of the system. `true` ⟹ the generator system genuinely has
/// no degree-`d` `GF(2)` Nullstellensatz refutation. Degree-bounded enumeration — `num_vars ≤ 63`.
pub fn check_ns_lower_bound_polys(num_vars: usize, gens: &[Poly], degree: usize, witness: &[Mono]) -> bool {
    let l: BTreeSet<Mono> = witness.iter().copied().collect();
    if !l.contains(&0u64) {
        return false; // L(1) must be 1
    }
    let basis = monomials_up_to_degree(num_vars, degree);
    for g in gens {
        if g.is_empty() {
            continue;
        }
        for &m in &basis {
            let prod = poly_mul_mono(g, m);
            if !prod.is_empty()
                && poly_degree(&prod) <= degree
                && prod.iter().filter(|t| l.contains(t)).count() % 2 == 1
            {
                return false; // ⟨L, m·g⟩ must be 0
            }
        }
    }
    true
}

/// The **linear encoding** of exactly-one constraints: for each group `G` the degree-1 generator
/// `1 + Σ_{v∈G} x_v` (the `GF(2)` form of `Σ x = 1`) plus the pairwise products `x_u·x_v` over each
/// group, deduplicated. This is the encoding under which the modular-counting and pigeonhole degree
/// lower bounds are stated in the literature — the wide at-least-one clause is recovered from it modulo
/// the pairs (the interreduction test pins the identity, and the clause→linear direction is
/// degree-preserving, so bounds against this encoding are the stronger statements). The linear
/// generators come first (one per group, in group order), then the pairs.
pub fn exactly_one_linear_generators(groups: &[Vec<u32>]) -> Vec<Poly> {
    let mut gens: Vec<Poly> = Vec::new();
    for g in groups {
        let mut lin: Poly = [0u64].into_iter().collect();
        for &v in g {
            assert!(v < 63, "the u64 monomial mask carries ≤ 63 variables");
            toggle(&mut lin, 1u64 << v);
        }
        gens.push(lin);
    }
    let mut pairs: BTreeSet<Mono> = BTreeSet::new();
    for g in groups {
        for (i, &u) in g.iter().enumerate() {
            for &v in &g[i + 1..] {
                pairs.insert((1u64 << u) | (1u64 << v));
            }
        }
    }
    gens.extend(pairs.into_iter().map(|m| [m].into_iter().collect::<Poly>()));
    gens
}

/// Solve a `GF(2)` linear system `⟨x, coeffᵢ⟩ = rhsᵢ` (each `coeff` a multi-word bit-vector over `nvars`
/// variables) by Gaussian elimination to reduced row echelon form. Returns any solution `x` (bit-packed into
/// `⌈nvars/64⌉` words) or `None` if the system is inconsistent. Multi-word, so it scales past 63 variables.
pub(crate) fn gf2_solve(equations: &[(Vec<u64>, bool)], nvars: usize) -> Option<Vec<u64>> {
    let words = nvars.div_ceil(64).max(1);
    let bit = |v: &[u64], i: usize| (v[i / 64] >> (i % 64)) & 1 == 1;
    let mut rows: Vec<(Vec<u64>, bool)> = equations.to_vec();
    let mut pivots: Vec<usize> = Vec::new();
    let mut r = 0usize;
    for col in 0..nvars {
        let Some(sel) = (r..rows.len()).find(|&i| bit(&rows[i].0, col)) else {
            continue;
        };
        rows.swap(r, sel);
        let (pmask, prhs) = (rows[r].0.clone(), rows[r].1);
        for i in 0..rows.len() {
            if i != r && bit(&rows[i].0, col) {
                for w in 0..words {
                    rows[i].0[w] ^= pmask[w];
                }
                rows[i].1 ^= prhs;
            }
        }
        pivots.push(col);
        r += 1;
    }
    if rows.iter().any(|(m, b)| *b && m.iter().all(|&w| w == 0)) {
        return None; // 0 = 1 — inconsistent
    }
    // RREF: each pivot row's only set bits are its pivot column plus free columns; free vars = 0 ⟹ x_col = rhs.
    let mut x = vec![0u64; words];
    for (i, &col) in pivots.iter().enumerate() {
        if rows[i].1 {
            x[col / 64] |= 1u64 << (col % 64);
        }
    }
    Some(x)
}

/// **A re-checkable degree-`d` Nullstellensatz LOWER-bound certificate.** Where [`nullstellensatz_refutes`]
/// *decides* whether a degree-`d` refutation exists, this witnesses its NON-existence: a `GF(2)` linear
/// functional `L` on the degree-`≤ d` monomials (a *degree-`d` pseudo-expectation`) with `L(1) = 1` and
/// `L(m · p_C) = 0` for every generator. Such an `L` exists iff `1` is **not** in the `GF(2)`-span of the
/// generators, i.e. iff there is no degree-`d` refutation — so `Some(L)` certifies the lower bound
/// `NS-degree(F) > d`, independently re-checkable by [`check_ns_lower_bound`] (no trust in the solver). The
/// certificate is returned as the list of monomials on which `L` is `1`. `None` means a degree-`d` refutation
/// exists (no lower bound at `d`). Multi-word linear algebra, so the monomial basis is not size-capped —
/// only `num_vars ≤ 20` for the explicit basis enumeration.
pub fn ns_lower_bound_witness(num_vars: usize, clauses: &[Vec<Lit>], degree: usize) -> Option<Vec<u64>> {
    if num_vars > 20 {
        return None;
    }
    let mut index: HashMap<Mono, usize> = HashMap::new();
    let mut monos: Vec<Mono> = Vec::new();
    for m in 0u64..(1u64 << num_vars) {
        if m.count_ones() as usize <= degree {
            index.insert(m, monos.len());
            monos.push(m);
        }
    }
    let nb = monos.len();
    let words = nb.div_ceil(64).max(1);
    let mask_of = |p: &Poly| -> Vec<u64> {
        let mut mask = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                mask[i / 64] |= 1u64 << (i % 64);
            }
        }
        mask
    };
    let mut eqs: Vec<(Vec<u64>, bool)> = Vec::new();
    for c in clauses {
        let width = c.len();
        if width == 0 {
            return None; // an empty clause is an immediate refutation — no lower bound
        }
        if width > degree {
            continue;
        }
        let pc = clause_polynomial(c);
        for &m in &monos {
            if m.count_ones() as usize <= degree - width {
                eqs.push((mask_of(&poly_mul_mono(&pc, m)), false)); // ⟨L, m·p_C⟩ = 0
            }
        }
    }
    let t0 = index[&0u64];
    let mut target = vec![0u64; words];
    target[t0 / 64] |= 1u64 << (t0 % 64);
    eqs.push((target, true)); // L(1) = 1
    let l = gf2_solve(&eqs, nb)?;
    Some((0..nb).filter(|&i| (l[i / 64] >> (i % 64)) & 1 == 1).map(|i| monos[i]).collect())
}

/// [`ns_lower_bound_witness`] restricted to a **sub-basis** of monomials: the functional `L` is sought only
/// on monomials `m` with `in_basis(m)` (and `L = 0` elsewhere), while the constraints `⟨L, m·p_C⟩ = 0` still
/// range over *all* generators. `Some(L)` is a fully valid, `check_ns_lower_bound`-verifiable witness (the
/// restriction only limits the *search*, not the check); `None` here means "no witness on this sub-basis" —
/// which, unlike the full-basis version, does **not** imply a refutation exists. This exposes the *structure*
/// of a lower bound: e.g. for pigeonhole, the partial-matching sub-basis already carries the certificate.
pub fn ns_lower_bound_witness_on_basis(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    degree: usize,
    in_basis: &dyn Fn(Mono) -> bool,
) -> Option<Vec<u64>> {
    if num_vars > 20 {
        return None;
    }
    let mut index: HashMap<Mono, usize> = HashMap::new();
    let mut basis: Vec<Mono> = Vec::new();
    for m in 0u64..(1u64 << num_vars) {
        if m.count_ones() as usize <= degree && in_basis(m) {
            index.insert(m, basis.len());
            basis.push(m);
        }
    }
    index.get(&0u64)?; // the empty monomial must be in the basis for L(1) = 1
    let nb = basis.len();
    let words = nb.div_ceil(64).max(1);
    let mask_of = |p: &Poly| -> Vec<u64> {
        let mut mask = vec![0u64; words];
        for &m in p {
            if let Some(&i) = index.get(&m) {
                mask[i / 64] |= 1u64 << (i % 64);
            }
        }
        mask
    };
    let mults: Vec<Mono> =
        (0u64..(1u64 << num_vars)).filter(|m| m.count_ones() as usize <= degree).collect();
    let mut eqs: Vec<(Vec<u64>, bool)> = Vec::new();
    for c in clauses {
        let width = c.len();
        if width == 0 {
            return None;
        }
        if width > degree {
            continue;
        }
        let pc = clause_polynomial(c);
        for &m in &mults {
            if m.count_ones() as usize <= degree - width {
                eqs.push((mask_of(&poly_mul_mono(&pc, m)), false));
            }
        }
    }
    let t0 = index[&0u64];
    let mut target = vec![0u64; words];
    target[t0 / 64] |= 1u64 << (t0 % 64);
    eqs.push((target, true));
    let l = gf2_solve(&eqs, nb)?;
    Some((0..nb).filter(|&i| (l[i / 64] >> (i % 64)) & 1 == 1).map(|i| basis[i]).collect())
}

/// Is a `PHP` monomial a **partial matching** — an injective partial pigeon→hole map? PHP's variable
/// `x_{p,h}` sits at index `p·holes + h` ([`crate::families::php`]), so a monomial (a set of variables) is a
/// partial matching iff no two of its variables share a pigeon or a hole. This is the support of the
/// Razborov degree lower bound's pseudo-expectation.
pub fn php_is_partial_matching(mono: Mono, holes: usize) -> bool {
    let (mut pigeons, mut used_holes) = (0u64, 0u64);
    let mut bits = mono;
    while bits != 0 {
        let v = bits.trailing_zeros() as usize;
        let (p, h) = (v / holes, v % holes);
        if (pigeons >> p) & 1 == 1 || (used_holes >> h) & 1 == 1 {
            return false;
        }
        pigeons |= 1u64 << p;
        used_holes |= 1u64 << h;
        bits &= bits - 1;
    }
    true
}

/// Is a `PHP` monomial **hole-injective** — no two of its edges share a hole? Standard PHP forbids two
/// pigeons in one hole but allows a pigeon in several holes, so the at-most-one clauses force the `GF(2)`
/// pseudo-expectation to vanish exactly on hole-*collision* monomials — i.e. its support lies in the
/// hole-injective monomials (partial functions hole→pigeon). This is looser than a partial matching (which
/// also forbids pigeon repeats) and is the correct `GF(2)` support.
pub fn php_is_hole_injective(mono: Mono, holes: usize) -> bool {
    let mut used_holes = 0u64;
    let mut bits = mono;
    while bits != 0 {
        let h = (bits.trailing_zeros() as usize) % holes;
        if (used_holes >> h) & 1 == 1 {
            return false;
        }
        used_holes |= 1u64 << h;
        bits &= bits - 1;
    }
    true
}

/// Re-check a [`ns_lower_bound_witness`] certificate (zero trust in the producer): the functional `L` (given
/// as the monomials on which it is `1`) must satisfy `L(1) = 1` and `L(m · p_C) = 0` for every degree-`≤ d`
/// generator. `true` ⟹ `F` genuinely has no degree-`d` `GF(2)` Nullstellensatz refutation.
pub fn check_ns_lower_bound(num_vars: usize, clauses: &[Vec<Lit>], degree: usize, witness: &[u64]) -> bool {
    let l: BTreeSet<Mono> = witness.iter().copied().collect();
    let pairs = |p: &Poly| -> bool { p.iter().filter(|m| l.contains(m)).count() % 2 == 1 }; // ⟨L, p⟩
    if !l.contains(&0u64) {
        return false; // L(1) must be 1
    }
    for c in clauses {
        let width = c.len();
        if width == 0 {
            return false;
        }
        if width > degree {
            continue;
        }
        let pc = clause_polynomial(c);
        for m in 0u64..(1u64 << num_vars) {
            if m.count_ones() as usize <= degree.saturating_sub(width) {
                if pairs(&poly_mul_mono(&pc, m)) {
                    return false; // ⟨L, m·p_C⟩ must be 0
                }
            }
        }
    }
    true
}

/// The **atom** of the partition-of-unity recurrence on variable `v`: `(1 + x_v) + x_v`, which reduces to
/// the constant `1` in the multilinear `GF(2)` ring (`x_v + x_v = 0`). This single identity is the engine of
/// the whole `n = ∞` ratchet: it is *independent of `n`*, so a product of `n` copies of it is `1` at every
/// scale.
pub fn pou_atom(v: usize) -> Poly {
    let x: Poly = [1u64 << v].into_iter().collect();
    let one_plus_x: Poly = [0u64, 1u64 << v].into_iter().collect();
    let mut atom = one_plus_x;
    for m in x {
        toggle(&mut atom, m);
    }
    atom
}

/// The **partition of unity** over the `n`-cube: `Σ_{a ∈ {0,1}ⁿ} δ_a`, the sum of every corner's
/// point-indicator. It is the constant `1` for all `n` — the identity the constructive Nullstellensatz
/// certificate ([`build_ns_certificate`]) rests on. Computed here by direct summation (for finite checks);
/// [`pou_as_product`] gives the closed form that proves it `∀n`.
pub fn partition_of_unity(n: usize) -> Poly {
    let mut sum = Poly::new();
    for a in 0..(1u64 << n) {
        for m in point_indicator(a, n) {
            toggle(&mut sum, m);
        }
    }
    sum
}

/// The **closed form** of the partition of unity: the product `Π_{v<n} ((1+x_v) + x_v)` of the per-coordinate
/// atoms. By distributivity `Σ_a Π_i f_{i,a_i} = Π_i (f_{i,0} + f_{i,1})`, this equals
/// [`partition_of_unity`] — a *sum of `2ⁿ` products* rewritten as a *product of `n` sums*. Since every atom
/// is `1` ([`pou_atom`]), the product is `1` for **every** `n`. This is the ratchet to `n = ∞`: not `2ⁿ`
/// terms checked one cube at a time, but `n` identical unit factors.
pub fn pou_as_product(n: usize) -> Poly {
    let mut product: Poly = [0u64].into_iter().collect(); // the polynomial 1
    for v in 0..n {
        product = poly_mul(&product, &pou_atom(v));
    }
    product
}

/// Apply a formula automorphism to a monomial: a monomial is a *set of variables*, so the permutation
/// part of `σ` relabels them (phase flips do not act on monomials). The bridge from the symmetry group
/// to the polynomial basis.
pub(crate) fn apply_perm_to_mono(perm: &crate::proof::Perm, m: Mono) -> Mono {
    let mut out = 0u64;
    for v in 0..perm.num_vars() {
        if m & (1 << v) != 0 {
            out |= 1 << perm.apply(Lit::pos(v as u32)).var();
        }
    }
    out
}

/// **Symmetry-break Polynomial Calculus at the basis.** Partition the degree-≤`degree` monomials into
/// orbits under the formula's automorphisms. The orbit count is the width of the *symmetry-reduced*
/// Nullstellensatz system — a symmetric certificate is constant on each orbit, so the Gaussian runs over
/// the quotient instead of all `C(n,d)` monomials. The same collapse that made the field cuts O(1),
/// inherited by the algebraic engine. (Bounded to `num_vars ≤ 20`.)
pub fn monomial_orbits(num_vars: usize, degree: usize, generators: &[crate::proof::Perm]) -> Vec<Vec<Mono>> {
    let basis: BTreeSet<Mono> =
        (0u64..(1u64 << num_vars)).filter(|m| m.count_ones() as usize <= degree).collect();
    let mut seen: BTreeSet<Mono> = BTreeSet::new();
    let mut orbits = Vec::new();
    for &m in &basis {
        if seen.contains(&m) {
            continue;
        }
        let mut orbit = BTreeSet::new();
        orbit.insert(m);
        let mut stack = vec![m];
        while let Some(x) = stack.pop() {
            for g in generators {
                let y = apply_perm_to_mono(g, x);
                if basis.contains(&y) && orbit.insert(y) {
                    stack.push(y);
                }
            }
        }
        for &x in &orbit {
            seen.insert(x);
        }
        orbits.push(orbit.into_iter().collect());
    }
    orbits
}

/// The generators of the full symmetric group `Sₙ` on `n` variables: the adjacent transpositions
/// `(i, i+1)`. `Sₙ` is the symmetry of a *fully-symmetric* formula (every variable interchangeable), and
/// under it the monomial basis collapses to one orbit per degree — the sharpest instance of
/// [`monomial_orbits`]' compression.
pub fn symmetric_group_generators(n: usize) -> Vec<crate::proof::Perm> {
    (0..n.saturating_sub(1))
        .map(|i| {
            let images: Vec<Lit> = (0..n)
                .map(|v| {
                    if v == i {
                        Lit::pos((i + 1) as u32)
                    } else if v == i + 1 {
                        Lit::pos(i as u32)
                    } else {
                        Lit::pos(v as u32)
                    }
                })
                .collect();
            crate::proof::Perm::from_images(images)
        })
        .collect()
}

/// **Symmetry-reduced Nullstellensatz** — the algebraic refutation collapsed by the formula's symmetry.
/// Full degree-`d` NS asks whether `1` lies in the `GF(2)`-span of the generators `m·p_C`, a Gaussian over
/// up to `C(n,≤d)` monomial columns. When the formula has a symmetry group `G`, summing each generator's
/// `G`-orbit gives an *invariant* generator, and every invariant polynomial is constant on the monomial
/// orbits ([`monomial_orbits`]) — so the same span check runs over just `#orbits` columns and
/// `#generator-orbits` rows. For a symmetric family that is the difference between `2^Θ(n)` and `O(1)`.
///
/// **Sound**: each row is an honest `GF(2)`-sum of NS generators, so `1` in the reduced span is `1` in the
/// full span — a real refutation, hence UNSAT. Incomplete (a refutation need not be `G`-invariant), and
/// fail-closed: if a passed generator is not a genuine symmetry (an orbit step leaves the generator set)
/// it declines rather than reduce unsoundly. `generators` must be automorphisms of `clauses`.
pub fn nullstellensatz_refutes_symmetric(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    degree: usize,
    generators: &[crate::proof::Perm],
) -> bool {
    if num_vars > 20 {
        return false;
    }
    // Monomial orbits give the reduced column basis; an invariant polynomial is all-or-nothing per orbit.
    let mono_orbits = monomial_orbits(num_vars, degree, generators);
    let n_orbits = mono_orbits.len();
    let words = n_orbits.div_ceil(64).max(1);
    let orbit_index: HashMap<Mono, usize> = (0u64..(1u64 << num_vars))
        .filter(|m| m.count_ones() as usize <= degree)
        .map(|m| (m, mono_orbits.iter().position(|o| o.contains(&m)).unwrap()))
        .collect();
    let to_orbit_bits = |p: &Poly| -> Vec<u64> {
        let mut b = vec![0u64; words];
        for (oi, orbit) in mono_orbits.iter().enumerate() {
            if p.contains(&orbit[0]) {
                b[oi / 64] |= 1 << (oi % 64);
            }
        }
        b
    };
    let apply_sigma = |sigma: &crate::proof::Perm, p: &Poly| -> Poly {
        let mut out = Poly::new();
        for &m in p {
            toggle(&mut out, apply_perm_to_mono(sigma, m));
        }
        out
    };
    let canon = |p: &Poly| -> Vec<Mono> { p.iter().copied().collect() };

    // The NS generators m·p_C with deg(m·p_C) ≤ degree.
    let monos: Vec<Mono> = orbit_index.keys().copied().collect();
    let mut gens: Vec<Poly> = Vec::new();
    for c in clauses {
        if c.is_empty() {
            return true; // an empty clause is `1 = 0`
        }
        let width = c.len();
        if width > degree {
            continue;
        }
        let pc = clause_polynomial(c);
        for &m in &monos {
            if m.count_ones() as usize <= degree - width {
                gens.push(poly_mul_mono(&pc, m));
            }
        }
    }
    let gen_set: HashSet<Vec<Mono>> = gens.iter().map(|p| canon(p)).collect();

    // Sum each generator-orbit into an invariant generator; express it in the orbit basis.
    let mut seen: HashSet<Vec<Mono>> = HashSet::new();
    let mut rows: Vec<Vec<u64>> = Vec::new();
    for g in &gens {
        if seen.contains(&canon(g)) {
            continue;
        }
        let mut orbit_sum = Poly::new();
        let mut local: HashSet<Vec<Mono>> = HashSet::from([canon(g)]);
        let mut stack = vec![g.clone()];
        while let Some(x) = stack.pop() {
            seen.insert(canon(&x));
            for &m in &x {
                toggle(&mut orbit_sum, m);
            }
            for sigma in generators {
                let y = apply_sigma(sigma, &x);
                let yk = canon(&y);
                if !gen_set.contains(&yk) {
                    return false; // not a genuine symmetry of the NS system — fail closed
                }
                if local.insert(yk) {
                    stack.push(y);
                }
            }
        }
        rows.push(to_orbit_bits(&orbit_sum));
    }

    // Target: the constant `1` (the empty monomial, its own orbit).
    let mut target = vec![0u64; words];
    if let Some(&oi) = orbit_index.get(&0u64) {
        target[oi / 64] |= 1 << (oi % 64);
    }
    in_gf2_span(rows, &target)
}

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

    fn sat(num_vars: usize, clauses: &[Vec<Lit>]) -> bool {
        (0u64..(1u64 << num_vars)).any(|x| {
            clauses.iter().all(|c| c.iter().any(|l| ((x >> l.var()) & 1 != 0) == l.is_positive()))
        })
    }

    /// **The constructive completeness certificate carries a re-checkable witness.** `nullstellensatz_refutes`
    /// only *decides* that a degree-`n` certificate exists; [`build_ns_certificate`] *produces* it — the
    /// explicit `g_C` with `Σ_C p_C·g_C = 1` — and it re-checks against the original clauses. The construction
    /// rests on the partition of unity `Σ_a δ_a = 1`; a SAT formula yields a re-checked model, never a false
    /// refutation; and the certificate fails closed against a clause set it was not built for.
    #[test]
    fn ns_certificate_is_a_constructive_completeness_proof() {
        // Partition of unity `Σ_a δ_a = 1` — the identity the whole construction rests on.
        let mut unity = Poly::new();
        for a in 0u64..8 {
            for m in point_indicator(a, 3) {
                toggle(&mut unity, m);
            }
        }
        assert!(unity.len() == 1 && unity.contains(&0u64), "Σ_a δ_a must be the constant 1");

        // A transitive-XOR contradiction: x0=x1, x1=x2, x0≠x2 — UNSAT with no two clauses in direct conflict.
        let p = |v: u32| Lit::pos(v);
        let q = |v: u32| Lit::neg(v);
        let core = vec![
            vec![q(0), p(1)], vec![p(0), q(1)],
            vec![q(1), p(2)], vec![p(1), q(2)],
            vec![p(0), p(2)], vec![q(0), q(2)],
        ];
        let cert = build_ns_certificate(3, &core).expect("the UNSAT core has a constructive certificate");
        assert!(cert.verify(&core), "the constructive certificate re-checks against the original clauses");
        assert!(cert.degree() <= cert.num_vars(), "the certificate degree is ≤ n by construction");
        // Fail-closed: the certificate must not verify against a clause set it was not built for.
        assert!(!cert.verify(&core[..core.len() - 1]), "a certificate must not verify a different clause set");

        // SAT ⇒ a re-checked satisfying assignment, never a spurious refutation.
        let satisfiable = vec![vec![p(0), p(1)], vec![q(0), p(2)]];
        match build_ns_certificate(3, &satisfiable) {
            Err(model) => assert!(
                satisfiable.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
                "the returned SAT witness must satisfy every clause"
            ),
            Ok(_) => panic!("a satisfiable formula must not yield a refutation certificate"),
        }
    }

    /// **The pattern that ratchets to `n = ∞` (discrete-math induction).** The partition of unity — the
    /// identity `Σ_a δ_a = 1` behind constructive Nullstellensatz completeness — is not checked cube-by-cube
    /// (that dies at `2ⁿ`). It FACTORS: `Σ_a Π_i f_{i,a_i} = Π_i ((1+x_i) + x_i)`, a product of `n`
    /// per-coordinate atoms, each equal to the constant `1`. Base `PoU(0) = 1`; step `PoU(n+1) = PoU(n)·atom
    /// = PoU(n)·1 = PoU(n)`. The step is `n`-INDEPENDENT (one fixed identity `(1+x)+x = 1`), so induction
    /// closes it for ALL `n`. Here: the atom is `1`, the base holds, the recurrence holds, and `PoU(n)`
    /// equals both the direct sum and the product — the finite checks that pin the `∀n` factorization.
    #[test]
    fn partition_of_unity_is_one_for_all_n_by_the_atom_factorization() {
        let one: Poly = [0u64].into_iter().collect();
        // The atom is the constant 1 — the n-independent engine of the ratchet.
        for v in 0..8 {
            assert_eq!(pou_atom(v), one, "the atom (1+x{v})+x{v} reduces to 1");
        }
        // Base case: the 0-cube's partition of unity is 1.
        assert_eq!(partition_of_unity(0), one, "PoU(0) = 1 (base case)");
        for n in 0..=12 {
            // The factorization (distributivity): the 2ⁿ-term sum equals the n-factor product.
            assert_eq!(partition_of_unity(n), pou_as_product(n), "PoU(n) = Π atoms (sum-of-products = product-of-sums)");
            // And the product of n ones is one — the conclusion, at every n.
            assert_eq!(partition_of_unity(n), one, "PoU(n) = 1");
        }
        // The inductive STEP, explicit: PoU(n+1) = PoU(n) · atom_n (the recurrence the induction climbs).
        for n in 0..12 {
            assert_eq!(
                partition_of_unity(n + 1),
                poly_mul(&partition_of_unity(n), &pou_atom(n)),
                "PoU(n+1) = PoU(n)·atom — the n-uniform inductive step"
            );
        }
    }

    /// **A parametric family with machine-checked degree growth.** The all-corners cube `F_n` (every one of
    /// the `2ⁿ` assignments forbidden by a full-width clause) has minimum `GF(2)` Nullstellensatz degree
    /// *exactly* `n` — certified at each `n` by a re-checkable dual witness that no degree-`(n-1)` refutation
    /// exists, plus a degree-`n` refutation that does. That is machine-checked, re-verifiable **linear degree
    /// growth**. Honest caveat: this particular bound is *width-driven* — a width-`n` family admits no
    /// generator below degree `n` — so it is a clean but "easy" lower bound. A *bounded-width* family with
    /// super-constant degree is the deeper object; PHP(3) is measured as an honest data point.
    #[test]
    /// **The genuine Ω(n) degree lower bound: pigeonhole is NS-hard, and its degree GROWS.** PHP(m) (m
    /// pigeons, m−1 holes) has clause width `≤ m−1` but its `GF(2)` Nullstellensatz degree is `2(m−1) =
    /// Θ(√vars)` — the classical pigeonhole degree bound. We certify the EXACT degree for m = 3 (degree 4) and
    /// m = 4 (degree 6): a re-checkable dual witness that there is no degree-`(2m−3)` refutation, and a
    /// refutation at `2(m−1)`. The certified degree strictly *exceeds the clause width* (so it is not the
    /// trivial width bound) and strictly *grows* with `m` — a genuine, non-width, parametric degree lower
    /// bound with certified growth. (The uniform `∀m` proof that it is exactly `2(m−1)` is the classical
    /// Razborov-style theorem; here it is certified per-`m` with re-checkable witnesses.)
    #[test]
    fn pigeonhole_has_certified_growing_non_width_ns_degree() {
        let measured = [(3usize, 4usize), (4, 6)]; // (pigeons, exact GF(2) NS degree)
        let mut degrees = Vec::new();
        for (m, deg) in measured {
            let (php, _) = crate::families::php(m);
            // Re-checkable dual witness: no degree-(deg−1) refutation ⟹ NS-degree > deg−1.
            let w = ns_lower_bound_witness(php.num_vars, &php.clauses, deg - 1)
                .unwrap_or_else(|| panic!("PHP({m}): a degree-{} lower-bound witness must exist", deg - 1));
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, deg - 1, &w), "PHP({m}): NS-degree > {} re-checks", deg - 1);
            // Refuted at `deg` ⟹ NS-degree(PHP(m)) = deg exactly.
            assert!(nullstellensatz_refutes(php.num_vars, &php.clauses, deg), "PHP({m}): a degree-{deg} refutation exists");
            assert!(!nullstellensatz_refutes(php.num_vars, &php.clauses, deg - 1), "PHP({m}): NS-degree = {deg} exactly");
            // Genuine (non-width): the degree exceeds the max clause width `m−1`.
            assert!(deg > m - 1, "PHP({m}): NS-degree {deg} > max clause width {} — not a width bound", m - 1);
            degrees.push(deg);
        }
        // Certified GROWTH: the NS degree strictly climbs with the family size (Θ(√vars)).
        assert!(degrees.windows(2).all(|w| w[1] > w[0]), "the certified NS degree grows with n: {degrees:?}");
    }

    /// **The symmetric NS width is CONSTANT in `m` at each fixed degree.** An orbit-type of a degree-`≤d` PHP
    /// monomial under `Sₘ × Sₘ₋₁` is the isomorphism type of its bipartite pigeon/hole graph; there are only
    /// finitely many such types with `≤ d` edges, and every one is realizable once `m ≥ d+1`. So for each fixed
    /// `d` the orbit-type count is **independent of `m`** — the symmetric Nullstellensatz basis at degree `d` is
    /// `O(1)`-wide at every scale. (The *witness* of §5.3 has degree `2m−3` that grows with `m`, so its own
    /// orbit count grows as `Σ_{k≤m−1} p(k)`; this is the complementary fixed-degree statement.) We verify the
    /// count stabilizes across `m` for `d = 1, 2, 3`.
    #[test]
    fn php_symmetric_ns_width_is_constant_in_m_at_fixed_degree() {
        // `monomial_orbits` enumerates the 2^vars monomial cube, so keep PHP small (m ≤ 5 ⟹ ≤ 20 vars). The
        // orbit-type count stabilizes once m ≥ d+1 (enough pigeons/holes to realize every ≤d-edge graph type).
        for (d, ms) in [(1usize, vec![2, 3, 4, 5]), (2, vec![3, 4, 5]), (3, vec![4, 5])] {
            let counts: Vec<usize> = ms
                .iter()
                .map(|&m| {
                    let (php, _) = crate::families::php(m);
                    monomial_orbits(php.num_vars, d, &crate::hypercube::php_perm_symmetries(m)).len()
                })
                .collect();
            eprintln!("degree {d}: symmetric-NS orbit-type counts across m = {counts:?}");
            assert!(counts.windows(2).all(|w| w[0] == w[1]), "degree {d}: orbit-type count constant in m: {counts:?}");
        }
    }

    /// **The uniform lower bound is FORCED BY SYMMETRY.** The witness `L = [hole-injective]` is invariant
    /// under PHP's automorphism group (permute pigeons × permute holes) — it is the *symmetric*
    /// pseudo-expectation. So the whole degree lower bound is a symmetry fact: the invariant witness collapses
    /// the exponential monomial basis to a handful of orbit-types (symmetry = compression = the certificate).
    /// We verify invariance and report the orbit compression.
    #[test]
    fn the_uniform_php_witness_is_the_symmetric_pseudo_expectation() {
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let d = 2 * holes - 1;
            let l: BTreeSet<Mono> = (0u64..(1u64 << php.num_vars))
                .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                .collect();
            let gens = crate::hypercube::php_perm_symmetries(m);
            // Invariance: every pigeon/hole permutation maps the witness onto itself.
            for g in &gens {
                for &mo in &l {
                    assert!(l.contains(&apply_perm_to_mono(g, mo)), "PHP({m}): the uniform witness is symmetry-invariant");
                }
            }
            // Compression: the witness (|L| monomials) is a union of few symmetry orbit-types.
            let orbits = monomial_orbits(php.num_vars, d, &gens);
            let witness_orbits = orbits.iter().filter(|o| l.contains(&o[0])).count();
            eprintln!(
                "PHP({m}): symmetric witness = {} monomials → {} orbit-types (of {} total), compression ×{:.1}",
                l.len(), witness_orbits, orbits.len(), l.len() as f64 / witness_orbits as f64
            );
            assert!(witness_orbits < l.len(), "PHP({m}): symmetry compresses the witness to fewer orbit-types");
        }
    }

    /// **A UNIFORM `∀m` degree lower bound, via a closed-form parity-aware witness.** The explicit functional
    /// `L(M) = [M is hole-injective]` (1 on every hole-injective monomial, 0 elsewhere) is a valid
    /// degree-`(2m−3)` `GF(2)` pseudo-expectation for PHP(m) — proving `NS-degree(PHP(m)) ≥ 2(m−1)` for **all
    /// m**, by a single argument, not a per-`m` Gaussian search:
    ///   - the at-most-one clauses vanish because their generators are hole collisions (`L = 0`);
    ///   - each pigeon clause gives `⟨L, m·p_C⟩ = Σ_{S⊆U} 1 = 2^{|U|} ≡ 0 (mod 2)`, and the multiplier `m` has
    ///     degree `≤ (2m−3) − (m−1) = m−2 < holes`, so it misses ≥1 hole (`|U| ≥ 1`) — the parity that holds
    ///     over `GF(2)` and **fails** over characteristic 0.
    /// Here the *explicit* `L` is re-checked at `m = 3, 4` (the argument gives every `m`). This is a genuine,
    /// uniform proof-complexity lower bound — a hardness result (the P ≠ NP direction), not an algorithm.
    #[test]
    fn uniform_parity_aware_witness_proves_php_degree_bound_for_all_m() {
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let d = 2 * holes - 1; // 2m − 3
            let l: Vec<u64> = (0u64..(1u64 << php.num_vars))
                .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                .collect();
            assert!(
                check_ns_lower_bound(php.num_vars, &php.clauses, d, &l),
                "PHP({m}): the hole-injective indicator is a valid degree-{d} pseudo-expectation ⟹ NS-degree ≥ {}",
                2 * holes
            );
            // Tight: it matches the measured exact degree 2(m−1).
            assert!(nullstellensatz_refutes(php.num_vars, &php.clauses, 2 * holes), "PHP({m}): refuted at 2(m−1)");
        }
    }

    /// **THE BRIDGE: the symmetric certificate's *depth* equals the NS degree, exactly, `∀m`.** The naive
    /// guess — that the affine-symmetry *group* grows with hardness — is false and the tools prove it: PHP is
    /// affine-shear-*rigid* (no shears at any depth), and parity carries only a constant depth-2 shear. So the
    /// symmetry that governs degree is not read off the group's *width* but off the *depth of the invariant
    /// certificate it supports*. Define the **symmetric depth** of a family as the greatest degree `d` at which
    /// its symmetry-invariant pseudo-expectation is still valid (the deepest the symmetric compression reaches
    /// before a refutation forces it to zero). For PHP(m) that certificate is the hole-injective indicator
    /// (§5.3), invariant under `Sₘ × Sₘ₋₁`, and its symmetric depth is `2m−3`, while the NS degree is `2m−2` —
    /// so **`NS-degree(PHP(m)) = symmetric-depth(PHP(m)) + 1` for every `m`**. The `+1` is exactly the
    /// witness↔refutation duality unit: a degree-`d` pseudo-expectation certifies "no degree-`d` refutation," so
    /// the deepest surviving symmetric certificate sits precisely one below the refutation degree. This is the
    /// honest form of "depth tracks NS degree" — not a loose correlation but an exact identity, certified at
    /// `m = 3, 4` here and proven for all `m` by the uniform parity-aware witness. Symmetry-depth and
    /// proof-degree are one number, read twice.
    #[test]
    fn the_symmetric_certificate_depth_is_exactly_one_below_ns_degree() {
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let nv = php.num_vars;

            // NS degree = least d with a degree-d refutation (scan up).
            let ns_degree = (1..=nv)
                .find(|&d| nullstellensatz_refutes(nv, &php.clauses, d))
                .expect("PHP is UNSAT so some refutation degree exists");

            // Symmetric depth = greatest d at which the invariant (hole-injective) pseudo-expectation is valid.
            let symmetric_depth = (0..=nv)
                .rev()
                .find(|&d| {
                    let w: Vec<u64> = (0u64..(1u64 << nv))
                        .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                        .collect();
                    check_ns_lower_bound(nv, &php.clauses, d, &w)
                })
                .expect("the invariant witness is valid at some degree");

            // The exact bridge, both sides computed independently.
            assert_eq!(ns_degree, 2 * (m - 1), "PHP({m}): NS degree is 2(m−1)");
            assert_eq!(symmetric_depth, 2 * m - 3, "PHP({m}): symmetric certificate depth is 2m−3");
            assert_eq!(
                ns_degree,
                symmetric_depth + 1,
                "PHP({m}): NS-degree = symmetric-depth + 1 — the witness↔refutation duality unit"
            );
            eprintln!("PHP({m}): symmetric-depth={symmetric_depth}, NS-degree={ns_degree} = depth+1 ✓");
        }
    }

    /// **The symmetric-group arity grades the certificate depth (`∀m`).** The dichotomy (§4) says PHP's
    /// hardness is protected by *permutation* symmetry — the group `Sₘ × Sₘ₋₁`, of arity `m` (the pigeon
    /// count). This is the tracking that the dichotomy predicts *should* exist on the permutation side, and it
    /// does, exactly: the depth of the symmetry-invariant certificate (the hole-injective indicator, §5.3) is
    /// `2m − 3`, an exact strictly-increasing linear function of the arity — **each unit of arity buys exactly
    /// two units of certificate depth**. Not a correlation; a closed form, certified at `m = 3, 4` and proven
    /// for all `m` by the uniform witness. This is the graded law the failed shear/symplectic chases were
    /// groping for — on the correct axis (arity), not the wrong one (linear-symmetry weight, structurally
    /// pinned at 2 by the weight-2 generation of the classical groups).
    #[test]
    fn the_symmetric_group_arity_grades_the_certificate_depth() {
        let mut points = Vec::new();
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let nv = php.num_vars;
            let cert_depth = (0..=nv)
                .rev()
                .find(|&d| {
                    let w: Vec<u64> = (0u64..(1u64 << nv))
                        .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                        .collect();
                    check_ns_lower_bound(nv, &php.clauses, d, &w)
                })
                .expect("the invariant witness is valid at some degree");
            assert_eq!(cert_depth, 2 * m - 3, "arity {m}: certificate depth = 2·arity − 3");
            points.push((m, cert_depth));
        }
        let (m0, d0) = points[0];
        let (m1, d1) = points[1];
        assert_eq!(
            (d1 - d0) / (m1 - m0),
            2,
            "each unit of symmetric-group arity buys exactly two units of certificate depth"
        );
        for (m, d) in points {
            eprintln!("arity m={m} → certificate depth {d} = 2m−3");
        }
    }

    /// **THE CAPSTONE — one group-theoretic number grades a machine-certified lower bound across three proof
    /// systems.** For `PHP_m`, a single quantity, the *arity* `m` of the protecting symmetric group `Sₘ ×
    /// Sₘ₋₁` (order `m!·(m−1)!`), drives — through certified chains, no trust — three independent
    /// proof-complexity coordinates, each computed from a *different* proof system and each strictly increasing
    /// with `m`:
    ///   arity `m`  →  symmetric-certificate depth `2m−3`  →  Nullstellensatz degree `2m−2`  →  resolution
    ///   width `m−1` (lower bound re-checked by a closed set).
    /// This is the thesis "symmetry = compression = complexity" made an *exact, executable, cross-system law*:
    /// the amount of symmetry (arity) determines the amount of hardness (degree, width), end to end, in the
    /// kernel's own currency of re-checkable certificates. By Ben-Sasson–Wigderson the growing width forces
    /// super-polynomial resolution *size* — the classical exponential lower bound this chain terminates in.
    ///
    /// **What this is not** — the honest boundary, stated in the theorem itself. This lives entirely in the
    /// *structured / symmetric* regime. As `work/PROOF_SKETCH.md` records: *"a fast algorithm for structured or
    /// symmetric instances says nothing; NP-hardness lives in the worst case."* The chain measures how a
    /// symmetry number places a *symmetric family* between the two kernel poles (trivial structure at degree 1;
    /// completeness at degree `n`); it says nothing about worst-case instances and is **not** a step toward P
    /// vs NP. The ultimate here is an exact law of the measurement science, not a resolution of the open
    /// problem — and it is stronger for being honest about which it is.
    #[test]
    fn the_ultimate_symmetry_to_hardness_chain_is_certified() {
        use crate::res_width::{
            check_res_width_lower_bound, min_res_width_clauses, resolution_width_closure, WidthConvention,
        };
        let mut chain = Vec::new();
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let nv = php.num_vars;
            let group_order = (1..=m as u128).product::<u128>() * (1..=holes as u128).product::<u128>();

            // (1) symmetric-certificate depth
            let cert_depth = (0..=nv)
                .rev()
                .find(|&d| {
                    let w: Vec<u64> = (0u64..(1u64 << nv))
                        .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                        .collect();
                    check_ns_lower_bound(nv, &php.clauses, d, &w)
                })
                .unwrap();
            // (2) Nullstellensatz degree
            let ns_degree = (1..=nv).find(|&d| nullstellensatz_refutes(nv, &php.clauses, d)).unwrap();
            // (3) resolution width, with a re-checked lower-bound certificate (zero trust)
            let res_width = min_res_width_clauses(nv, &php.clauses, WidthConvention::WideAxioms).unwrap();
            let closed = resolution_width_closure(&php.clauses, res_width - 1, WidthConvention::WideAxioms);
            assert!(
                check_res_width_lower_bound(&php.clauses, res_width - 1, WidthConvention::WideAxioms, &closed),
                "PHP({m}): certified resolution width > {}",
                res_width - 1
            );

            // Each coordinate is the arity, transformed by a certified chain.
            assert_eq!(cert_depth, 2 * m - 3, "arity {m}: certificate depth = 2m−3");
            assert_eq!(ns_degree, 2 * m - 2, "arity {m}: NS degree = 2m−2");
            assert_eq!(ns_degree, cert_depth + 1, "the witness↔refutation duality unit");
            assert_eq!(res_width, m - 1, "arity {m}: resolution width = m−1");
            chain.push((m, group_order, cert_depth, ns_degree, res_width));
        }

        // One symmetry number, three proof systems, all graded strictly by the arity.
        let (a, b) = (chain[0], chain[1]);
        assert!(b.0 > a.0, "arity increases");
        assert!(b.2 > a.2, "certificate depth grows with arity");
        assert!(b.3 > a.3, "NS degree grows with arity");
        assert!(b.4 > a.4, "resolution width grows with arity");
        for (m, order, d, g, w) in chain {
            eprintln!(
                "arity m={m} (|Sₘ×Sₘ₋₁|={order}): cert-depth={d}=2m−3  NS-degree={g}=2m−2  res-width={w}=m−1 — all certified, all graded by m"
            );
        }
    }

    /// **The dichotomy the exploration forced into the open, as asserted facts.** Over `GF(2)` a formula's
    /// symmetry is one of two *types*, and the type predicts the complexity regime: PHP carries growing NS
    /// degree yet is affine-shear-**rigid** (no shear automorphism at any depth up to the variable count — its
    /// hardness is permutation-protected), whereas a single parity block carries a nontrivial affine shear at
    /// constant depth 2 and no NS degree at all (it is satisfiable — Gaussian-trivial). Affine-shear symmetry
    /// and high NS degree are mutually exclusive here: the symmetry *type* is the complexity *type*. This is
    /// why "shear depth tracks degree" is the wrong bridge and [`the_symmetric_certificate_depth_is_exactly_one_below_ns_degree`]
    /// is the right one.
    #[test]
    fn affine_shear_symmetry_and_high_ns_degree_are_mutually_exclusive() {
        use crate::census::affine_composite_shear_generators;
        // PHP: growing NS degree, but rigid under affine shears at every depth.
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let nv = php.num_vars;
            for depth in 1..=nv.min(5) {
                let shears = affine_composite_shear_generators(nv, &php.clauses, depth);
                assert!(
                    shears.iter().all(|(s, _)| s.len() != depth),
                    "PHP({m}) is affine-shear-rigid — no genuine depth-{depth} shear"
                );
            }
            assert!(nullstellensatz_refutes(nv, &php.clauses, 2 * (m - 1)), "PHP({m}) NS degree grows to 2(m−1)");
        }
        // Parity block: a nontrivial shear appears at depth 2 (never depth 1), and it is satisfiable.
        for w in [3usize, 4, 5] {
            let vars: Vec<u32> = (0..w as u32).collect();
            let clauses: Vec<Vec<Lit>> = (0u32..(1 << w))
                .filter(|p| p.count_ones() % 2 == 1)
                .map(|p| (0..w).map(|i| Lit::new(vars[i], (p >> i) & 1 == 0)).collect())
                .collect();
            assert!(affine_composite_shear_generators(w, &clauses, 1).is_empty(), "parity({w}): no depth-1 shear");
            assert!(
                affine_composite_shear_generators(w, &clauses, 2).iter().any(|(s, _)| s.len() == 2),
                "parity({w}): a genuine depth-2 shear exists — constant, does not grow with w"
            );
        }
    }

    /// **The characteristic-2 obstruction to symmetrizing a proof — why the witness must be found *natively*.**
    /// Over a field of characteristic 0 the Reynolds operator `L ↦ (1/|G|) Σ_{g∈G} g·L` averages *any* valid
    /// witness into a symmetric one, so "the extremal witness is symmetric" is free (Razborov's symmetric
    /// pseudo-expectation is obtained this way). Over `GF(2)` there is no `1/|G|`, and the un-normalized sum
    /// `Σ_{g∈G} g·L` evaluates on the constant monomial to `Σ_{g} L(g⁻¹·1) = |G|·L(1) = |G| (mod 2)` — so when
    /// `|G|` is **even** it *annihilates* the normalization `L(1)=1`, collapsing the witness to the zero
    /// functional. The pigeonhole group `Sₘ × Sₘ₋₁` has order `m!·(m−1)!`, even for every `m ≥ 2`. So symmetry
    /// is **not** free here: averaging destroys the witness, and the symmetric pseudo-expectation
    /// (the hole-injective indicator) must be exhibited *natively* — which is exactly what the parity-aware
    /// construction does. This is the GF(2)-specific sauce: the degree bound lives precisely where a native
    /// symmetric proof survives an obstruction that kills the averaged one.
    #[test]
    fn over_gf2_symmetrizing_a_proof_annihilates_when_the_group_is_even() {
        for m in [3usize, 4] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            let d = 2 * holes - 1;
            let group = close_perm_group(&crate::hypercube::php_perm_symmetries(m), php.num_vars);
            let expected_order: usize =
                (1..=m).product::<usize>() * (1..=holes).product::<usize>(); // m! · (m−1)!
            assert_eq!(group.len(), expected_order, "PHP({m}): |Sₘ × Sₘ₋₁| = m!·(m−1)!");
            assert_eq!(group.len() % 2, 0, "PHP({m}): the pigeonhole group is even");

            // A genuine, re-checkable degree-d witness exists.
            let witness = ns_lower_bound_witness(php.num_vars, &php.clauses, d).expect("witness exists");
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, d, &witness), "the witness re-checks");
            assert!(witness.contains(&0u64), "a valid pseudo-expectation carries L(1)=1 (the empty monomial)");

            // Reynolds over GF(2) annihilates it: the constant monomial is toggled |G| times ⟹ gone.
            let averaged = symmetrize(&witness, &group);
            assert!(
                !averaged.contains(&0u64),
                "PHP({m}): symmetrizing over an even group kills L(1)=1 — the averaged witness is degenerate"
            );

            // Yet the NATIVE symmetric witness (hole-injective indicator) is both invariant AND valid.
            let native: Vec<u64> = (0u64..(1u64 << php.num_vars))
                .filter(|&mo| mo.count_ones() as usize <= d && php_is_hole_injective(mo, holes))
                .collect();
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, d, &native), "PHP({m}): native witness valid");
            let native_set: BTreeSet<Mono> = native.iter().copied().collect();
            for g in &group {
                for &mo in &native {
                    assert!(native_set.contains(&apply_perm_to_mono(g, mo)), "PHP({m}): native witness is invariant");
                }
            }
            eprintln!(
                "PHP({m}): |G|={} (even) ⟹ averaged witness annihilated; native symmetric witness = {} monomials survives",
                group.len(), native.len()
            );
        }
    }

    /// **A structural finding: over GF(2), the pigeonhole witness is NOT the classical matching one.** The
    /// restricted-basis tool is sound — with the full (all-monomial) sub-basis it reproduces a valid witness.
    /// We then probe the classical char-0 structure (Razborov's pseudo-expectation, supported on partial
    /// matchings) over GF(2): it does **not** carry the witness. The reason is a parity obstruction — the
    /// pigeon-clause constraint on the matching indicator reduces to `1 + (holes − |m|) ≡ 0 (mod 2)`, which
    /// fails for half the monomials. So the GF(2) degree lower bound needs a genuinely different (parity-aware)
    /// witness structure than the field-of-characteristic-0 case — an honest, non-obvious observation the tool
    /// surfaces, and a caution for anyone porting classical lower bounds to `GF(2)`.
    #[test]
    fn pigeonhole_witness_structure_differs_over_gf2() {
        for (m, deg) in [(3usize, 4usize), (4, 6)] {
            let (php, _) = crate::families::php(m);
            let holes = m - 1;
            // Soundness of the restricted-basis tool: the full sub-basis reproduces a valid witness.
            let full = ns_lower_bound_witness_on_basis(php.num_vars, &php.clauses, deg - 1, &|_| true)
                .expect("full-basis witness exists");
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, deg - 1, &full), "full-basis witness re-checks");
            // The classical partial-matching sub-basis does NOT carry the GF(2) witness (parity obstruction:
            // it also forbids pigeon repeats, which GF(2) does not require).
            let pm = move |mono: Mono| php_is_partial_matching(mono, holes);
            let on_pm = ns_lower_bound_witness_on_basis(php.num_vars, &php.clauses, deg - 1, &pm);
            // The correct GF(2) support is HOLE-INJECTIVE monomials — the at-most-one clauses vanish exactly
            // on hole collisions. This looser sub-basis DOES carry a valid, re-checkable witness.
            let hi = move |mono: Mono| php_is_hole_injective(mono, holes);
            let on_hi = ns_lower_bound_witness_on_basis(php.num_vars, &php.clauses, deg - 1, &hi);
            eprintln!(
                "PHP({m}) over GF(2): partial-matching carries witness? {} ; hole-injective? {}",
                on_pm.is_some(),
                on_hi.is_some()
            );
            assert!(on_pm.is_none(), "PHP({m}): partial-matching sub-basis fails (too strict for GF(2))");
            let w = on_hi.expect("hole-injective sub-basis must carry the GF(2) witness");
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, deg - 1, &w), "PHP({m}): hole-injective witness re-checks");
            assert!(w.iter().all(|&mo| php_is_hole_injective(mo, holes)), "PHP({m}): witness supported on hole-injective monomials");
        }
    }

    fn parametric_family_has_machine_checked_degree_growth() {
        for n in 2..=5usize {
            let f_n: Vec<Vec<Lit>> = (0u64..(1u64 << n))
                .map(|a| (0..n as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect())
                .collect();
            let w = ns_lower_bound_witness(n, &f_n, n - 1)
                .unwrap_or_else(|| panic!("F_{n}: a degree-(n-1) lower-bound witness must exist"));
            assert!(check_ns_lower_bound(n, &f_n, n - 1, &w), "F_{n}: the degree-{} lower bound re-checks", n - 1);
            assert!(nullstellensatz_refutes(n, &f_n, n), "F_{n}: a degree-{n} refutation exists (NS-degree = n)");
            assert!(!nullstellensatz_refutes(n, &f_n, n - 1), "F_{n}: no degree-(n-1) refutation (NS-degree > n-1)");
        }
        // Bounded-width data points: PHP is a COUNTING principle — incomparable to GF(2) algebra — so it is
        // algebraically hard for Nullstellensatz. We certify `NS-degree(PHP(m)) > 3` for m = 3 (6 vars) AND
        // m = 4 (12 vars), the latter with a monomial basis of 299 ≫ 63 (exercising the multi-word solver).
        // These are genuine, non-width-driven degree lower bounds, each a re-checkable dual witness.
        let probe = 3usize;
        for pigeons in [3usize, 4] {
            let (php, _) = crate::families::php(pigeons);
            let min_deg = (1..=probe).find(|&d| nullstellensatz_refutes(php.num_vars, &php.clauses, d));
            eprintln!("PHP({pigeons}): {} vars, min GF(2) NS degree (probed ≤{probe}) = {min_deg:?}", php.num_vars);
            let (d, msg) = match min_deg {
                Some(d) if d >= 2 => (d - 1, "min-1"),
                None => (probe, "> probe (counting is NS-hard)"),
                _ => continue,
            };
            let w = ns_lower_bound_witness(php.num_vars, &php.clauses, d)
                .unwrap_or_else(|| panic!("PHP({pigeons}): a degree-{d} lower-bound witness must exist"));
            assert!(check_ns_lower_bound(php.num_vars, &php.clauses, d, &w), "PHP({pigeons}): degree-{d} lower bound ({msg}) re-checks");
        }
    }

    /// **Degree lower bounds are re-checkable certificates, dual to refutation existence.** The witness `L`
    /// exists *exactly* when no degree-`d` refutation does (`ns_lower_bound_witness` ⟺ `¬nullstellensatz_refutes`),
    /// and when present it re-checks — turning "our solver found no proof" into an independently verifiable
    /// lower bound `NS-degree(F) > d`. Checked on random formulas and on a family with minimum degree exactly
    /// `n` (the all-corners cube: a witness at `d = n−1`, none at `d = n`).
    #[test]
    fn ns_degree_lower_bounds_are_certifiable_and_dual_to_refutation() {
        // Consistency + re-checkability on random formulas across degrees.
        let mut s = 0xCAFE_F00D_1234_9999u64;
        let mut rng = || {
            s ^= s << 13;
            s ^= s >> 7;
            s ^= s << 17;
            s
        };
        for _ in 0..120 {
            let n = 3 + (rng() % 3) as usize; // 3..=5
            let m = 2 + (rng() % 8) as usize;
            let clauses: Vec<Vec<Lit>> = (0..m)
                .map(|_| {
                    let mut c = Vec::new();
                    for v in 0..n {
                        if rng() % 2 == 0 {
                            c.push(Lit::new(v as u32, rng() % 2 == 0));
                        }
                    }
                    if c.is_empty() {
                        c.push(Lit::new((rng() % n as u64) as u32, rng() % 2 == 0));
                    }
                    c
                })
                .collect();
            for d in 1..=n {
                let refutes = nullstellensatz_refutes(n, &clauses, d);
                match ns_lower_bound_witness(n, &clauses, d) {
                    Some(w) => {
                        assert!(!refutes, "a lower-bound witness exists only when there is NO degree-{d} refutation");
                        assert!(check_ns_lower_bound(n, &clauses, d, &w), "the lower-bound witness must re-check");
                    }
                    None => assert!(refutes, "no witness ⟹ a degree-{d} refutation exists"),
                }
            }
        }
        // A family with minimum degree exactly n: the all-corners cube. Certified lower bound at n−1.
        for n in 3..=4usize {
            let all_corners: Vec<Vec<Lit>> = (0u64..(1u64 << n))
                .map(|a| (0..n as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect())
                .collect();
            let w = ns_lower_bound_witness(n, &all_corners, n - 1)
                .expect("all-corners has no degree-(n−1) refutation — a lower bound witness exists");
            assert!(check_ns_lower_bound(n, &all_corners, n - 1, &w), "the degree-(n−1) lower bound re-checks");
            assert!(ns_lower_bound_witness(n, &all_corners, n).is_none(), "at full degree n a refutation exists");
        }
    }

    /// **No finite randomness — but at exponential cost, which is why it is NOT P = NP.** "For finite `n`,
    /// random does not exist" is a *theorem*: every unsatisfiable formula over `n` variables has a degree-`≤n`
    /// GF(2) Nullstellensatz certificate (completeness), so nothing is structureless — verified constructively
    /// on the hardest object (all `2ⁿ` corners forbidden) at `n = 5, 6`. What this does NOT give is efficiency:
    /// the degree-`n` certificate lives in the full multilinear basis of size `2ⁿ`, so its *existence* is an
    /// information-theoretic fact about the finite cube, not a fast proof. P vs NP is asymptotic (about a
    /// family as `n → ∞`); "P = NP for finite `n`" is vacuous (a fixed finite problem is `O(1)` by table
    /// lookup). The honest content is exactly this gap: structure always exists, and it always costs `2ⁿ`.
    #[test]
    fn no_finite_randomness_but_the_certificate_is_exponentially_large() {
        // No structureless finite formula: the hardest object (every corner forbidden) is refuted at n.
        for n in 5..=6usize {
            let all_corners: Vec<Vec<Lit>> = (0u64..(1u64 << n))
                .map(|a| (0..n as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect())
                .collect();
            assert!(build_ns_certificate(n, &all_corners).is_ok(), "n={n}: no structureless formula — a certificate exists");
        }
        // But the full-degree NS system is exactly 2ⁿ wide — the certificate exists in EXPONENTIAL space.
        for n in 1..=16usize {
            assert_eq!(nullstellensatz_basis_size(n, n), 1u128 << n, "the degree-n NS basis is exactly 2ⁿ");
            // Monotone in the degree budget; the cheap (bounded-degree) fragment is a vanishing slice at large n.
            assert!(nullstellensatz_basis_size(n, n / 2) <= nullstellensatz_basis_size(n, n), "basis grows with degree");
        }
        // Exponential, not polynomial: by n=40 the certificate space (2⁴⁰ ≈ 10¹²) dwarfs any fixed poly like n⁶.
        assert!(nullstellensatz_basis_size(40, 40) > 40u128.pow(6), "the certificate space is exponential, not polynomial");
    }

    /// **We PROVE, we do not iterate: structureless = 0 past the census wall.** The `Bₙ`-orbit census is
    /// infeasible at `n = 5` (~10⁷ orbits); it can only *measure* `structureless = 0` up to `n = 4`. The
    /// uniform construction settles it by *proof*: at `n = 5, 6, 7` it is a total, certifying decision on
    /// hundreds of random formulas — every UNSAT instance gets a certificate that re-checks (degree ≤ n) and
    /// is genuinely modelless by brute force; every SAT instance gets a model that satisfies it. One
    /// construction, correct at every `n`: no minimal-UNSAT family is ever structureless.
    #[test]
    fn ns_construction_is_total_and_sound_past_the_census_wall() {
        let mut state = 0x1234_5678_9abc_def0u64;
        let mut rng = || {
            state ^= state << 13;
            state ^= state >> 7;
            state ^= state << 17;
            state
        };
        for &n in &[5usize, 6, 7] {
            for _ in 0..150 {
                let num_clauses = n + (rng() % (3 * n as u64)) as usize;
                let clauses: Vec<Vec<Lit>> = (0..num_clauses)
                    .map(|_| {
                        let width = 2 + (rng() % 2) as usize; // 2- or 3-clauses
                        let mut seen = std::collections::HashSet::new();
                        let mut c = Vec::new();
                        while c.len() < width {
                            let v = (rng() % n as u64) as u32;
                            if seen.insert(v) {
                                c.push(Lit::new(v, rng() & 1 == 0));
                            }
                        }
                        c
                    })
                    .collect();
                match build_ns_certificate(n, &clauses) {
                    Ok(cert) => {
                        assert!(cert.verify(&clauses), "n={n}: the constructive certificate must re-check");
                        assert!(cert.degree() <= n, "n={n}: the certificate degree must be ≤ n");
                        assert!(!sat(n, &clauses), "n={n}: a certificate is issued only for a genuinely UNSAT formula");
                    }
                    Err(model) => {
                        assert!(sat(n, &clauses), "n={n}: SAT witness ⟹ the formula is genuinely satisfiable");
                        assert!(
                            clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
                            "n={n}: the returned model must satisfy every clause"
                        );
                    }
                }
            }
        }
    }

    /// **Truly random can't live in a finite hypercube — the complexity is *capped by the dimension*.**
    /// True (Martin-Löf) randomness needs *unbounded* Kolmogorov complexity. But the `n`-cube is finite,
    /// and Nullstellensatz is **complete at degree `n`** — every unsatisfiable formula over `n` variables
    /// has its `1`-in-the-ideal certificate by degree `n`, no higher. So the proof-complexity (the
    /// "randomness" measure) is **bounded by `n`**, never unbounded. The cube holds only the *finite
    /// shadow* of randomness — incompressible-relative-to-size, capped at the dimension. Truly random,
    /// being unbounded, has no room. We verify the cap on the maximally-constrained ("most random") UNSAT
    /// formula: it is decided exactly at degree `n`.
    #[test]
    fn truly_random_cannot_live_in_a_finite_hypercube() {
        for nv in 3..=5 {
            // The hardest object: every one of the 2ⁿ assignments forbidden by a full-width clause.
            let mut cl: Vec<Vec<Lit>> = Vec::new();
            for a in 0..(1u32 << nv) {
                cl.push((0..nv as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect());
            }
            assert!(!sat(nv, &cl), "all assignments forbidden ⟹ UNSAT");
            // It is decided at the dimension-bound degree n — the cap. No formula over n vars needs more.
            assert!(
                nullstellensatz_refutes(nv, &cl, nv),
                "the hardest n={nv} formula is refuted at degree n — complexity capped at the dimension"
            );
        }
    }

    /// **Symmetry collapses Polynomial Calculus to a counting problem — and for pigeonhole it *is* the
    /// pigeonhole count.** The degree-2 monomial basis of PHP(n), `Θ(n⁴)` monomials, collapses under the
    /// grid group `Sₙ × Sₙ₋₁` to a handful of orbit-types — and that handful is *constant in n*. The
    /// symmetric Nullstellensatz system has one column per orbit, so it is `O(1)` wide regardless of
    /// scale; counting those orbit-types is the whole cut. Everything came down to counting.
    #[test]
    fn symmetry_collapses_the_pc_basis_to_a_counting_problem() {
        let mut orbit_counts = Vec::new();
        for n in 3..=5 {
            let (cnf, _) = crate::families::php(n);
            let nv = cnf.num_vars;
            let generators = crate::hypercube::php_perm_symmetries(n);
            let orbits = monomial_orbits(nv, 2, &generators);
            let full = 1 + nv + nv * (nv - 1) / 2; // C(nv,0)+C(nv,1)+C(nv,2)

            // The basis collapses hard — orbit-types are a tiny fraction of the monomials.
            assert!(
                orbits.len() * 3 < full,
                "PHP({n}): {} orbit-types ≪ {full} monomials — the counting collapse",
                orbits.len()
            );
            // Burnside check: the orbits partition the basis exactly (counting is consistent).
            assert_eq!(
                orbits.iter().map(|o| o.len()).sum::<usize>(),
                full,
                "the orbits partition the monomial basis"
            );
            // Each orbit is closed under the symmetry.
            for orbit in &orbits {
                let set: BTreeSet<Mono> = orbit.iter().copied().collect();
                for &m in orbit {
                    for g in &generators {
                        assert!(set.contains(&apply_perm_to_mono(g, m)), "orbit closed under the group");
                    }
                }
            }
            orbit_counts.push(orbits.len());
        }
        // The orbit-type count is essentially constant in n — O(1) symmetric NS width, at every scale.
        let max = *orbit_counts.iter().max().unwrap();
        let min = *orbit_counts.iter().min().unwrap();
        assert!(max - min <= 2, "orbit-type count is ~constant in n: {orbit_counts:?}");
    }

    /// **THE SYMMETRY COST-CUT: `2ⁿ → n+1`, exponential to linear.** The full-degree Nullstellensatz basis is
    /// `2ⁿ` monomials — the brute-force cost of finding structure. But when a formula is *fully symmetric*
    /// (the symmetric group `Sₙ` permutes its variables), an invariant certificate is constant on the monomial
    /// orbits, and under `Sₙ` two monomials are equivalent iff they have the same degree — so the `2ⁿ` basis
    /// collapses to exactly **`n+1` orbit-columns, one per degree**. The Gaussian runs over `n+1` columns, not
    /// `2ⁿ`. That is symmetry = compression, made exact: the exponential search becomes linear. The reduced
    /// certificate is *sound* (an invariant `1`-in-the-span is a genuine refutation), checked here on a
    /// fully-`Sₙ`-symmetric UNSAT family.
    #[test]
    fn symmetry_cuts_the_full_ns_basis_from_exponential_to_linear() {
        for n in 2..=8usize {
            let gens = symmetric_group_generators(n);
            let orbits = monomial_orbits(n, n, &gens);
            // Under Sₙ, the 2ⁿ full-degree basis collapses to exactly n+1 orbits — one per monomial degree.
            assert_eq!(orbits.len(), n + 1, "Sₙ collapses the 2ⁿ basis to n+1 degree-orbits (n={n})");
            assert_eq!(nullstellensatz_basis_size(n, n), 1u128 << n, "the full basis is 2ⁿ");
            // Each orbit is *all* monomials of one degree, so the orbit sizes are exactly {C(n,k)}.
            let mut sizes: Vec<u128> = orbits.iter().map(|o| o.len() as u128).collect();
            sizes.sort_unstable();
            let mut binoms: Vec<u128> = (0..=n).map(|k| binom(n, k)).collect();
            binoms.sort_unstable();
            assert_eq!(sizes, binoms, "each degree-orbit k has C(n,k) monomials");
        }
        // The cut deepens without bound: 2ⁿ / (n+1) → ∞. Symmetry turns the exponential basis linear.
        let cut = |n: u32| (1u128 << n) / (n as u128 + 1);
        assert!(cut(8) > cut(4) && cut(4) > cut(2), "the symmetry cut 2ⁿ/(n+1) grows with n");

        // SOUNDNESS of the collapsed certificate: on a fully-Sₙ-symmetric UNSAT family (every corner
        // forbidden), the symmetry-reduced NS — over the n+1 orbit columns, not 2ⁿ — still refutes, and agrees
        // with full NS. The cheap certificate is a real one.
        for n in 2..=5usize {
            let all_corners: Vec<Vec<Lit>> = (0u64..(1u64 << n))
                .map(|a| (0..n as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect())
                .collect();
            let gens = symmetric_group_generators(n);
            assert!(nullstellensatz_refutes(n, &all_corners, n), "full NS refutes all-corners at degree n");
            assert!(
                nullstellensatz_refutes_symmetric(n, &all_corners, n, &gens),
                "the symmetry-reduced NS (n+1 columns) still refutes — the 2ⁿ→n+1 cut is sound (n={n})"
            );
        }
    }

    /// **Nullstellensatz at full degree is a complete, sound decision** — verified against brute force on
    /// a fuzz: a degree-`num_vars` refutation exists iff the formula is unsatisfiable.
    #[test]
    fn nullstellensatz_full_degree_matches_brute_force() {
        fn sm(s: &mut u64) -> u64 {
            *s = s.wrapping_add(0x9E37_79B9_7F4A_7C15);
            let mut z = *s;
            z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
            z ^ (z >> 31)
        }
        let mut state = 0x9015_0001u64;
        for _ in 0..60 {
            let nv = 3 + (sm(&mut state) % 3) as usize; // 3..5 vars
            let m = 3 + (sm(&mut state) % 8) as usize;
            let mut cl: Vec<Vec<Lit>> = Vec::new();
            for _ in 0..m {
                let mut c = Vec::new();
                for v in 0..nv {
                    if sm(&mut state) % 2 == 0 {
                        c.push(Lit::new(v as u32, sm(&mut state) % 2 == 0));
                    }
                }
                if !c.is_empty() {
                    cl.push(c);
                }
            }
            if cl.is_empty() {
                continue;
            }
            let unsat = !sat(nv, &cl);
            assert_eq!(
                nullstellensatz_refutes(nv, &cl, nv),
                unsat,
                "NS at full degree must decide exactly: {cl:?}"
            );
        }
    }

    /// **Parity is the degree-1 fragment.** An odd XOR cycle (`x_i ≠ x_{i+1}` around a 5-cycle) is
    /// unsatisfiable, and Nullstellensatz refutes it at the low degree its width permits — the algebraic
    /// form of the parity cut, now inside the one general engine.
    #[test]
    fn nullstellensatz_refutes_parity_at_low_degree() {
        // 2-colouring an odd cycle: (x_u ∨ x_v) ∧ (¬x_u ∨ ¬x_v) per edge — UNSAT for an odd cycle.
        let edges = [(0u32, 1u32), (1, 2), (2, 3), (3, 4), (4, 0)];
        let mut cl = Vec::new();
        for (u, v) in edges {
            cl.push(vec![Lit::new(u, true), Lit::new(v, true)]);
            cl.push(vec![Lit::new(u, false), Lit::new(v, false)]);
        }
        assert!(!sat(5, &cl), "odd-cycle 2-colouring is UNSAT");
        assert!(nullstellensatz_refutes(5, &cl, 2), "NS refutes the parity obstruction at degree 2");
    }

    /// **The degree dial has real teeth: a refutation can need more than the minimum.** A formula that is
    /// UNSAT but whose only Nullstellensatz certificate needs the full degree is *not* refuted below it —
    /// the engine honestly reports "no low-degree algebraic proof," which is the hardness signal.
    #[test]
    fn the_degree_is_a_genuine_power_dial() {
        // All eight 3-clauses over x0,x1,x2 forbidding each assignment ⟹ UNSAT; needs degree 3 (the width).
        let mut cl = Vec::new();
        for a in 0u32..8 {
            cl.push(
                (0..3u32)
                    .map(|v| Lit::new(v, (a >> v) & 1 == 0))
                    .collect::<Vec<Lit>>(),
            );
        }
        assert!(!sat(3, &cl), "all 8 assignments forbidden ⟹ UNSAT");
        assert!(!nullstellensatz_refutes(3, &cl, 2), "no degree-2 certificate — width-3 clauses unusable");
        assert!(nullstellensatz_refutes(3, &cl, 3), "degree 3 refutes it");
    }

    /// Soundness, isolated: a satisfiable formula has **no** Nullstellensatz refutation at any degree.
    #[test]
    fn satisfiable_formulas_are_never_refuted() {
        let cl = vec![vec![Lit::new(0, true), Lit::new(1, true)], vec![Lit::new(0, false), Lit::new(2, true)]];
        assert!(sat(3, &cl));
        for d in 0..=3 {
            assert!(!nullstellensatz_refutes(3, &cl, d), "a SAT formula is refuted at no degree (d={d})");
        }
    }

    /// **Symmetry-reduced Nullstellensatz collapses the basis and stays sound.** The "all assignments
    /// forbidden" instance is fully symmetric and UNSAT; full NS spans `2ⁿ` monomials, but the
    /// symmetry-reduced refutation runs over the `n+1` weight-class orbits and still refutes — an
    /// exponential column collapse. Soundness: a satisfiable symmetric formula is refuted at no degree.
    #[test]
    fn symmetry_reduced_nullstellensatz_collapses_and_is_sound() {
        for nv in 3..=5usize {
            let mut cl: Vec<Vec<Lit>> = Vec::new();
            for a in 0..(1u32 << nv) {
                cl.push((0..nv as u32).map(|v| Lit::new(v, (a >> v) & 1 == 0)).collect());
            }
            assert!(!sat(nv, &cl), "all assignments forbidden ⟹ UNSAT");
            let gens = crate::symmetry_detect::find_generators(nv, &cl);
            assert!(
                nullstellensatz_refutes_symmetric(nv, &cl, nv, &gens),
                "symmetry-reduced NS refutes the all-forbidden instance (n={nv})"
            );
            let cols = monomial_orbits(nv, nv, &gens).len();
            assert!(cols < (1usize << nv), "n={nv}: {cols} orbit columns ≪ {} monomials", 1usize << nv);
        }
        // Soundness: a satisfiable symmetric formula is refuted at no degree.
        let sat_cl = vec![vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)]];
        let gens = crate::symmetry_detect::find_generators(3, &sat_cl);
        for d in 0..=3 {
            assert!(
                !nullstellensatz_refutes_symmetric(3, &sat_cl, d, &gens),
                "a satisfiable formula has no symmetry-reduced refutation (d={d})"
            );
        }
    }

    /// A deterministic LCG for reproducible fuzz corpora inside tests (no `rand`, no wall clock).
    fn lcg(state: &mut u64) -> u64 {
        *state = state.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407);
        *state >> 33
    }

    /// **The polynomial-generator NS engine agrees with the clause engine on CNFs.** `ns_refutes_polys`
    /// / `ns_lower_bound_witness_polys` / `check_ns_lower_bound_polys` generalize the clause API to
    /// arbitrary `GF(2)` generator systems (the substrate for the linear encoding and the symmetric-family
    /// machinery). Fed the clause polynomials of a CNF they must reproduce the clause engine exactly —
    /// refutability at every degree, witness existence (the duality `refutes(d) ⟺ no witness at d`), and
    /// cross-checker validation both ways. Corpus: pigeonhole, modular counting, a transitive-XOR core,
    /// and a deterministic random-3-CNF fuzz sweep.
    #[test]
    fn ns_over_polynomial_generators_agrees_with_the_clause_encoding_on_cnfs() {
        let mut corpus: Vec<(usize, Vec<Vec<Lit>>)> = Vec::new();
        let (php3, _) = crate::families::php(3);
        corpus.push((php3.num_vars, php3.clauses));
        let (cnt32, _) = crate::families::mod_counting(3, 2);
        corpus.push((cnt32.num_vars, cnt32.clauses));
        let (cnt42, _) = crate::families::mod_counting(4, 2);
        corpus.push((cnt42.num_vars, cnt42.clauses));
        let p = |v: u32| Lit::pos(v);
        let q = |v: u32| Lit::neg(v);
        corpus.push((3, vec![
            vec![q(0), p(1)], vec![p(0), q(1)],
            vec![q(1), p(2)], vec![p(1), q(2)],
            vec![p(0), p(2)], vec![q(0), q(2)],
        ]));
        let mut seed = 0x5EED_CAFE_u64;
        for _ in 0..24 {
            let nv = 4 + (lcg(&mut seed) % 3) as usize; // 4..=6 variables
            let nc = 6 + (lcg(&mut seed) % 12) as usize;
            let mut cl = Vec::new();
            for _ in 0..nc {
                let mut vars: Vec<u32> = Vec::new();
                while vars.len() < 3 {
                    let v = (lcg(&mut seed) % nv as u64) as u32;
                    if !vars.contains(&v) {
                        vars.push(v);
                    }
                }
                cl.push(vars.iter().map(|&v| Lit::new(v, lcg(&mut seed) & 1 == 1)).collect());
            }
            corpus.push((nv, cl));
        }

        for (nv, clauses) in &corpus {
            let gens: Vec<Poly> = clauses.iter().map(|c| clause_polynomial(c)).collect();
            for d in 1..=(*nv).min(5) {
                let clause_verdict = nullstellensatz_refutes(*nv, clauses, d);
                assert_eq!(
                    ns_refutes_polys(*nv, &gens, d),
                    clause_verdict,
                    "n={nv} d={d}: the polynomial-generator engine matches the clause engine"
                );
                let w_clause = ns_lower_bound_witness(*nv, clauses, d);
                let w_polys = ns_lower_bound_witness_polys(*nv, &gens, d);
                assert_eq!(
                    w_clause.is_some(),
                    w_polys.is_some(),
                    "n={nv} d={d}: witness existence agrees across the two engines"
                );
                assert_eq!(
                    w_polys.is_none(),
                    clause_verdict,
                    "n={nv} d={d}: duality — a refutation at d exists iff no degree-d pseudo-expectation"
                );
                if let (Some(wc), Some(wp)) = (w_clause, w_polys) {
                    assert!(
                        check_ns_lower_bound_polys(*nv, &gens, d, &wc),
                        "n={nv} d={d}: the clause-engine witness passes the polynomial checker"
                    );
                    assert!(
                        check_ns_lower_bound(*nv, clauses, d, &wp),
                        "n={nv} d={d}: the polynomial-engine witness passes the clause checker"
                    );
                }
            }
        }
    }

    /// **Degree-bounded monomial enumeration lifts the 20-variable cap.** The clause engine enumerates
    /// `0..2ⁿ` and filters — dead at `n > 20`. `monomials_up_to_degree` walks only the `C(n, ≤d)`
    /// monomials, so fixed-degree work scales to the full `Mono = u64` range. Differential against the
    /// filter on every `n ≤ 12`; counts pinned to `nullstellensatz_basis_size`; and the real payoff
    /// exercised end-to-end: a re-checked degree-2 lower-bound witness on a 22-variable instance (PHP(3)
    /// padded with sixteen spectator variables — the ideal, hence the NS degree, is unchanged), where the
    /// bounded basis has 254 monomials against the 4-million-corner cube.
    #[test]
    fn degree_bounded_monomial_enumeration_scales_past_twenty_variables() {
        for n in 0..=12usize {
            for d in 0..=n {
                let bounded: BTreeSet<Mono> = monomials_up_to_degree(n, d).into_iter().collect();
                let filtered: BTreeSet<Mono> =
                    (0u64..(1u64 << n)).filter(|m| m.count_ones() as usize <= d).collect();
                assert_eq!(bounded, filtered, "n={n} d={d}: bounded enumeration = filtered cube");
                assert_eq!(
                    bounded.len() as u128,
                    nullstellensatz_basis_size(n, d),
                    "n={n} d={d}: the count is Σ C(n,k)"
                );
            }
        }
        // Sorted ascending — the stable index order the witness machinery relies on.
        let ms = monomials_up_to_degree(10, 3);
        assert!(ms.windows(2).all(|w| w[0] < w[1]), "monomials come sorted ascending");
        // Far past the cube: C(40, ≤2) monomials without touching 2^40.
        assert_eq!(monomials_up_to_degree(40, 2).len(), 821); // 1 + 40 + C(40,2)
        assert_eq!(nullstellensatz_basis_size(40, 2), 821);

        // End-to-end at 22 variables: PHP(3) with spectator variables. NS-degree(PHP(3)) = 4, so a
        // degree-2 pseudo-expectation exists — found and re-checked entirely on the bounded basis.
        let (php3, _) = crate::families::php(3);
        let gens: Vec<Poly> = php3.clauses.iter().map(|c| clause_polynomial(c)).collect();
        let nv = 22usize;
        let w = ns_lower_bound_witness_polys(nv, &gens, 2)
            .expect("a degree-2 witness exists for padded PHP(3) — the degree is 4");
        assert!(
            check_ns_lower_bound_polys(nv, &gens, 2, &w),
            "the 22-variable witness re-checks on the bounded basis"
        );
        // Spectators change nothing: the same verdicts as the unpadded instance.
        assert!(!ns_refutes_polys(nv, &gens, 3), "padded PHP(3) is not refuted at degree 3");
        assert!(ns_refutes_polys(nv, &gens, 4), "padded PHP(3) is refuted at degree 4");
    }

    /// **The clause and linear encodings interreduce at bounded degree — with an asymmetric, degree-exact
    /// direction.** For an exactly-one group `G` (at-least-one clause + at-most-one pairs), the wide ALO
    /// clause polynomial `Π_{v∈G}(1+x_v)` and the linear generator `1 + Σ_{v∈G} x_v` differ by a sum of
    /// pair-generator multiples: every `≥2`-subset monomial is a multiple of some pair `x_u x_v`. So:
    /// (i) the syntactic identity `Π(1+x) + (1+Σx) ∈ span{m·(x_u x_v)}` at degree `|G|`, exactly;
    /// (ii) **clause-refutable at `d` ⟹ linear-refutable at `d`** (degree-preserving — every clause
    ///     generator rewrites into linear generators of no larger degree), which is why lower bounds
    ///     proven against the linear encoding are the stronger statements (the literature-standard form);
    /// (iii) linear-refutable at `d` ⟹ clause-refutable at `d + k−1` (`k` = the widest group) — the
    ///     honest reverse transfer with its explicit degree tax.
    #[test]
    fn the_linear_and_clause_encodings_interreduce_at_bounded_degree() {
        // (i) The syntactic identity, exactly, for group sizes 2..=6.
        for k in 2..=6usize {
            let group: Vec<u32> = (0..k as u32).collect();
            let alo: Vec<Lit> = group.iter().map(|&v| Lit::pos(v)).collect();
            let clause_poly = clause_polynomial(&alo);
            let gens = exactly_one_linear_generators(&[group.clone()]);
            let linear: &Poly = &gens[0]; // the 1 + Σ x_v generator leads; pairs follow
            assert_eq!(linear.len(), k + 1, "the linear generator is 1 + Σ x (k+1 monomials)");
            assert_eq!(gens.len(), 1 + k * (k - 1) / 2, "one linear generator plus C(k,2) pairs");
            let mut diff = clause_poly.clone();
            for &m in linear {
                toggle(&mut diff, m);
            }
            // diff = Σ_{|S|≥2} x_S must lie in span{ m · pair : deg ≤ k }.
            let mut index: HashMap<Mono, usize> = HashMap::new();
            for m in 0u64..(1u64 << k) {
                let i = index.len();
                index.insert(m, i);
            }
            let words = index.len().div_ceil(64).max(1);
            let to_bits = |p: &Poly| -> Vec<u64> {
                let mut b = vec![0u64; words];
                for &m in p {
                    b[index[&m] / 64] |= 1 << (index[&m] % 64);
                }
                b
            };
            let mut rows = Vec::new();
            for pair in &gens[1..] {
                for m in monomials_up_to_degree(k, k) {
                    let prod = poly_mul_mono(pair, m);
                    if !prod.is_empty() && poly_degree(&prod) <= k {
                        rows.push(to_bits(&prod));
                    }
                }
            }
            assert!(
                in_gf2_span(rows, &to_bits(&diff)),
                "k={k}: Π(1+x) + (1+Σx) is a sum of pair-generator multiples at degree k"
            );
        }

        // (ii)+(iii) The semantic transfer, measured on modular counting (the W2 substrate).
        for (n, q) in [(3usize, 2usize), (5, 2)] {
            let (cnf, _) = crate::families::mod_counting(n, q);
            let nv = cnf.num_vars;
            // The exactly-one groups are the all-positive covering clauses; AMO pairs are the rest.
            let groups: Vec<Vec<u32>> = cnf
                .clauses
                .iter()
                .filter(|c| c.iter().all(|l| l.is_positive()))
                .map(|c| c.iter().map(|l| l.var()).collect())
                .collect();
            assert_eq!(groups.len(), n, "one exactly-one group per point");
            let k = groups.iter().map(|g| g.len()).max().unwrap();
            let linear_gens = exactly_one_linear_generators(&groups);
            let clause_gens: Vec<Poly> = cnf.clauses.iter().map(|c| clause_polynomial(c)).collect();
            let dmax = nv.min(5);
            for d in 1..=dmax {
                if ns_refutes_polys(nv, &clause_gens, d) {
                    assert!(
                        ns_refutes_polys(nv, &linear_gens, d),
                        "Count_{q}({n}) d={d}: clause-refutable ⟹ linear-refutable at the SAME degree"
                    );
                }
                if ns_refutes_polys(nv, &linear_gens, d) {
                    assert!(
                        ns_refutes_polys(nv, &clause_gens, (d + k - 1).min(nv)),
                        "Count_{q}({n}) d={d}: linear-refutable ⟹ clause-refutable at d + k − 1"
                    );
                }
            }
            // The linear encoding refutes an UNSAT counting instance at low degree somewhere ≤ dmax.
            assert!(
                (1..=dmax).any(|d| ns_refutes_polys(nv, &linear_gens, d)),
                "Count_{q}({n}): the linear encoding refutes within the probed degrees"
            );
        }
    }

    /// **The char-matched control: `Count_2` collapses to degree 1 over `GF(2)`.** The linear encoding's
    /// point generators are `GF(2)` linear equations `1 + Σ_{e∋i} x_e`; summing all `n` of them counts
    /// each edge `q = 2` times, so the edge terms cancel and the sum is `n·1 = 1` for odd `n` — a
    /// degree-**1** Nullstellensatz refutation, pure linear algebra. This is the characteristic-matched
    /// foil for the mismatch row: the same family that is resolution-hard (Ajtai; Beame–Pitassi) is
    /// trivial for the algebra whose characteristic divides the count. Even `n` is SAT (a perfect
    /// matching exists), and soundness holds: no refutation at any probed degree.
    #[test]
    fn count_two_is_char_matched_and_falls_to_low_degree_gf2_ns() {
        for n in [3usize, 5, 7] {
            let (cnf, _) = crate::families::mod_counting(n, 2);
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 2));
            assert!(
                ns_refutes_polys(cnf.num_vars, &gens, 1),
                "Count_2({n}), n odd: linear-encoded NS degree 1 — the char-matched collapse"
            );
        }
        for n in [4usize, 6] {
            let (cnf, _) = crate::families::mod_counting(n, 2);
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 2));
            for d in 1..=3 {
                assert!(
                    !ns_refutes_polys(cnf.num_vars, &gens, d),
                    "Count_2({n}), n even: SAT (a perfect matching) ⟹ no refutation at degree {d}"
                );
            }
        }
    }

    /// **The char-mismatch row: `Count_3` has certified, growing, non-width `GF(2)` NS degree — in two
    /// provably distinct regimes.** The modular counting principle with `3 ∤ n` is UNSAT by a mod-3
    /// argument `GF(2)` algebra cannot make at low degree; on the **linear encoding** (degree-1 point
    /// generators `P_i = 1 + Σ_{e∋i} x_e` + degree-2 overlap pairs — the encoding the literature states
    /// bounds against, and the *stronger* side of the interreduction):
    ///
    /// - **The dense degenerate regime `n < 2q` (`n = 4, 5`): exact degree 2.** Below `n = 6` every two
    ///   triples of `[n]` intersect, so for any `f` and `i ∉ f`, `x_f·P_i ≡ x_f` mod the pairs — every
    ///   variable enters the degree-2 span, and with `Σ_i P_i = n + Σ_e x_e (mod 2)` (each edge counted
    ///   `q = 3 ≡ 1` times) the constant `1` follows. Degree 1 is impossible: a sum `Σ_{i∈S} P_i = 1`
    ///   needs `|e ∩ S|` even for every triple `e` with `|S|` odd, and no such `S ⊆ [n]` exists (a
    ///   singleton meets some triple once; a triple meets itself thrice). Both halves certified.
    /// - **The genuine regime (`n = 7, 8` — 35 and 56 variables, reachable only through the
    ///   degree-bounded basis): NS-degree ≥ 3, certified.** The re-checked dual witness at degree 2
    ///   exceeds every generator's degree (non-width) and the bound grows from the degenerate regime's
    ///   2. The exact upper half (refutation at degree 3) is release-scale Gaussian elimination and
    ///   lives in the `#[ignore]` scale probe, measured `= 3` at both `n`.
    ///
    /// The `GF(3)` route refutes the same family in microseconds — together the marquee two-sided
    /// characteristic-mismatch row of the separations atlas.
    #[test]
    fn count_three_has_certified_growing_non_width_ns_degree_over_gf2() {
        // Dense degenerate regime: exact degree 2, both halves certified.
        for n in [4usize, 5] {
            let (cnf, _) = crate::families::mod_counting(n, 3);
            let nv = cnf.num_vars;
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 3));
            assert!(!ns_refutes_polys(nv, &gens, 1), "Count_3({n}): no degree-1 refutation");
            let w1 = ns_lower_bound_witness_polys(nv, &gens, 1).expect("dual witness at degree 1");
            assert!(check_ns_lower_bound_polys(nv, &gens, 1, &w1), "Count_3({n}): NS-degree > 1 re-checks");
            assert!(
                ns_refutes_polys(nv, &gens, 2),
                "Count_3({n}), n < 2q: every two blocks overlap ⟹ the degree-2 collapse"
            );
            eprintln!("Count_3({n}): certified exact linear-encoded GF(2) NS degree = 2 (dense regime)");
        }
        // Genuine regime: certified NS-degree ≥ 3 — non-width, and growth past the dense regime.
        for n in [7usize, 8] {
            let (cnf, _) = crate::families::mod_counting(n, 3);
            let nv = cnf.num_vars;
            assert!(nv > 20, "the genuine regime lives past the clause engine's cap ({nv} vars)");
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 3));
            let w2 = ns_lower_bound_witness_polys(nv, &gens, 2)
                .expect("a degree-2 pseudo-expectation exists — the degree exceeds 2");
            assert!(
                check_ns_lower_bound_polys(nv, &gens, 2, &w2),
                "Count_3({n}): NS-degree ≥ 3 re-checks with zero trust"
            );
            eprintln!("Count_3({n}) [{nv} vars]: certified NS-degree ≥ 3 (exact = 3 in the scale probe)");
        }
    }

    /// **The exact upper half at scale: `Count_3(7)` and `Count_3(8)` refute at degree 3, exactly.**
    /// The certified test carries the lower half (re-checked degree-2 dual witnesses); this probe pins
    /// the refutations at degree 3 — 35- and 56-variable Gaussian eliminations over the degree-bounded
    /// basis, minutes at test-profile optimization — locking the exact linear-encoded degree
    /// `NS-degree(Count_3(7)) = NS-degree(Count_3(8)) = 3`.
    #[test]
    #[ignore = "scale measurement — minutes of Gaussian elimination; run explicitly or via the fast suite"]
    fn count_three_scale_probe_measures_the_degree_growth() {
        for n in [7usize, 8] {
            let (cnf, _) = crate::families::mod_counting(n, 3);
            let nv = cnf.num_vars;
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 3));
            assert!(!ns_refutes_polys(nv, &gens, 2), "Count_3({n}): no degree-2 refutation");
            assert!(ns_refutes_polys(nv, &gens, 3), "Count_3({n}): refuted at degree 3 — exact");
            eprintln!("Count_3({n}) [{nv} vars]: exact linear-encoded GF(2) NS degree = 3");
        }
    }

    /// Is a `Count_q` monomial a **partial partition** — a set of pairwise-disjoint blocks? The
    /// counting-family analog of pigeonhole's partial matchings.
    fn count_is_disjoint(mono: Mono, edges: &[Vec<usize>]) -> bool {
        let mut used = 0u64;
        let mut bits = mono;
        while bits != 0 {
            let e = bits.trailing_zeros() as usize;
            let mask: u64 = edges[e].iter().fold(0, |m, &v| m | (1u64 << v));
            if used & mask != 0 {
                return false;
            }
            used |= mask;
            bits &= bits - 1;
        }
        true
    }

    /// **The `Count_3` witness support: the invariant closed form lives on a Lucas schedule in `n`, and
    /// off-schedule symmetry and validity part ways.** The `Sₙ`-invariant degree-2 pseudo-expectation
    /// on the **partial-partition support** (pairwise-disjoint blocks — the counting analog of partial
    /// matchings) is forced onto type values `(a, b₀)` (singles, disjoint pairs); solving the type
    /// constraints by hand: the pair generators vanish outright, `⟨L, P_i⟩ = 1 + C(n−1,2)·a` pins `a`,
    /// and `⟨L, x_f·P_i⟩` with `i ∉ f` contributes `a + C(n−4, 2)·b₀` — so an **invariant** witness on
    /// this support exists iff those binomials are odd: a parity-of-binomials condition, `n ≡ 3 (mod 4)`
    /// (Lucas). Machine-locked, both faces:
    ///
    /// - **`n = 7` (on schedule):** the explicit indicator `L(M) = [M pairwise disjoint]` is valid — a
    ///   closed-form, symmetry-invariant witness, the analog of pigeonhole's hole-injective one.
    /// - **`n = 8` (off schedule):** *all four* invariant candidates on the disjoint support (the whole
    ///   `(a, b₀)` cube) are invalid — machine-enumerated — yet the sub-basis search still finds a
    ///   valid witness on the very same support, necessarily **non-invariant**. The Reynolds
    ///   obstruction (`over_gf2_symmetrizing_a_proof_annihilates_when_the_group_is_even`) live at a
    ///   concrete scale: over `GF(2)`, off the Lucas schedule, no symmetric witness survives where
    ///   asymmetric ones do. This is the phenomenon the symmetric-collapse machinery must respect (its
    ///   verdicts are about *invariant* certificates), and the first concrete face of the
    ///   periodicity-in-`n` it is built to decide.
    #[test]
    fn count_three_witness_support_structure_is_probed_on_sub_bases() {
        // Dense regime, degree 1: the disjoint support carries (singles are always disjoint).
        for n in [4usize, 5] {
            let (cnf, _) = crate::families::mod_counting(n, 3);
            let nv = cnf.num_vars;
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 3));
            let full = ns_lower_bound_witness_polys_on_basis(nv, &gens, 1, &|_| true)
                .expect("the unrestricted sub-basis search reproduces the witness");
            assert!(check_ns_lower_bound_polys(nv, &gens, 1, &full), "the control witness re-checks");
            let edges = crate::families::mod_counting_edges(n, 3);
            let probe =
                ns_lower_bound_witness_polys_on_basis(nv, &gens, 1, &|m| count_is_disjoint(m, &edges));
            let w = probe.expect("dense regime, degree 1: the disjoint support carries the witness");
            assert!(check_ns_lower_bound_polys(nv, &gens, 1, &w), "the sub-basis witness re-checks");
        }

        // Genuine regime, degree 2: the invariant closed form on its n mod 4 schedule.
        for n in [7usize, 8] {
            let on_schedule = n % 4 == 3;
            let (cnf, _) = crate::families::mod_counting(n, 3);
            let nv = cnf.num_vars;
            let gens = exactly_one_linear_generators(&crate::families::mod_counting_groups(n, 3));
            let edges = crate::families::mod_counting_edges(n, 3);
            let disjoint: Vec<Mono> = monomials_up_to_degree(nv, 2)
                .into_iter()
                .filter(|&m| count_is_disjoint(m, &edges))
                .collect();
            // Every invariant candidate on the disjoint support: L(1)=1, singles ∈ {0,1}, pairs ∈ {0,1}.
            for (a, b0) in [(false, false), (false, true), (true, false), (true, true)] {
                let candidate: Vec<Mono> = disjoint
                    .iter()
                    .copied()
                    .filter(|&m| match m.count_ones() {
                        0 => true,
                        1 => a,
                        _ => b0,
                    })
                    .collect();
                let is_indicator = a && b0;
                let expect = on_schedule && is_indicator;
                assert_eq!(
                    check_ns_lower_bound_polys(nv, &gens, 2, &candidate),
                    expect,
                    "Count_3({n}): invariant candidate (a={a}, b0={b0}) valid iff on the Lucas \
                     schedule and the full indicator"
                );
            }
            // The support still carries a witness at every n — off schedule it must be non-invariant.
            let probe =
                ns_lower_bound_witness_polys_on_basis(nv, &gens, 2, &|m| count_is_disjoint(m, &edges));
            let w = probe.expect("the disjoint support carries a (possibly asymmetric) witness");
            assert!(check_ns_lower_bound_polys(nv, &gens, 2, &w), "the sub-basis witness re-checks");
            eprintln!(
                "Count_3({n}) at degree 2 (n mod 4 = {}): invariant closed form {}; support witness found",
                n % 4,
                if on_schedule { "VALID (the partial-partition indicator)" } else { "IMPOSSIBLE — witness is necessarily asymmetric" },
            );
        }
    }
}