reasonTable_length
plain-language theorem explainer
The Gap-2 gauge-counting necessary-reasons census is a concrete list of exactly eighteen scored rows. Anyone packaging the composite certificate for that census cites this equality as the length guard. The proof is a one-line decidability check on the literal list.
Claim. The gauge-counting inevitable-reasons table (each row a status triple: identifier, claim gloss, and score among THEOREM / OPEN / MODEL / REFUTED) has length exactly $18$.
background
Gap-2 in the SevenGaps gravity program asks whether richer RecognitionLedger and posting-layer structure forces the Gauge Counting Principle for physical class mass (equivalently $\nu = 1/|\mathrm{Aut}|$). This module runs a necessary-reasons census: every candidate fact that would make that principle unavoidable is listed and scored THEOREM, OPEN, MODEL, or REFUTED.
The table is a finite List of status records. Sibling rows cover invariance underdetermining the path-sum measure, the equivalence of GCP with gauge-orbit mass, failure of uniform class mass, pinned-carrier complexity, uniqueness walls for invariant enrichments, label-asymmetric costs, orbit-stabilizer accounting, and the R18 fugacity-rebooking block (Boltzmann product preserved; no product-visible prior forces unit fugacity).
Upstream modules supply the individual scored facts (measure substrate blockers, gauge volume, gluing stationarity, size-blindness, ledger-site blindness). The length theorem only audits the census container, not those derivations.
proof idea
One-line decidability proof. The table is a closed concrete list literal; decide discharges list.length = 18 by computation on that finite value. No lemmas about individual reasons are invoked.
why it matters
Composite certificates in the SevenGaps audit chain guard on table length before conjoining scored rows. Downstream, labelInsertionDynamics_certified and insertionAsymmetryReasons_certified use the same length-guard pattern on their own censuses (9 and 17 rows); this declaration is the analogous guard for the gauge-counting census of eighteen reasons.
It anchors honesty bookkeeping from the module brief: THEOREM rows (invariance underdetermines; GCP iff gauge-orbit mass; uniform fails; uniqueness wall; R18 rebooking) stay separated from REFUTED derivation paths (invariant enrichment, equivariant posting cost, bare-posting gluing, size-blindness from cluster decomposition, label indifference as selector) and from the OPEN residual (action-first prior). Without a fixed length, a certificate could silently drop or duplicate a scored reason. It does not move the Gap-2 measure-derived flag; it only certifies census cardinality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.