Module hypercube

Expand description

The Boolean hypercube {0,1}ⁿ and its subcube cover — the geometric substrate beneath SAT, and the executable form of Pnp.lean’s HypercubeSAT (the Lean formalization lives at work/Pnp.lean).

Every clause of a CNF is a blocker: the set of corners (vertices) of the hypercube that falsify it. A clause of width w forbids exactly the 2^{n-w} corners that set each of its literals false — a subcube (a face) of codimension w. The whole formula is UNSAT precisely when its blockers cover the hypercube: every one of the 2ⁿ corners is forbidden by some clause, so no satisfying assignment escapes. SAT ⟺ some corner has energy zero — covered by no blocker. This is Pnp.lean’s Blocker / vertexEnergy / CoverUNSAT, made concrete.

The point of the representation: the problem (solutions = uncovered corners) and the rules (clauses = blockers) live in the same world {0,1}ⁿ. A clause is not a separate syntactic object; it is a region of the very space the solutions inhabit. So one group action — a CubeSym, Pnp.lean’s CubeSymmetry of coordinate permutations and per-coordinate flips — moves both: it permutes blockers among themselves and permutes corners among themselves, in lockstep. That is what lets us symmetry-break the rules and the solutions with a single move, and it is why the cover-totality question (UNSAT) collapses by the order of the symmetry group: a cover is total iff it covers one representative per orbit, not all 2ⁿ corners.

Pigeonhole is the canonical instance because we can always build one (php_cover): n pigeons into n-1 holes, with the full row×column symmetry group Sₙ × Sₙ₋₁ acting on the grid of variables. Here we build the stage, answer the first question — which corners are we blocking? — and then measure how far each stacked symmetry collapses the cover-check.

Structs§

AbstractRefutation: An abstract, scale-invariant refutation: the family’s rules symmetry-broken to their orbit types, plus the abstract invariant those types violate, plus the constant-size witness. For pigeonhole this is two rule-types (every pigeon takes a hole; no two share one) and the counting fact pigeons > holes — identical at every scale. This is the lift-and-shift-left: the proof’s true size is O(1) in the rule-types, reached by symmetry breaking the rules to their types, never by enumerating resolvents (the concrete and even the symmetric resolution closure both explode).
AdvanceStep: One step of the self-driving reduction: the lever applied, and the structure remaining after it.
CarveStats: Autocarve — recursive carving that lets the rules fall out. Carve the formula to its core, decompose into independent components, and for each: if a certified cut recognizes it, the rule falls out and the component closes; otherwise branch one variable and carve again on each branch. Every decision cascades fresh unit propagations and pure literals, exposing structure the previous level hid — so a buried, masked, or nested invariant surfaces on its own at the depth it becomes visible. UNSAT iff any component is, SAT iff all are; None past the budget. What an autocarve run did: how many recursion nodes it visited, how many times a certified cut fired (a “punch”), and how deep the carving recursed.
CollapseStep: One step of the collapse curve: how many orbits remain after stacking the first k generators.
Cover: A cover of the hypercube by clause-blockers — the geometric form of a CNF. UNSAT ⟺ the blockers leave no corner uncovered.
CubeSym: A hypercube symmetry: permute coordinates, then optionally flip each one (Pnp.lean’s CubeSymmetry). perm[j] is the coordinate that j’s value lands on; flip[j] negates it. These are the automorphisms that move blockers among blockers and corners among corners with the same action — the bridge that puts rules and solutions in one mathematical world.
Diagnosis: A complete auto-diagnosis of an instance: every structure-detector run at once, so you can read off the full menu of applicable symmetry-breaks and cuts — what you can still do to it.
FamilySignature: The abstract signature of a family: its rules symmetry-broken to their orbit types, and which certified shadow (if any) refutes it. This is the auto-collapse spread across families — the same machinery that found pigeonhole’s two-type counting abstraction, applied blind to any cover.
LadderStats: What a laddered branch-and-cut search did: how many subcubes (nodes) it visited, how deep it laddered, and how many subtrees a certified cut closed outright.
RuleSymmetry: The rule-symmetry signature of a cover: how the polynomially-many blockers collapse under the family’s automorphism group. rule_orbits is the count of essentially-distinct rules — a measure of structural complexity read off without enumerating the 2ⁿ corners. A small, scale-invariant rule_orbits is the geometric fingerprint of a family that admits a short symmetry-broken proof.
StructuralProfile: The structural profile of an instance — what every lever reveals about where its difficulty lives. quotient is the number of rule orbit-types under its discovered symmetry (how far the cube collapses); cut is the certified shadow that decides it, if any; core_clauses is what survives carving + bounded variable elimination (the irreducible residue). Together they place the instance on the spectrum from “all symmetry, O(1) quotient, instantly cut” to “no symmetry, full quotient, nothing reduces — the genuinely interesting core.”
Subcube: A subcube of {0,1}ⁿ: the coordinates set in care are fixed to the matching bits of value; the rest are free. As a blocker it is the footprint of one clause — the corners that falsify it. (Pnp.lean’s Blocker, generalized from clean 3-bit faces to any width.)

Enums§

AdvanceStatus: Where auto_advance ended: a decided verdict, or the structureless residue (the irreducible core no structural lever could touch — where you’d branch).
CarveOutcome: What carving the hypercube reduced a formula to.
CoverVerdict: The verdict of auto-cutting a cover: which certified cut showed it total (no corner escapes), or that a corner escapes (satisfiable), or that it is not a cover the prover decides.
ProofRung: Where an UNSAT instance sits in the proof-complexity landscape, as our certified cuts see it. This is a ladder of proof systems (Cook–Reckhow): each rung crushes families the cheaper ones are blind to. Counting and Parity are incomparable narrow detectors — pigeonhole needs counting and is invisible to GF(2); Tseitin needs GF(2) and is invisible to counting — while Nullstellensatz{min_degree} is the universal algebraic height over GF(2), complete at degree n. The honest face of the wall: an instance whose narrow cuts are silent and whose minimum NS degree is large sits at the top of this ladder, and the cost at that height is exponential. We can locate an instance on the ladder; we cannot prove the top rung is unavoidable for a family — that lower bound is exactly P vs NP, and it stays open.
SearchCost: The measured cost of a branch search: either it decided within the node budget, or the search blew past it (the exponential explosion, captured rather than hung).
Shadow: Which certified shadow refutes a cover — the abstract class of its hardness.

Functions§

abstract_signature: Symmetry-break any cover to its abstract signature: discover its automorphisms, quotient the rules to orbit-types (clause_orbits), and probe the certified shadows in turn — counting, then parity, then cutting-planes. shadow = None means no shadow recognizes it (it falls through to the general certified CDCL core). A maximally symmetric family collapses to a few rule-types decided by one shadow; an unstructured one spreads across many types with no shadow — but still has a backdoor.
applicable_levers: From a Diagnosis, the list of symmetry-breaks and cuts that apply — the menu of moves, in order of decisiveness. Empty global structure ⟹ the honest fallback: backdoor + branch on the residue.
apply_perm_to_model: Push a model through an automorphism: if σ preserves the clause set and m satisfies it, so does σ(m). Variable v’s value lands on σ(+v)’s variable, negated when σ(+v) is the negative literal — chosen so m ⊨ C ⟹ σ(m) ⊨ σ(C).
apply_renaming: Apply a flip-renaming x_v → ¬x_v for every v with flips[v] — a phase-flip symmetry of the cube. It permutes models bijectively (negate the flipped coordinates), so it preserves satisfiability.
auto_advance: Auto-diagnose, auto-break, auto-advance — to the fixpoint. Repeatedly diagnose the instance and apply the most decisive lever it offers: a certified cut decides it outright; otherwise carve (unit / pure-literal / subsumption) and bounded variable elimination peel it down; the loop advances until a verdict drops out or no structural lever reduces it further — the structureless residue, where the only remaining move is to branch. The returned trace shows the structure draining away step by step.
autocarve
autocarve_measured: Like autocarve, but also returns the CarveStats — node count, punch count, recursion depth.
automorphism_group_size: The order of a formula’s automorphism group — 1 means rigid (only the identity preserves it), the maximally asymmetric extreme. Discovers the generators and closes them under composition.
backdoor_branch_orbit_count: Symmetry breaking for speed. Count the orbits of the 2^{|U|} backdoor branches (assignments to U) under the generators that preserve U setwise. A symmetry-aware solver inspects one branch per orbit instead of all 2^{|U|} — fewer poly-time solves for the same verdict. Generators that move U off itself do not act on the branches and are skipped; each kept generator induces a permutation-with-flips on the backdoor positions.
blocker_orbit: The full orbit of a blocker under the group generated by generators (BFS over images). For a structured family this is polynomial-sized even though |G| is astronomical, because the blocker’s stabilizer is huge (a pigeonhole exclusion has orbit holes·C(pigeons,2), not |G|).
bounded_variable_elimination: Bounded variable elimination — carve away every dimension whose projection doesn’t grow the formula (resolvents ≤ clauses removed). Iterated to a fixpoint, it peels the cube down dimension by dimension wherever it’s free to do so; the variables that would explode (pigeonhole’s, by Haken) are left for the cuts. Satisfiability-preserving.
burnside_corner_orbits: Combinatorics — Burnside’s lemma. The number of corner orbits equals the average number of corners fixed by a group element: (1/|G|) Σ_g |Fix(g)|. A different invariant for the same count the orbit-BFS computes — counting by fixed points instead of by walking orbits. (n ≤ ~16.)
burnside_orbit_count: Burnside orbit count — the number of essentially-distinct witnesses. By Burnside’s lemma the number of orbits of a group action equals the average number of fixed points: #orbits = (1/|G|) · Σ_{g∈G} |Fix(g)|, where Fix(g) = { m : g·m = m }. Applied to the solution set (closed under the automorphisms, since every g is an automorphism), this counts the witnesses up to symmetry — the essential solutions — as a fixed-point average, never enumerating an orbit. The sum is exactly divisible by |G| (the lemma guarantees it); group must be the whole group (use perm_group_closure).
canonical_blocker: The orbit representative (canonical form) of a blocker under a generating set: the lexicographically minimal blocker reachable through the generators. Two blockers are symmetric iff they share a canonical form, so canonicalizing is how a symmetry-aware engine dedups derived rules by orbit.
canonical_cover: The Bₙ-canonical form of a cover, and its orbit size. Acts the group on the whole cover by g·C = { g.map_subcube(b) } and returns the lexicographically least sorted-blocker key together with the number of distinct covers in the orbit. The canonical key is constant on an orbit and distinct across orbits, a sound orbit invariant; the orbit size feeds the orbit–stabilizer identity |Stab| · orbit_size = |Bₙ|.
canonical_model: Symmetry-break the witness. The canonical (lexicographically least) model in a witness’s orbit under the automorphisms — the symmetry-broken representative. All witnesses in one orbit reduce to the same canonical witness, so the essential content of the solution set is one canonical witness per orbit; the symmetry regenerates the rest via model_orbit.
carve: Carve away the hypercube. Peel the formula down by the three classic simplifications, iterated to a fixpoint: unit propagation (a unit clause carves the cube in half by forcing a variable), pure-literal assignment (carves an autark section), and subsumption (drops a blocker contained in a stronger one). All three preserve satisfiability, so the result is either a verdict or the irreducible core that genuine hardness leaves behind. Pigeonhole carves to itself.
clause_orbits: Symmetry-break the rules at the clause level — the lift-and-shift-left form that scales to any number of variables. Partition the clause indices (the blockers) into orbits under a generating set of automorphisms, applying each Perm to clause literals directly via the canonical clause_key. A blocker is a clause, so this is the same rule-quotient as Cover::blocker_orbits — but with no 2ⁿ corner geometry and no 63-variable ceiling, so it runs at scales where the cube is astronomically large. The orbit count is the number of essentially-distinct rules. (Generators that move a clause off the set are simply not followed — only genuine rule-automorphisms close orbits.)
clauses_to_expr: Build the CNF ProofExpr over atoms x{var} from raw clauses — the door into the certified prover, scalable (no cube). None on an empty clause or empty formula.
collapse_curve: Stack the generators one at a time and record how the orbit count shrinks — the executable answer to “how much does each symmetry break cut the problem?” Begins at 2ⁿ (no symmetry) and descends as generators compose. The ratios are measured, not asserted.
components: Partition a formula into its independent components — maximal clause groups sharing no variable (the connected components of the variable-interaction graph). The formula is the conjunction of its components, so it is UNSAT iff any component is, and each can be attacked on its own. A structured UNSAT component buried in a big mixed formula — invisible to the monolithic cut — is laid bare here.
crush: The unified crush. Compose every lever into one decision procedure: carve the autark sections (pure literals), split into independent components, and decide each by the cut-enabled symmetry-aware search — a component refuted by a certified cut at the root closes in one node, the rest fall to bounded branch-and-cut. The formula is UNSAT iff any component is, SAT iff all are. Returns None only when a component blows past the budget — the genuinely hard residue, honestly surfaced rather than hidden.
cube_group_closure: The full group generated by generators, materialized (closure under composition) — the public door onto the otherwise-internal [group_closure]. For the small groups the census needs (Bₙ, n ≤ 5 ⇒ |G| = 3840) the orbit–stabilizer cross-checks sum over every element.
decide_2sat: Decide a width-≤2 CNF in polynomial time via the 2-SAT SCC solver. true = satisfiable. An empty clause forces UNSAT. Panics if handed a clause wider than 2 (not a 2-SAT instance).
decide_laddered: Ladder up the hypercube: crush what we can, brute-force the rest. Branch-and-cut over {0,1}ⁿ, one variable at a time — exactly DPLL with our certified cuts as the theory:
decide_laddered_nocut: The baseline the symmetry-pruned search is measured against: the same branch engine with no cut and no generators (so violates_lex_leader never fires). Isolates the effect of symmetry pruning.
decide_laddered_sym: Symmetry-break the search itself. The same branch-and-cut ladder, but it branches variables in index order and prunes a node whenever a root automorphism maps its decided prefix to a lexicographically smaller decided assignment — classic lex-leader symmetry breaking during search. Sound by construction: every orbit of assignments keeps exactly one lex-leader, and only strict non-leaders are pruned, so the verdict never changes; symmetric subtrees are simply skipped. The automorphisms are discovered once at the root.
decide_sat_via_2sat_backdoor: Decide satisfiability through a 2-SAT backdoor: the instance is satisfiable iff some fixing of U leaves a satisfiable 2-SAT residual. This solves in 2^{|U|} polynomial branches instead of a 2ⁿ search — the structure (the backdoor) turned an exponential into a small, easy fan-out. U must be a strong backdoor to 2-SAT (every residual width ≤ 2).
decompose_and_crush: Decompose into independent components and crush: return true (UNSAT) the moment any component is refuted by a certified cut, never having examined the rest. Isolating a structured UNSAT component unlocks a cut the monolithic formula hides.
diagnose: Run every lever’s detector and report what applies. The automated “what can we still do” — one call, the whole portfolio probed.
eliminate_variable: Carve out a dimension. Eliminate variable v by resolution (Davis–Putnam): drop every clause mentioning v, and add the non-tautological resolvents of each v-clause against each ¬v-clause. Geometrically this projects the cube’s v-axis away — the formula over n dimensions becomes an equisatisfiable one over n-1. Sound: a model of the projection lifts to a model of the original.
face_vector: Geometry — the f-vector. The number of blockers of each face dimension. A symmetry permutes blockers among themselves but preserves each one’s dimension, so the f-vector is a geometric invariant of the cover (the discrete analog of a polytope’s face counts).
find_random_core: Find the randomness. Strip every structural lever — a certified cut decides it (so there was no irreducible randomness), carve (unit/pure/subsumption) and bounded variable elimination peel structure away — and return what survives: the irreducible core. None means the instance was fully structured and got decided. Some(core) is the kernel where carving can do no more; check it with diagnose — if it also has no cut and ~zero symmetry-bits, that is the randomness, isolated.
greedy_2sat_backdoor: Greedily find a backdoor to 2-SAT: a set of variables U such that every clause has at most two literals outside U. Then under any assignment to U, each clause is either satisfied or shrinks to width ≤ 2, so the residual is 2-SAT — poly-decidable. Built by repeatedly fixing the variable that appears in the most still-too-wide clauses (a hitting set of the wide clauses).
hyperoctahedral_generators: Generators of the full hyperoctahedral group Bₙ = (ℤ/2)ⁿ ⋊ Sₙ — the signed permutations, the automorphism group of the n-cube and the complete clause-level symmetry: every CubeSym is one of its elements. The n−1 adjacent coordinate transpositions generate Sₙ; the single coordinate-0 flip, conjugated by those, generates the (ℤ/2)ⁿ of phase flips; together they generate all of Bₙ. The cube_group_closure of these has order exactly 2ⁿ·n! (1, 2, 8, 48, 384, 3840 for n = 0..=5). The census quotients minimal covers by this group.
is_antipodally_symmetric: Is the cover invariant under the antipodal map — global negation x → ¬x, the center-inversion of the cube? True iff flipping every literal of every clause maps the clause set onto itself. This is a symmetry axis distinct from coordinate permutation: it is the involution whose unique fixed point is the ½-center (CubeSym::map_fractional with all flips and no permutation fixes ½ⁿ). When it holds, satisfying assignments come in antipodal pairs {a, ¬a}, so one variable’s value is free WLOG.
is_strong_backdoor_to_2sat: Verify U is a strong backdoor to 2-SAT by enumeration: every one of the 2^{|U|} assignments to U yields a residual of width ≤ 2. Bounded to |U| ≤ 24 (the enumeration guard).
is_total_via_orbits: The symmetry-broken cover-totality check: when every generator is a verified automorphism, the cover is total iff it covers one representative per orbit. Same verdict as Cover::is_total, but it inspects orbit_count corners instead of 2ⁿ. None (fail-closed) when some generator is not actually an automorphism — never a guessed answer.
min_resolution_width: The minimum width of a resolution refutation of an UNSAT cover — the size of the widest clause any width-bounded refutation must carry, the classic resolution complexity measure (Ben-Sasson– Wigderson). A subcube is a clause (Subcube::clause_literals) and Subcube::resolve is the geometry of the resolution step; the empty subcube (care = 0, the whole cube blocked) is the derived contradiction. For width budget w we seed with the input blockers of support ≤ w and saturate under width-≤ w resolution; the least w that derives the empty subcube is the width. None only if the cover is satisfiable (no refutation at any width); every UNSAT cover succeeds by w = n since full-width resolution is complete. (For small covers — it enumerates resolvents.)
minimal_cover_orbits: Enumerate every minimal UNSAT cover of the n-cube, one canonical representative per Bₙ orbit. A minimal cover is a set of subcube blockers that covers every corner (UNSAT) and none of which is droppable (every blocker privately owns some corner) — i.e. a minimal unsatisfiable CNF (an MUS), the irreducible atom of the UNSAT universe. Branch on the lex-least uncovered corner: it lies in exactly 2ⁿ subcubes (one per support care ⊆ [n], with value = corner & care); recurse on each. Monotone pruning kills a branch the moment any chosen blocker becomes fully redundant (it can never recover a private corner once one is stolen). A leaf is total ∧ fully essential; leaves are folded to their canonical_cover key so each orbit is reported once. (Exhaustive; for small n.)
model_orbit: Symmetry generates solutions. From one model, the entire orbit under a generating set of automorphisms — every member a model too, produced with no search. The generative dual of resolution (which begets rules from symmetry); here symmetry begets solutions.
orbit_count: How many orbits the corners fall into under these generators.
orbit_representatives: Orbit partition of the 2ⁿ corners under a set of generators, each a verified automorphism. Returns one representative per orbit (the orbit-collapsed corner set the cover check needs). Materializes a 2ⁿ seen-bitmap, so this is itself bounded by the hypercube size — it measures the collapse rather than escaping it; the counting/parity shadows are what decide totality without the 2ⁿ walk. Honest by construction.
partition_into_orbits: Symmetry-aware solution counting. Partition a set of models into orbits under a generating set of automorphisms; each orbit is the full model_orbit of any of its members. The solution count is the sum of the orbit sizes, so a symmetric instance collapses to one representative per orbit — far fewer than the solutions themselves. (models should be closed under the symmetry, e.g. all models.)
perm_group_closure: The full symmetry group: every distinct Perm reachable by composing the generators (closure under composition). Small-group only — the orbit-stabilizer accounting below needs the whole group, not a generating set. Includes the identity.
php_cover: The pigeonhole cover: n pigeons into n-1 holes. Variable (p,h) (“pigeon p in hole h”) lives at index p*(n-1)+h, matching crate::families::php. Always buildable, always UNSAT.
php_perm_symmetries: The pigeonhole grid symmetry group Sₙ × Sₙ₋₁ as scalable Perms — adjacent pigeon (row) and hole (column) transpositions over the n*(n-1) grid variables. No u64 cap.
php_symmetries: The generating symmetries of the pigeonhole cover: adjacent transpositions of pigeons (rows) and of holes (columns). Together they generate the full grid symmetry group Sₙ × Sₙ₋₁ — pure coordinate permutations (no phase flips). Each is a CubeSym over the n*(n-1) grid variables.
pigeonhole_abstract_refutation: Symmetry-break pigeonhole to its abstract certificate. The rules collapse (via clause_orbits) to exactly two types regardless of n; the abstract invariant on those types is Hall’s condition, witnessed by the O(1) counting certificate pigeons > holes. The whole certificate is constant in size and identical in shape at every scale — the auto-collapse of pigeonhole, lifted to the type level where it actually scales. None only in the degenerate hole-free case.
pigeonhole_rule_symmetry: The rule-symmetry signature of pigeonhole at scale n, computed at the clause level with the full grid group Sₙ × Sₙ₋₁. The blocker set grows superlinearly and the cube has 2^{n(n-1)} corners, yet the rules always collapse to exactly two orbits — the complexity limit symmetry exposes, computable at any n because it never touches the cube.
pure_literal_reduce: Cut out the autark sections. A pure literal (a variable appearing in only one polarity) is the simplest autarky: assigning it satisfies every clause it touches, so that whole section of the cube is removed without affecting satisfiability. Iterate to a fixpoint and what remains is the hard core — the part with no free section to cut. Returns (core clauses, assigned pure literals). Sound: pure- literal elimination preserves satisfiability (Davis–Putnam).
renaming_to_horn: Recognize a new symmetry: renamable-Horn. Is there a flip-renaming under which every clause has at most one positive literal (Horn)? Horn-SAT is polynomial (unit propagation finds the least model), so a renamable-Horn formula is in a poly class our field cuts cannot see. Crucially, finding the renaming is itself a 2-SAT: a clause is Horn-after-flip iff no two of its literals are both positive, and “literal l is positive after flip” is the single f-literal (l.var, l.is_positive). Returns the flip-set, or None if no renaming makes it Horn.
restrict: The residual CNF after fixing variables: assignment[v] = Some(b) fixes v, None leaves it free. Clauses satisfied by a fixed literal are dropped; falsified literals are removed. An empty clause in the result means the restriction already falsifies the formula.
search_cost: Run the branch engine purely to measure its size, with use_cut selecting whether the certified cuts fire, and a hard budget on visited nodes so a resolution-class explosion is recorded as Exceeded instead of running forever. With the cut off this is raw DPLL (resolution-strength); with it on, the certified cut closes whole subtrees. The apples-to-apples gap between the two is the campaign’s thesis, quantified.
search_cost_antipodal: Recursive antipodal symmetry breaking. Branch search that, at every node, re-detects whether the residual is antipodally symmetric (is_antipodally_symmetric); when it is, it fixes the pivot to false WLOG and prunes the true branch — soundly, since the residual’s models come in antipodal pairs. A disjoint union of self-complementary blocks keeps regaining the symmetry as each block’s first variable is fixed, so the break fires recursively, collapsing one factor of 2 per block.
stabilizer: The stabilizer of a witness — the subgroup of symmetries that fix it (σ·m = m). These are the transformations under which the witness sees itself; they are exactly the redundancy in its perspective of the others.
structural_profile: Profile an instance: collapse its rules to orbit-types, probe which cut decides it, and carve it to its irreducible core. The reading that emerges — quotient size tracks cut-decidability tracks core reducibility — is the single axis underneath every lever: difficulty is quotient size.
symmetric_resolution_closure: Symmetric resolution closure on orbit representatives: resolve each representative against every image in another representative’s orbit. Since resolution commutes with symmetry — σ(resolve(c,d)) = resolve(σc,σd) — this captures every derivable rule up to symmetry without building the raw exponential closure. Returns the saturated count of orbit-types and whether the empty clause (a refutation) was derived, bounded by max_rounds and a max_reps size guard.
symmetric_resolution_growth: Symmetric resolution closure — rules beget rules, collapsed by symmetry. From a cover’s blockers, repeatedly resolve all pairs (each resolvent a new rule) and record, per round, both the raw count of distinct derived rules and the count of their orbit representatives under the automorphism group. The widening gap between the two is the symmetry collapse of the resolution proof: raw resolution explodes, but modulo symmetry only a handful of essentially-distinct rules are ever derived — the geometric reason symmetric proof systems refute pigeonhole in polynomial size where plain resolution cannot.
symmetry_entropy_bits: Information theory — the bits of symmetry. log₂|Aut| is the symmetry-entropy: the number of bits the automorphism group compresses out of the formula’s description (knowing one orbit representative plus the group recovers the rest). High for symmetric structure, exactly 0 for a rigid one — and that zero is the maximal-information, incompressible extreme.
walsh_hadamard_energy: Analysis — the Walsh–Hadamard (Fourier) spectrum. Expand the cover’s vertex-energy function over the cube’s characters χ_S(x) = (-1)^{⟨S,x⟩}: f̂(S) = 2⁻ⁿ Σ_x energy(x) χ_S(x). Harmonic analysis on the hypercube — the coefficients are the analytic invariant. (n ≤ ~16.)
weakest_crushing_rung: Locate an instance on the ProofRung ladder: the weakest certified cut that crushes it, probed cheapest-first (carve ≺ counting ≺ parity ≺ Nullstellensatz-by-degree). The narrow rungs (Counting, Parity) are incomparable; probe order only decides the label when more than one happens to fire.
weakest_crushing_rung_with_char: weakest_crushing_rung with the characteristic rungs enabled — the same cascade, plus, between the parity probe and the algebraic ascent, a certified mod-p cut per prime in primes: when the CNF is a recognized one-hot encoding of a GF(p) linear system (crate::modp::recover_from_cnf, which declines rather than guesses) and the GF(p) Gaussian refutation re-checks (crate::modp::is_refutation), the instance lands on ProofRung::ModCount. This is the ladder rung the census’s router_beats_ladder audit flagged as missing: the structured router’s Route::ModP specialist finally has a certified proof system the ladder can name. With primes = &[] the cascade is exactly the legacy one.
witness_perspective: Symmetry-break across the witness’s perspective of the other witnesses. From witness m, every other witness in its orbit is reached by some symmetry — but many symmetries land on the same one (they differ by a stabilizer element of m). The symmetry-broken perspective quotients that redundancy out: exactly one representative transformation per distinct witness m can see — a transversal of the coset space G / Stab(m). The returned (witness, σ) pairs satisfy σ·m = witness, and their count is |G| / |Stab(m)| = |orbit(m)| (orbit–stabilizer). The first entry is (m, identity): the witness’s view of itself.

Type Aliases§

Corner: A corner (vertex) of the hypercube {0,1}ⁿ: bit v holds the value of variable v. Enumeration routines assume n ≤ 63; the algebra itself is width-agnostic.