IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ
Defines the quotient-first path sum Z_q over triangulation classes, evaluating the symmetry-factor measure on a chosen representative of each class. Gravity and path-sum workers cite it when comparing the quotient convention to the labeled PathSumMeasure.Z. The module packages the class-sum definition, fiber-excess identities relating Z_q to the labeled sum, and a grounded status tag.
claimLet triangulation configurations be quotiented by the relevant symmetry into classes $[c]$. The quotient-first path sum is $Z_q = \sum_{[c]} \mu(\mathrm{rep}([c]))$, where $\mu$ is the per-class symmetry-factor measure on a chosen representative. Relative to the labeled path sum $Z_{\mathrm{lab}}$, one has $Z_{\mathrm{lab}} = Z_q + E_{\mathrm{fiber}}$, with $E_{\mathrm{fiber}}$ the fiber-excess; equality $Z_q = Z_{\mathrm{lab}}$ holds precisely when every fiber is a singleton (or excess vanishes).
background
Seven Gaps Crux-2 treats the path-sum side of the gravity ledger under the locked QUOTIENT_BOOKKEEPING protocol. The upstream ClassPushforward module supplies the finite-quotient fiberwise sum and the pushforward of the labeled measure onto triangulation classes.
The standing labeled object is PathSumMeasure.Z, which sums over labeled configurations. The quotient convention instead sums once per class, inserting the symmetry factor only on a representative. That is the object introduced here as $Z_q$ (Lean Zq), together with the weight on classes and the comparison identities to the labeled sum.
Fiber cardinality enters through a fiber-excess term: the labeled sum equals the class sum plus a nonnegative excess that vanishes exactly on singleton fibers. Status is recorded by an explicit grounded tag so downstream lanes can cite a single source of truth for the convention.
proof idea
Definition-and-identity module, not a single deep theorem. Zq is the class sum of the representative measure. Equality of outgoing measures on equal class marks is a congruence lemma. The labeled sum is rewritten as a fiberwise sum of fiber cardinality times class measure, then split as $Z_q$ plus fiber excess. Biconditional and singleton-fiber corollaries are immediate rearrangements. A small inductive status record marks the construction as grounded under the quotient-bookkeeping protocol.
why it matters in Recognition Science
Feeds Lane D3 phase structure: ZqPhaseStructure imports this module and equips QuotientFirstZ.Zq with an explicit oscillatory phase model, proving structure theorems at fixed complexity cap (continuum limit left open). Without a single quotient-first object and the fiber-excess dictionary to the labeled Z, phase and continuum arguments would mix conventions.
In the Seven Gaps gravity stack this is the bookkeeping hinge between Crux-2 class pushforward and later quotient-native analysis. It does not itself close continuum or dynamical claims; it fixes the measure convention those claims must use.
scope and limits
- Does not define or alter the labeled PathSumMeasure.Z; only compares to it.
- Does not prove continuum limits or dynamical gravity equations.
- Does not choose a canonical representative beyond congruence of the measure.
- Does not supply the oscillatory phase model (that lives in ZqPhaseStructure).
- Does not claim fiber excess vanishes in generic triangulations.
used by (1)
depends on (1)
declarations in this module (11)
-
def
Zq -
theorem
mu_out_eq_of_mk_eq -
class
weight -
theorem
labeledZ_eq_sum_fiberCard_mul_mu -
def
fiberExcess -
theorem
labeledZ_eq_Zq_plus_fiberExcess -
theorem
Zq_eq_labeledZ_iff_fiberExcess_vanishes -
theorem
Zq_eq_labeledZ_of_singleton_fibers -
structure
QuotientFirstStatus -
def
quotientFirstStatus -
theorem
quotientFirstStatus_grounded