Zq
plain-language theorem explainer
Quotient-first path sum over triangulation classes: each class contributes its representative symmetry factor times a class weight. Gravity and Seven Gaps authors cite it as the P2c-promoted object, distinct from the standing labeled path sum. The definition is the finite sum of μ(out q)·w(q) over the class quotient.
Claim. For a bound $B\in\mathbb{N}$ and a weight $w$ on triangulation classes of bound $B$, the quotient-first path sum is $Z^{\mathrm{q}}(B,w)=\sum_{q}\mu(\mathrm{out}\,q)\,w(q)$, where the sum runs over classes and $\mu$ is the per-representative symmetry factor $1/|\mathrm{Aut}|$ evaluated on a chosen representative of $q$.
background
Pillar 2 of the Seven Gaps program isolates the path-sum measure on bounded triangulation data. The standing labeled object sums over individual complexes; the P2c panel instead promotes a quotient-first sum over triangulation classes, weighting each class by the symmetry factor of a chosen representative.
Here a triangulation class is an equivalence class of bounded complexes under the relabeling setoid. The measure $\mu$ on a representative is the classical $1/|\mathrm{Aut}|$ factor imported from the path-sum measure layer. The quotient is finite by the scoped finite-quotient instances from the class-pushforward module, so the sum is well-defined as a complex number.
The module is explicit that this is not an unconditional rewrite of the labeled path sum: non-singleton fibers exist, and the difference is tracked by an explicit fiber-excess term rather than erased by convention.
proof idea
Pure definition: the value is the finite sum, over all triangulation classes $q$ of bound $B$, of the complexified symmetry factor $\mu(\mathrm{out},q)$ times the supplied class weight $w(q)$. No lemmas are applied; classical choice enters only through Quotient.out and the finite-quotient instance that makes the sum legal.
why it matters
This is the canonical quotient-first object for Gap 2 measure work. Downstream, the labeled-weight bridge proves the Gibbs-weighted labeled sum equals this quotient sum with no fiber factor (gibbsZ_eq_Zq, gibbs_fiberExcess_vanishes), while the plain $\mu$-weighted labeled sum agrees only under trivial orbits (muZ_eq_Zq_of_trivial_orbits). The exact mismatch identity labeledZ = Zq + fiberExcess is stated in this module and used to keep the honesty boundary honest.
Cap-shell reindexing uses it as the target of phased finite-sum transport (phasedZq_eq_exactComplexityCutoff). The full-theory ledger cites the surrounding measure-selection blocker: normalized gauge counting is equivalent to $1/|\mathrm{Aut}|$, and a quotient-uniform decoy fails on a concrete two-point class, so richer substrate structure is still required. No orbit-stabilizer theorem for the full bounded carrier is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.