Module census 

The small-n SAT-space census — the measurement instrument.

Brute-force over every minimal UNSAT formula (= every minimal subcube cover, the irreducible MUS atoms of the UNSAT universe) for a given n, one representative per hyperoctahedral (Bₙ) orbit, and attach to each orbit the full menu of invariants the solver stack can read off it: its symmetry group (orbit size + stabilizer), its face vector, its minimum resolution width, where it sits on the certified proof-complexity ladder (ProofRung / Shadow), and which engine the full structured router (crate::solve::solve_structured) actually decides it with.

The point is the audit: the certified diagnostic ladder (weakest_crushing_rung, diagnose) and the full router can disagree about a cover — e.g. the router crushes a mod-p germ with the polynomial GF(p) engine (crate::solve::Route::ModP) while the certified ladder, which has no mod-p rung, sees only a high-degree GF(2) Nullstellensatz. Every such disagreement is a concrete, located gap between what the solver can do and what the certified cascade can prove cheaply. The census enumerates them exhaustively at small n.

Structs

AglCollapse

The AGL collapse of the census — how far the affine group AGL(n,2) ⊋ Bₙ merges the Bₙ-orbit count. Because the certified family is AGL-invariant (proved), the AGL census carries the same family tower — just fewer classes: more symmetry, less to cover.

AglWitness

An auto-discovered affine equivalence between two Bₙ-orbit representatives: a concrete φ ∈ AGL(n,2) carrying one cover’s blocker set onto the other’s. The Bₙ census reports the two orbits as distinct classes; this witness proves they are the SAME unsatisfiable problem up to an affine coordinate change — the structure the signed-permutation lens could not see, made explicit and re-checkable. Codifying the collapse this way turns a merge count into concrete affine symmetries.

CoverageSummary

The hardness spectrum of the n-variable SAT hypercube — the durable “how much do we cover, and where is the hard core” map, aggregated from census. Each minimal-UNSAT family is placed on the certified proof-complexity ladder by its weakest crushing rung (the cheapest proof system that refutes it), and split by whether it carries Bₙ symmetry to break. The Nullstellensatz rung is further resolved by minimum degree — the algebraic-hardness dial — so the spectrum shows not just that the residue is algebraic but how deep it sits.

MenuSplit

The lens-menu split + morph clustering. A lean pass (per-orbit certified invariants only — no full router, no group closure — so it reaches n=4): which certified lens-class covers each orbit, and how many distinct structural signatures the orbits collapse to. A signature is (rung, shadow, min-res-width, face-vector) — the structural fingerprint. When distinct_signatures ≪ orbits, the vast orbit count is mostly morphs of a few structural types (the same family, mutated), exactly as one expects: symmetry already quotiented the exact symmetries, and the residual multiplicity is near-symmetric variation.

OrbitRecord

One Bₙ-orbit of minimal UNSAT formulas over n variables, with every invariant the solver can compute about it. The raw measurements; the audit flags (OrbitRecord::router_beats_ladder, OrbitRecord::finder_is_incomplete) are derived from them.

ResidueMap

The residue map — the honest “here’s what we crush, and here’s the wall” partition of the census. Every minimal-UNSAT family lands in exactly one of: crushed (a structural specialist route decided it — parity, mod-p, counting, a symmetry route, SoS, …), or the residue (routed to Incompressible/Cdcl — no lens caught it). Within those, targetable are the families still carrying unbroken symmetry (break more → crush cheaper), and rigid_core ⊆ residue are the families with no symmetry to break at all — the incompressible wall the counting bound predicts. This is a search with structure: not random probing, but a ranked pass of every lens over every family, surfacing exactly which ones resist and why.

StructureAccounting

Structure accounting — the answer to “how many minimal-UNSAT families have no structure, and how does cheap structure run out?” For each n: the cumulative number of orbits covered by a certified proof of degree ≤ d (covered_by_degree[d]), and the structureless count = orbits with no bounded certificate at all (rung = beyond-budget). The honest finding at n ≤ 4: structureless = 0 — every minimal-UNSAT cover is algebraically structured (degree ≤ n). Nothing at finite n is truly random; but the degree the structure requires grows with n (= n), so any fixed-degree (“cheap”) lens covers a shrinking fraction. That reconciles “no finite randomness” with the counting bound: structure always exists, but cheap structure runs out.

Functions

affine_composite_shear_generators

A bounded-composite affine-symmetry finder — climbing the “single-transvection wall” instead of declaring it. affine_transvection_generators only sees depth-1 shears (a single x_i ↦ x_i ⊕ x_j), so it is blind to symmetries realized only as a product of transvections — the parity/linear shears are the canonical example (“add x_j to x_i and x_k” preserves ⊕ x = b because it adds x_j to the form twice = 0; neither half does). This extends the finder to shears of composite depth ≤ max_targets: for every source j and every target set S ⊆ vars∖{j} with 1 ≤ |S| ≤ max_targets, the commuting product “add x_j to each x_i ∈ S”. At max_targets = 1 it is the transvection finder; at max_targets = 2 it catches the parity shears I earlier called out of reach. Polynomial for fixed depth (O(n^{max_targets+1}·|clauses|)), sound (every returned generator is verified to permute the clause set), and still incomplete only at unbounded depth — but the depth is now a tunable window, and the composite depth a formula’s symmetries require is itself a complexity measure. Returns each generator as (S, j).

affine_transvection_generators

A scalable, ∀n affine-symmetry finder — the transvection generators, in polynomial time. Exhaustive AGL(n,2) enumeration is stuck at n ≤ 4; this finds every transvection x_i ↦ x_i ⊕ x_j that is an affine automorphism of the clause set, in O(n² · |clauses|) time via [transvection_image_clause] — no 2ⁿ anywhere, so it runs at any n. Sound: every returned pair is a genuine automorphism (the produced clause set is checked equal to the original). Incomplete by design: an affine symmetry realized only by a composite of transvections (e.g. parity’s shears, products of two transvections) is not a single generator and is not returned — completeness for general formulas is a hard affine-equivalence problem, and the closed form (crate::affine::affine_subspace_agl_order) is the route for structured families.

agl_collapse_exact

The exact AGL collapse (n ≤ 3). Canonicalize every Bₙ-orbit representative under the full affine group in point-set space (affine_canonical_form); the number of distinct canonical forms is the exact AGL-class count. Brute over |AGL(n,2)| per orbit, so bounded to n ≤ 3.

agl_collapse_via_transvections

The AGL collapse via CNF-preserving affine moves — scales to n = 4. Since AGL = ⟨Bₙ, transvections⟩, uniting the Bₙ orbits connected by a single CNF-preserving transvection (its image stays a valid clause set, then Bₙ-canonicalized) merges genuine affine equivalences. The component count is an upper bound on the AGL-class count — every union is a real affine equivalence; only merges that must route through a non-CNF affine intermediate are missed — hence a rigorous lower bound on the collapse, exact when the walk is tight (checked against agl_collapse_exact at n = 3).

census

The Bₙ-orbit census of all minimal UNSAT formulas over n variables.

clause_agl_symmetries

The clause-level AGL symmetry detector — the affine analog of the Bₙ stabilizer, and the one symmetry lens that works on UNSAT formulas (the model-based detector is vacuous — no models). An affine map φ : x ↦ Ax ⊕ b (φ ∈ AGL(n,2)) is a clause-set automorphism iff, acting on 𝔽₂ⁿ, it permutes the falsifying-point sets of the clauses. Since Bₙ ⊆ AGL(n,2), |Aut_AGL| ≥ |Bₙ-stabilizer|; a Bₙ-rigid core with |Aut_AGL| > 1 has hidden affine symmetry (breakable by an affine SBP); |Aut_AGL| = 1 means it is affine-rigid — structure-minimal at the affine level too. Brute over AGL(n,2), feasible n ≤ 4.

coverage_summary

Aggregate the census into the CoverageSummary hardness spectrum.

extended_rung

The orbit’s ladder placement under the characteristic-extended cascade (weakest_crushing_rung_with_char), recomputed from the representative cover. The audit-gap closer: an orbit the router crushes via its mod-p specialist while the legacy ladder pays an algebraic price (OrbitRecord::router_beats_ladder) lands on its ModCount { p } rung here; every cover outside the mod-p population is placed exactly as the legacy ladder places it.

family_census

The family census across n — classify every minimal-UNSAT orbit into its certified family (lean: reaches n=4). This is the parametric handle on the infinite tower: the families are defined for all n, so recognizing membership (poly for the cheap families; n^d for the degree-d algebraic ones) covers the structured tower without enumerating it — the only way past the super-exponential orbit count.

family_growth

The family growth across n — for each n ≤ max_n: the number of distinct certified families, and which families are new (absent at n−1). The finding: the cheap families (unit-propagation, parity, counting) form a fixed menu that saturates early; from then on each increase in n forces exactly one new family — the degree-n algebraic family (algebraic-d{n}) — because max_ns_degree = n, so a degree-n certificate becomes necessary at n and was not at n−1. That is the forcing mechanism: the degree wall. The family count is therefore Θ(n) (fixed cheap menu + one algebraic rung per n), climbing forever — no finite family set covers all n (bounded-degree incompleteness).

family_of_types

Label ALL structural types. Every distinct signature (morph-class) at n, labeled with its family; returns (num_types, family → type-count) — so we see how the types (not orbits) distribute across the families. This is the full census of “what are the 403 types and where do they come from”: each is a low-degree named family, a bounded-algebraic one, or the generic full-degree core.

family_tower

The family tower — proven complete and finite at every n, without enumeration. The constructive Nullstellensatz completeness of crate::polycalc::build_ns_certificate (every UNSAT formula over n variables has a degree-≤ n GF(2) refutation, so nothing is beyond budget) pins the weakest crushing rung of every minimal-UNSAT formula to a FIXED, parametric set: the three cheap families (unit propagation, counting, parity) and the algebraic degrees d = 2..=n. No family lies outside this tower. So the complete list of families at scale n is produced in O(n) here — not read off the super-exponential orbit census. This is the “we do not iterate — we PROVED the families” statement, and family_census (which does enumerate) is always a subset of it. The size is Θ(n), climbing forever: no finite family set covers all n, because the degree wall forces a fresh algebraic-d{n} at each n.

find_agl_witness

Search AGL(n,2) for an affine map carrying from’s blocker set onto to’s — the witness that two Bₙ orbits are affine-equivalent, or None if they are genuinely affine-distinct. Exhaustive, so n ≤ 4.

generic_subfamilies

Peek inside the generic full-degree cores. They’re Bₙ-rigid and full-degree — but are they one undifferentiated blob, or do finer invariants split them into sub-families? Sub-classify the distinct generic full-degree types by their coarser invariants (shadow, min-res-width): returns (shadow, width) → number of distinct full-degree types. If a few buckets hold most of the types, the “generic” bucket has real sub-structure (more families); if they’re spread thin, it’s genuinely varied.

max_ns_degree_at

The degree-growth wall, measured. The deepest minimum-Nullstellensatz degree among the minimal-UNSAT families at n whose weakest certified refutation is algebraic (families caught by a cheaper lens — counting, parity — contribute nothing, correctly). This is a lean pass: only the certified proof-complexity ladder (weakest_crushing_rung) per orbit, none of the full router’s symmetry/algebraic machinery — so it reaches n=4 where the full census times out. As n grows this climbs (bounded-degree Nullstellensatz is incomplete — Tseitin/expander families force degree Ω(n)), so any fixed-degree lens is eventually outrun. That climb is the honest wall, not a fixed residue.

menu_split

Compute the MenuSplit for n (lean: reaches n=4).

named_giants

Name the giants. The top-k morph-classes at n (by orbit count), each labeled with the family it matches. Confirms which of the huge morph-classes are recognizable named families vs. the generic full-degree core.

realized_tower_families

The realization frontier at n — the lower-bound companion to family_tower. For each certified family that actually OCCURS among the minimal-UNSAT covers over n variables, one witness cover’s clauses. Where family_tower is the proven upper envelope (families ⊆ tower), this shows which rungs are realized at scale n, with a witness. A tower family absent here is simply not yet realized at this n — e.g. counting needs enough variables to host a pigeonhole, so it is empty at small n.

residue_map

Compute the ResidueMap: rank every lens over every family and partition by which resists.

structure_accounting

Compute StructureAccounting for n (lean: certified rung per orbit, reaches n=4).

symplectic_transvection_generators

The symplectic-transvection symmetry finder — one rung above affine shears. An affine shear is a rank-1 map whose right factor is a unit vector (v = e_j); dropping that restriction to a general v gives the full rank-1 group, whose bijective involutions are the symplectic transvections T_w = I ⊕ w wᵀ (even weight w). Where the affine dichotomy of §4 found permutation-symmetric families (PHP, mod-counting) to be affine-shear-rigid, this finder can still see their higher symmetry: it enumerates every even-weight w with 2 ≤ |w| ≤ max_weight and returns those whose T_w permutes the clause set (verified via [rank1_image_clause]). Cost O(Σ_{k≤W even} C(n,k) · |clauses|) — polynomial for fixed weight. Sound (every returned w is a checked automorphism); complete only up to the chosen weight. The weight of the smallest such symmetry is the graded invariant we track against NS degree.

witness_counting

A parametric UNSAT witness realizing the counting rung: the pigeonhole principle with pigeons pigeons and pigeons − 1 holes (crate::families::php). Resolution-exponential, invisible to GF(2) parity, closed only by a counting / Hall cut — so the weakest rung is ProofRung::Counting.

witness_parity

A parametric UNSAT witness realizing the parity rung at any n ≥ 3: the odd XOR triangle x₀⊕x₁ = 1, x₁⊕x₂ = 1, x₂⊕x₀ = 1 (their sum is 1 ≠ 0), encoded in CNF. No unit propagates and no counting cut sees it — only a GF(2) parity refutation closes it, so the weakest rung is ProofRung::Parity.

witness_unit_propagation

A parametric UNSAT witness realizing the unit-propagation rung at any n ≥ 1: a variable and its negation. Carving alone closes it, so its weakest crushing rung is ProofRung::Trivial.