gaugeCountingPrinciple_iff_mu_on_representatives
plain-language theorem explainer
Normalized gauge counting on triangulation classes is exactly the assignment of mass $1/|\mathrm{Aut}\,K|$ to every represented bounded complex. Anyone closing Gap-2 path-sum measure derivation cites this as the precise substrate premise, not a weaker invariance axiom. The proof is a short two-way rewrite through the orbit-mass characterization plus the preflight identity that orbit mass equals $\mu$.
Claim. For any bound $B$ and any real-valued mass $\nu$ on triangulation classes of bound $B$, the gauge-counting principle (class mass times gauge-witness volume equals labeled orbit size) holds if and only if for every bounded complex $K$, the mass of the relabeling class of $K$ equals $\mu(K)=1/|\mathrm{Aut}\,K|$.
background
The module sits in the Gap-2 path-sum measure program. Prior work shows that relabeling invariance, positivity, and normalization alone do not force a unique class mass (MeasureInvarianceNoGo). Separately, ExactShellGaugePreflight shows that the counting-defined gauge-orbit mass equals $\mu(K)=1/|\mathrm{Aut},K|$ and records normalized gauge counting as a MODEL premise rather than a theorem.
GaugeCountingPrinciple is that premise stated without naming Aut: for every class $c$, $\nu(c)\cdot\mathrm{pairCountClass}(c)=\mathrm{orbitCardClass}(c)$. Classes are the quotient of bounded complexes by the relabeling setoid. The live decoy is the uniform class mass on the quotient, which satisfies weaker invariance but fails this counting identity on a two-point class.
The local goal is exact identification: the counting principle holds precisely when every represented complex receives mass $\mu$, so the remaining substrate task cannot be discharged by renaming uniform quotient counting.
proof idea
Term-mode, two directions after one rewrite. First rewrite the left-hand side via the sibling equivalence that gauge counting holds iff $\nu$ equals the counting-defined gauge-orbit mass on every class.
Forward: assume $\nu$ equals gauge-orbit mass; for each complex $K$, substitute and apply the preflight identity gaugeOrbitMass_eq_mu, which states that the orbit mass of $K$ is $\mu(K)$.
Reverse: assume $\nu$ of the class of $K$ equals $\mu(K)$ for all $K$. Extensionality on classes, then Quotient.inductionOn, reduces to representatives; chain the hypothesis with the symmetric preflight identity to recover equality with gauge-orbit mass, hence gauge counting.
why it matters
This is the certified substrate blocker for Gap-2 measure derivation. Downstream closing theorems in Gap2MeasureDerivation apply it as the bridge from Aut-free constructions to the counting principle: gap2_gauge_counting_gibbsWeight and gap2_gauge_counting_from_surface_and_kindTotals both conclude gauge counting by the reverse direction after proving class mass equals $\mu$ via erasure/C4. classMass_gibbs_eq_mu_via_erasure supplies that Aut-free equality.
gaugeCounting_iff_labelIndifference rewrites the same premise into label-density language without Aut or witnesses. Hostile probes such as no_siteSymmetry_measure and closing_via_blocker_iff use it to kill candidate measures that factor through ledger site-symmetry counts. The module doc is explicit: the remaining task requires deriving normalized gauge counting from richer ledger structure; this file flips no FullTheoryLedger flag and only pins the exact missing principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.