weight
plain-language theorem explainer
Defines the class-level weight on bounded triangulation classes used by the quotient-first path sum Zq. Gravity and Seven-Gaps authors cite it whenever a labeled path sum is rewritten as a sum over classes with the pushforward mass factor. It is a definitional packaging of wq, not an equality proof; the fiber-mass bridge lives in sibling lemmas.
Claim. The class weight $w_q$ on triangulation classes is the weight argument of the quotient-first path sum. With this weight, the standing labeled path sum (pulled back to classes) is the quotient sum weighted by the pushforward class mass $|\mathrm{fiber}\, q|\cdot\mu(\mathrm{out}\, q)$.
background
Seven Gaps Pillar 2 builds a quotient-first path-sum object after the P2c panel lock. The quotient sum is
$$Z_q(B,w_q)=\sum_{q:\mathrm{TriangulationClass},B}\frac{1}{|\mathrm{Aut}(\mathrm{out}, q)|},w_q(q),$$
with finiteness from scoped FiniteQuotient instances in ClassPushforward.
The standing labeled path sum is PathSumMeasure.Z. When the weight is class-constant, the honest bridge to the quotient is not bare $1/|\mathrm{Aut}|$ but the pushforward mass $|\mathrm{fiber}, q|\cdot\mu(\mathrm{out}, q)$. Upstream gauge-volume and fugacity modules treat class weight as label density (orbit size over sector relabeling count) and force unit-sector fugacity under size-blind representability. This module inherits the non-singleton fiber fact, so the fiber factor stays in the bridge.
proof idea
Definitional declaration (typeclass or abbrev-style weight package). No tactic proof and no sorry. Downstream equalities such as the labeled-sum identity and the fiber-excess decomposition apply this weight as the $w_q$ argument; the algebraic content lives in those siblings, not here.
why it matters
Anchors the P2c quotient-first object: every rewrite of labeled Z through Zq or fiberExcess threads this weight. Sibling identities (labeled sum equals fiber-card times mu times wq; Zq equals labeled Z iff fiber excess vanishes) are the honesty boundary the panel required: no unconditional identification of labeled Z with the pure $1/|\mathrm{Aut}|$ quotient sum.
In the broader RS gravity stack this is scaffolding for Gap-2 dynamics and gauge-volume bookkeeping, not a T0–T8 forcing step. No orbit-stabilizer for the full bounded TriangulationClass setoid is claimed; varying signatures block a single global relabeling action in this wave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.