gaugeOrbitMass_eq_mu
plain-language theorem explainer
On each relabeling class of a bounded complex, the counting-defined gauge-orbit mass equals the symmetry factor 1/|Aut|. Discrete-gravity and path-sum authors cite this as the derivation that turns pure gauge counting into the standard 1/|Aut| measure. The proof unfolds both sides and cancels orbit cardinality against the orbit-stabilizer factorization of pair count.
Claim. For every bounded complex $K$ in the universe of bound $B$, the gauge-orbit mass of the relabeling class of $K$ equals the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut}(K)|$. Explicitly, if the class mass is defined as (orbit cardinality)/(pair count), then that ratio on the class of $K$ is $1/|\mathrm{Aut}(K)|$.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$. Here that factor is derived from pure counting, without writing Aut into the mass definition.
Three counting quantities are in play. The gauge orbit card of $K$ is the number of labeled complexes equivalent to $K$ inside the bounded universe. 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 of a triangulation class is then orbit card over pair count: labeled copies per unit of gauge volume.
Upstream, orbit-stabilizer is already proved: relabeling witnesses form a torsor over Aut, so pair count factors as orbit card times $|\mathrm{Aut}|$. Representative independence lifts the counts to well-defined class functions on the quotient by the relabeling setoid.
proof idea
Tactic proof, short algebraic cancellation. First obtain that the real cast of the orbit card of $K$ is nonzero, from positivity of the orbit card. Unfold both the counting mass and $\mu$. Rewrite the class-level orbit and pair counts at the quotient image of $K$ back to the labeled quantities, then apply the factorization pairCount = orbitCard * |Aut|. After casting the product to reals, rearrange the quotient as a double division and cancel the nonzero orbit-card factor, leaving $1/|\mathrm{Aut}(K)|$.
why it matters
This is the module's central derivation theorem: given the pair-counting model premise, $1/|\mathrm{Aut}|$ is forced by orbit-stabilizer rather than inserted by hand. It feeds the existence half of the counting principle (gaugeOrbitMass multiplies back to orbit card), and with uniqueness of any mass satisfying that principle it pins the measure completely.
Downstream, the grounding theorem packages this equality with orbit-stabilizer and factorization as status-backed facts. The diagnostic path-sum identity rewrites the labeled $Z$ as an orbit-weighted class sum whose measure is entirely counting data. The MeasureSubstrate blocker uses the equality to show normalized gauge counting is equivalent to assigning $\mu$ on representatives, so no weaker unnamed condition hides in the counting statement.
In the broader RS gravity stack this closes the preflight step that legitimates the symmetry-factor measure before shell and gap arguments proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.