GaugeCountingPrinciple
plain-language theorem explainer
Normalized gauge counting is the Prop that a class mass times its gauge-witness pair count equals the labeled orbit cardinality. Anyone working the Gap-2 path-sum measure derivation cites it as the exact undischarged MODEL premise. The body is a one-line universal equality over triangulation classes; no proof content beyond the definition.
Claim. For a fixed bound $B\in\mathbb{N}$ and a real-valued mass $\nu$ on triangulation classes of size at most $B$, the normalized gauge-counting principle holds when, for every class $c$, $\nu(c)\cdot N_{\mathrm{pair}}(c)=N_{\mathrm{orbit}}(c)$, where $N_{\mathrm{pair}}(c)$ is the gauge-witness volume of $c$ and $N_{\mathrm{orbit}}(c)$ is the labeled orbit size of $c$.
background
The module sits in the Gap-2 path-sum measure story. MeasureInvarianceNoGo already shows that relabeling invariance, positivity, and normalization alone do not pick a unique path-sum measure. ExactShellGaugePreflight shows that the gauge-counting mass equals $1/|\mathrm{Aut}|$ and records normalized gauge counting as a MODEL premise rather than a derived law.
A triangulation class is an orbit of bounded complexes under relabeling. The orbit cardinality $N_{\mathrm{orbit}}(c)$ is the number of labeled copies in the class; the pair count $N_{\mathrm{pair}}(c)$ is the gauge volume (labeled copy paired with a relabeling witness). Both are lifted from representatives via the quotient, so they are class-well-defined.
The local task is to name the missing premise exactly: class mass times gauge-witness volume equals labeled orbit size. That is the substrate blocker this definition packages.
proof idea
Definition only: the Prop is the universal statement that for every triangulation class $c$, the product of the real mass $\nu(c)$ with the realified pair-count equals the realified orbit cardinality. No tactics, no lemmas applied at the definition site. Downstream equivalences (to $1/|\mathrm{Aut}|$ mass, to label density, to unit fugacity) live in sibling and Gap2GaugeVolume theorems.
why it matters
This is the named residual for the measure half of Gap-2. FullTheoryLedger's gap2_measure_selection_blocker_certified certifies the measure pillar open at exactly this premise: gauge-orbit mass satisfies it, while the quotient-uniform decoy fails on a concrete two-point class. The residual DAG packages the same pair as TypedResidual R1.
Gap2GaugeVolume uses the Prop as the hinge of several equivalences: it holds for a class mass iff the mass equals label density on representatives; for sector-fugacity weights iff every occupied sector has fugacity one; and the Gibbs weight induces the RS path-sum measure precisely because its class mass satisfies the principle (hence equals $1/|\mathrm{Aut}|$). Gluing and invariant-weight routes are likewise phrased as "gives gauge counting."
In the Recognition gravity ledger this isolates what invariance axioms cannot supply: a derivation of normalized gauge counting from richer substrate structure. Continuum-limit Gap-2 remains a separate open half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.