gaugeOrbitMass_satisfies
plain-language theorem explainer
The counting-defined gauge-orbit mass on triangulation classes obeys normalized gauge counting: class mass times gauge-witness pair volume equals labeled orbit size. Continuum-measure residual and Gap-2 status work cite this as the positive half of the substrate blocker package. The proof is a one-line application of the ExactShellGaugePreflight multiplication identity.
Claim. For every natural number $B$ and every triangulation class $c$ at size parameter $B$, the counting-defined gauge-orbit mass $\nu$ satisfies $\nu(c)\cdot N_{\mathrm{pair}}(c)=N_{\mathrm{orbit}}(c)$, where $N_{\mathrm{pair}}(c)$ is the number of (labeled copy, relabeling witness) pairs on $c$ and $N_{\mathrm{orbit}}(c)$ is the labeled orbit cardinality of $c$.
background
This module sits in the SevenGaps gravity stack on path-sum measures. MeasureInvarianceNoGo shows that relabeling invariance, positivity, and normalization alone do not pick a unique path-sum measure. ExactShellGaugePreflight constructs the counting mass equal to $1/|\mathrm{Aut}|$ on each triangulation class and records normalized gauge counting as an extra model premise, not a consequence of those axioms.
Normalized gauge counting is the proposition that a class mass $\nu$ multiplies the gauge-witness pair count back to the labeled orbit size: $\nu(c)\cdot N_{\mathrm{pair}}(c)=N_{\mathrm{orbit}}(c)$ for every class $c$. The module's main equivalence later says this holds for all classes if and only if $\nu$ is exactly the $1/|\mathrm{Aut}|$ counting mass. The present theorem is the positive direction for that counting mass.
The local setting is a certified substrate blocker: invariance axioms and uniform quotient renaming cannot discharge the remaining measure task; a richer ledger derivation of gauge counting is still required.
proof idea
One-line term proof: the goal is definitionally the statement of the preflight lemma that multiplies gauge-orbit mass by pair count and recovers orbit cardinality. No extra rewriting or case split is needed; the theorem is that preflight identity re-exported under the named principle.
why it matters
This is the positive half of the measure-side substrate blocker. Downstream, the typed residual packages it with the failure of the quotient-uniform decoy: normalized gauge counting holds for the counting mass and fails for uniform class mass. The inevitable-reasons ledger records it as R03.
Gap-2 status binding uses it as the defect certificate for history-based discharge: the advertised history derivation rewrites to this prior theorem plus an identification of the history construction with the counting mass, without posting, dual-entry, or enrichment. Parameter-inertness of history measures follows from uniqueness of the gauge-counting solution once this fact is in hand.
In the Recognition gravity stack this pins why continuum path-sum selection cannot close from invariance alone: the missing principle is exactly this orbit-stabilizer accounting, and the counting mass is its unique solution. The module flips no FullTheoryLedger flag; it certifies the open substrate task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.