Module orbit_stability 

Orbit stability: deciding symmetric Nullstellensatz questions at every scale by one finite computation. The machinery behind the ∀m lower-bound program.

A symmetric family (pigeonhole, modular counting) is one formula shape instantiated at every scale m, with the scale-m symmetric group acting on its variables. At a fixed degree d, the GF(2) NS dual question — does a degree-d pseudo-expectation exist? — restricted to invariant functionals collapses onto orbit types: an invariant L is constant on monomial orbits, an orbit is named scale-independently by its canonical structure (the bipartite pigeon/hole graph; the block-intersection hypergraph), and one constraint per joint (multiplier-orbit × generator) representative captures the whole system (collapsed_dual_system, soundness = the one-line invariance lemma tested in an_invariant_functional_checked_on_orbit_representatives_is_checked_on_all_generators).

The stability phenomenon: at fixed d the type set stabilizes once every ≤ d-edge structure is realizable, and the constraint rows’ entries are parities of counting polynomials in m (binomials — e.g. Count_3’s off-point constraint a + C(n−4, 2)·b₀), hence eventually periodic in m with period a power of two (Lucas). So the invariant-witness verdict is decidable for every m from finitely many evaluations — each in-window verdict differentially validated against the direct orbit-collapsed solver and, where a witness exists, lifted and re-checked by check_ns_lower_bound_polys with zero trust.

The honest boundary, forced by our own char-2 theorem (over_gf2_symmetrizing_a_proof_annihilates_when_the_group_is_even): over GF(2) there is no Reynolds averaging, so “no invariant witness” does not imply “no witness” — Count_3(8) realizes the gap (an asymmetric witness on the partial-partition support survives where every invariant candidate dies). Verdicts here are about invariant certificates; a positive verdict is a sound NS-degree > d lower bound, a negative one is measured against the gap.

Structs

CollapsedDual

The collapsed dual system at one scale: columns = canonical orbit types of the degree-≤ d basis, rows = the distinct type-vectors of the admitted NS generators m·g, taken over one multiplier per orbit × every generator (complete by the invariance lemma: the row of σ(m)·g equals the row of m·σ⁻¹(g), and the group permutes the generator set). An invariant functional L (one bit per type, L(∅-type) = 1) is a valid degree-d pseudo-expectation iff it annihilates every row.

FittedCount

An integer-valued polynomial in the scale, in the finite-difference (binomial) basis: value(m) = Σ_k diffs[k] · C(m − base, k). Fitted from consecutive window evaluations; the interpolation certificate is that the difference table vanishes beyond the allowed degree — every window point past the fitting prefix is an exact verification.

ForAllVerdict

The ∀-scales verdict: the stabilized system plus its per-residue answers and the in-window differential validation record.

StabilizedSystem

The stabilized symbolic system: the window-fitted entry polynomials, evaluable (mod 2) at every scale — the finite object that decides the invariant-witness question for all m.

SymmetricInstance

A symmetric family instantiated at one scale: the variable count, the GF(2) generator polynomials, the scale’s symmetry generators, the variable → atom-list map that names orbit types scale-independently, and one anchor per generator — the pseudo-structure that pins the generator’s identity for cross-scale row labeling (a pigeon row is anchored by its pigeon, a point generator by its point, a fixed-shape generator by its own monomial structure; anchor atom-lists carry the marker sort 255 so they never collide with multiplier variables, while their point atoms share the real sorts and relabel consistently with the multiplier’s).

Functions

canonical_structure

The canonical form of a structure: the lexicographically least relabeling, minimized over all sort-respecting point bijections (brute force over the touched points of each sort — bounded by the degree, so a handful of points). This is the scale-independent orbit-type name.

collapsed_dual_system

Build the CollapsedDual of an instance at degree d. The type column set comes from the bounded orbit quotient (one canonization per orbit); the rows from one multiplier representative per orbit against every generator, each product’s monomials bucketed by cached type.

count_instance_linear

Modular counting Count_q at scale n, linear encoding (Sₙ symmetry acting on the q-subsets): variable e is its block’s points — one sort. The symmetry generators are the adjacent point transpositions, induced onto the edge variables.

count_instance_linear_marked

Modular counting with one marked point — the point-stabilizer instrument. Point 0 gets its own sort, so the symmetry drops from Sₙ to Stab(0) ≅ Sₙ₋₁ (adjacent transpositions of the unmarked points only) and the canonical types automatically distinguish “touches the marked point.” The collapsed dual then decides existence of a marked-invariant witness — a strictly larger search space than the fully-invariant one (every Sₙ-invariant functional is Stab(0)-invariant), the first refinement rung between “symmetric” and “arbitrary” on the char-2 gap.

decide_invariant_witness_for_all_scales

Decide the invariant-witness question at every scale by one finite computation. Build the labeled entry counts at each window scale (consecutive scales, all post-onset so every label is realizable throughout), fit each entry as a degree-≤ max_count_degree integer polynomial (the finite-difference certificate — window points beyond the fitting prefix are exact verifications), read off the Lucas period, and solve the fitted system once per residue class. Every window scale is differentially validated: the fitted verdict must equal invariant_witness_exists_direct’s, and positive verdicts lift to check_ns_lower_bound_polys-passing witnesses. A true residue is a machine-decided NS-degree > degree lower bound for every scale in that class from onset on — including scales no explicit basis can represent.

invariant_witness_exists_direct

The direct orbit-collapsed solver — the independent validation path. No canonical types, no representative tricks: every admitted generator m·g (all multipliers) becomes a constraint, the unknowns are one bit per orbit (constancy imposed directly), plus L(1) = 1. Same mathematical question as collapsed_dual_system + CollapsedDual::solve, different code path — the two must agree at every scale, which is the machine check that representative completeness and type canonization are right.

labeled_dual_counts

The labeled dual entries at one scale: label → (column type → monomial count) — the raw integer counts before the mod-2 reduction, the objects that are polynomial in the scale.

monomial_orbits_bounded

Degree-bounded monomial orbits: the quotient of the degree-≤ d basis under the group, walked on the bounded basis (C(n, ≤d) monomials, never 2ⁿ) so it scales to num_vars ≤ 63 — the scale window polycalc::monomial_orbits’s cube filter cannot reach.

php_instance_clause

Pigeonhole at scale m, clause encoding (the crate::families::php layout, Sₘ × Sₘ₋₁ symmetry): variable p·holes + h is the atom pair (pigeon p, hole h) — two sorts. A pigeon clause (all-positive row) is anchored by its pigeon; a hole pair by its own structure.

php_instance_linear

Pigeonhole at scale m, linear encoding: each pigeon row as the degree-1 generator 1 + Σ_h x_{p,h} (never dropped by a degree budget — the fixed-degree questions stay real at every m), plus the hole at-most-one pairs. Same symmetry and atoms as the clause encoding; pigeon-row generators anchored by their pigeon.

php_instance_linear_marked_hole

Linear-encoded pigeonhole with one marked hole — the hole-stabilizer instrument (Sₘ × Stab(h₀) ≅ Sₘ × Sₘ₋₂). Hole 0 gets its own sort; pigeon symmetry is untouched.

php_instance_linear_marked_pigeon

Linear-encoded pigeonhole with one marked pigeon — the pigeon-stabilizer instrument (Stab(p₀) × Sₘ₋₁). Pigeon 0 gets its own sort; hole symmetry is untouched.

Type Aliases

RowLabel

A cross-scale row label: the canonical joint structure of multiplier ⊕ generator anchor. Two (multiplier, generator) pairs with the same label lie in the same joint orbit, so their entry counts must be identical — enforced fail-closed during collection.

Structure

A monomial’s structure: one atom list per variable it contains, each atom a (sort, point) pair — pigeonhole variables are [(0, pigeon), (1, hole)], counting variables are the block’s points [(0, a), (0, b), (0, c)]. Two monomials at any two scales have the same orbit type iff their structures agree up to a sort-respecting relabeling of points (canonical_structure).