gaugePreflight_grounded
plain-language theorem explainer
Packages four proved gauge-counting facts for bounded complexes of size B: orbit-stabilizer for relabeling witnesses, pair-count factorization, equality of the counting-defined orbit mass with mu = 1/|Aut|, and uniqueness of that mass among class functions. Cite when grounding the discrete-gravity symmetry factor from pure counting rather than postulating it. Term-mode conjunction of four prior lemmas.
Claim. For every bound $B\in\mathbb{N}$, the following hold simultaneously: (i) if bounded complexes $K,K'$ of size $B$ are equivalent, then the number of relabeling witnesses equals $|\mathrm{Aut}\,K|$; (ii) for every such $K$, the pair count equals orbit cardinality times $|\mathrm{Aut}\,K|$; (iii) the gauge-orbit mass of the triangulation class of $K$ equals $\mu(K)=1/|\mathrm{Aut}\,K|$; (iv) any class function $\nu$ with $\nu(c)\cdot\mathrm{pairCount}(c)=\mathrm{orbitCard}(c)$ equals the gauge-orbit mass on every class.
background
In the Seven Gaps gravity stack, PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. This module instead derives that factor from pure gauge counting on the finite universe of bounded complexes of size $B$.
Three counting quantities are primary. The gauge orbit card of $K$ is the number of labeled complexes equivalent to $K$. The pair count of $K$ is the number of pairs $(K',r)$ with $K'$ in that orbit and $r$ a concrete relabeling witness; its definition mentions only equivalence and relabelings. The gauge-orbit mass on a triangulation class is orbit card over pair count: labeled copies per unit of gauge volume, with no reference to $\mu$ or $\mathrm{Aut}$ in the definition.
The local setting is the honest status tier for the derivation: torsor/orbit-stabilizer, representative independence of the counts, the identity of counting mass with $\mu$, and uniqueness of the counting mass among class functions satisfying the pair-count relation.
proof idea
Term-mode four-tuple. The first conjunct is the pointwise application of the orbit-stabilizer lemma: for equivalent $K,K'$, relabeling witnesses form a torsor over $\mathrm{Aut},K$, so their cardinality equals $|\mathrm{Aut},K|$. The second is the global factorization lemma that pair count equals orbit card times automorphism order. The third is the derivation that the counting-defined gauge-orbit mass of the class of $K$ equals $\mu(K)$. The fourth is uniqueness: any real class function satisfying the counting identity $\nu(c)\cdot\mathrm{pairCount}(c)=\mathrm{orbitCard}(c)$ coincides with the gauge-orbit mass. No new argument; pure packaging of those four results.
why it matters
This is the grounding theorem of the ExactShellGaugePreflight module. It certifies that the four status flags (orbit-stabilizer, pair-count factorization, $\mathrm{gaugeOrbitMass}=\mu$, and uniqueness) are backed by actual proved theorems with zero sorry and no new axioms.
In the Recognition gravity path, the discrete path-sum measure needs a symmetry factor. PathSumMeasure takes $\mu=1/|\mathrm{Aut}|$ as a modeling choice; this package shows that choice is forced once gauge volume is identified with the (copy, witness) pair count. A per-labeled-copy volume principle would instead yield the quotient-uniform measure, so the modeling content is isolated cleanly.
Downstream consumers of the seven-gaps exact-shell analysis can cite a single grounded package rather than four separate lemmas when they need the counting origin of the $1/|\mathrm{Aut}|$ weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.