labeledZ_eq_orbitWeighted_classSum
plain-language theorem explainer
For any relabeling-invariant complex weight, the labeled path sum Z (with the discrete-gravity 1/|Aut| measure) equals a sum over triangulation classes of orbit size times counting-derived gauge mass times the weight of a representative. Gravity and discrete-path-sum workers cite it when replacing labeled sums by class sums without inserting Aut by hand. The proof is a fiberwise Fintype sum over the relabeling quotient, using constancy of the summand on each orbit and the already-proved identification of gauge mass with 1/|Aut|.
Claim. Fix a bound $B\in\mathbb{N}$ and a weight $w$ on bounded complexes that is constant on relabeling-equivalence classes. Then the labeled path sum $Z(B,w)$ equals $\sum_c |\mathrm{orbit}(c)|\,\nu(c)\,w(\mathrm{rep}\,c)$, where the sum runs over triangulation classes $c$, $|\mathrm{orbit}(c)|$ is the number of labeled copies in the class, $\nu(c)$ is the counting-derived gauge mass of the class, and $\mathrm{rep}\,c$ is any chosen representative.
background
This module sits in the Seven Gaps gauge-preflight layer for discrete gravity. Upstream, PathSumMeasure postulates the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ on labeled complexes. Here that factor is derived from pure counting: the gauge orbit card is the number of labeled complexes equivalent to $K$; the pair count is the number of pairs (copy, concrete relabeling witness); the class mass $\nu(c)$ is orbit card over pair count on the quotient of triangulation classes. By orbit-stabilizer, pair count factors as orbit size times $|\mathrm{Aut}|$, so $\nu$ recovers $1/|\mathrm{Aut}|$.
The labeled path sum $Z(B,w)$ is the sum over all bounded complexes of $\mu(K),w(K)$. Relabeling equivalence generates the setoid whose quotient is the type of triangulation classes. The hypothesis on $w$ is invariance under that equivalence, so $w$ descends to classes. Upstream results already show the counting mass is a class function and equals $\mu$ on any representative (gaugeOrbitMass_eq_mu).
proof idea
Unfold $Z$, then rewrite the labeled sum as a fiberwise sum over fibers of the quotient map to triangulation classes (Fintype.sum_fiberwise). On each fiber over class $c$, every labeled complex is equivalent to the chosen representative Quotient.out c, so invariance of $w$ and the class-function property of $\mu$ make the summand constant (via summand_class_constant). The fiber therefore contributes cardinality times $\mu(\mathrm{rep}),w(\mathrm{rep})$. Identify fiber cardinality with orbitCardClass c by a subtype equivalence to the orbit of the representative, and replace $\mu(\mathrm{rep})$ by gaugeOrbitMass c using gaugeOrbitMass_eq_mu. Reassociate to obtain the stated class sum.
why it matters
This is the diagnostic bridge that moves the discrete-gravity path sum from a labeled sum carrying an inserted $1/|\mathrm{Aut}|$ measure to a pure class sum whose weights are counting data (orbit size and gauge mass). It closes the preflight claim that "the measure in $Z$ is now carried entirely by counting data," after the module has already proved torsor/orbit-stabilizer factorization and gaugeOrbitMass_eq_mu. In the Recognition gravity stack this legitimates working on triangulation classes without smuggling automorphism orders into the measure by hand. No downstream consumers are wired yet in the graph; the immediate role is internal to the Seven Gaps gauge-preflight ledger (T7 status block), grounding the true flags that the counting-derived mass is the symmetry factor used by $Z$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.