gaugeCountingMass_unique
plain-language theorem explainer
Any real-valued mass on triangulation classes that obeys the normalized gauge-counting identity (mass times pair-count equals orbit cardinality) is forced to equal the counting-defined gauge orbit mass. Discrete-gravity and path-sum authors cite this to pin the measure uniquely once the counting principle is fixed. The proof is a short algebraic uniqueness argument: positivity of the pair count turns the identity into the defining quotient.
Claim. Let $\nu$ assign a real mass to each triangulation class $c$. If $\nu(c)\cdot |\mathrm{pairs}(c)| = |\mathrm{orbit}(c)|$ for every class $c$, then $\nu(c)$ equals the gauge orbit mass $|\mathrm{orbit}(c)|/|\mathrm{pairs}(c)|$.
background
This module derives the standard discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it. Two class-level counting quantities are primary: the orbit cardinality (number of labeled complexes equivalent to a representative) and the pair count (number of pairs consisting of an orbit member and a concrete relabeling witness). Both are well-defined on the quotient of bounded complexes by the relabeling equivalence.
The gauge orbit mass of a class is defined solely as the ratio of those two counts: labeled copies per unit of gauge volume. It never mentions $\mu$ or automorphism groups in its definition. The module already proves that this mass satisfies the normalized counting identity mass times pair-count equals orbit card, and (via orbit-stabilizer) that it equals $1/|\mathrm{Aut}|$ on representatives.
Uniqueness is the remaining half of the existence-uniqueness package: any other class mass obeying the same linear counting identity must coincide with that ratio.
proof idea
Fix a class $c$. Pair-count positivity (pairCountClass_pos) gives that the real cast of the pair count is nonzero. Unfold the definition of gauge orbit mass (orbit card over pair count). Rewrite the desired equality via eq_div_iff using that nonzero denominator; the resulting product identity is exactly the hypothesis at $c$.
why it matters
Together with the existence identity that gauge orbit mass itself multiplies pair-count back to orbit card, this theorem closes uniqueness for the counting-defined measure. Downstream, gaugeCountingPrinciple_iff_eq_gaugeOrbitMass packages existence and uniqueness as a single equivalence: a mass satisfies the gauge counting principle if and only if it equals gauge orbit mass.
It is also cited by the grounding theorem gaugePreflight_grounded, which certifies that the module's status flags rest on actual proofs (orbit-stabilizer, pair-count factorization, derivation of $\mu$, and uniqueness). The companion derivation gaugeOrbitMass_eq_mu then identifies the unique counting mass with the classical $1/|\mathrm{Aut}|$ factor used by PathSumMeasure.
In the Seven Gaps gravity program this is the preflight step that justifies inserting the symmetry factor into path sums without smuggling automorphism data into the measure's definition: the measure is forced by gauge volume counting alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.