IndisputableMonolith.Gravity.SevenGaps.ClassPushforward
Defines the class-pushforward bookkeeping for the Seven Gaps path-sum: labeled fibers of quotient classes, fiber cardinality, and class mass as fiber size times the measure weight. Equates the configuration sum Z to a sum over triangulation classes of class masses. Gravity and quotient-first Z constructions import it to separate labeled configurations from orbit classes under Aut.
claimFor a quotient map $\pi:\alpha\to Q$, the labeled fiber of a class $q\in Q$ is $\{a\in\alpha:\pi(a)=q\}$. Fiber cardinality and class mass satisfy $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot\mu(q)$. The path-sum $Z$ equals the pushforward sum $\sum_q\mathrm{classMass}(q)$, and likewise for the RS path-sum $Z_{\mathrm{RS}}$.
background
Seven Gaps Lane 2 builds a proved path-sum measure $Z_{\mathrm{RS}}$ on a scoped finite configuration class BoundedComplex B (Fintype via an explicit coding equivalence). Configurations carry bounded incidence data; the measure is a weighted sum over those labeled objects.
When one passes to triangulation classes (orbits under automorphism), the same total must be rewritten as a sum over classes. This module supplies the elementary fiberwise dictionary: the preimage of a class under the quotient map, its cardinality, and the class mass (cardinality times the weight of a representative). Decidability of membership is classical noncomputable bookkeeping, not an algorithmic claim.
The setting is pure finite-sum reindexing. No continuum limit or physical mass formula is invoked here; the objects are combinatorial weights on a finite type.
proof idea
Definition-and-lemma module, not a single deep theorem. Fibers and membership are set-comprehension defs. Fiber cardinality is the Fintype card of the fiber. Class mass is defined as that card times the measure weight $\mu$.
The main identities are finite-sum rewrites: a sum over labeled configurations equals the sum over quotient classes of the fiberwise inner sums; when the weight is constant on fibers this collapses to $\sum_q |\mathrm{fiber}(q)|\cdot\mu(q)$. Equivalence of quotient constructors is the standard Quotient.eq direction. Equalities $Z=\mathrm{classPushforward}$ and $Z_{\mathrm{RS}}=\mathrm{classPushforward}$ are then one-line applications of those rewrites.
why it matters in Recognition Science
Feeds the quotient-first path-sum object in QuotientFirstZ, which constructs $Z_q B, w_q=\sum_{q:\mathrm{TriangulationClass},B}(1/|\mathrm{Aut}(\mathrm{out},q)|)\cdot w_q(q)$ under the P2c panel lock. Also imported by FreudenthalTorusClassMass, the Crux-2 consistency gate that compares labeled versus class mass for the canonical torus (after the panel's wording repair that the original "$N^{-3}$ suppression" claim was ill-posed).
Without fiberwise pushforward, one cannot move between the proved labeled path-sum measure of PathSumMeasure and any class-orbit formulation required by the Seven Gaps gravity lane. The module is pure bookkeeping infrastructure for that passage.
scope and limits
- Does not prove finiteness of BoundedComplex; that lives in PathSumMeasure.
- Does not define the RS weight law or the physical Z_RS measure itself.
- Does not address continuum limits, gravity field equations, or mass ladders.
- Does not claim computable decidability of fiber membership.
- Does not fix the ill-posed N^{-3} torus wording; that repair is downstream.
used by (2)
depends on (1)
declarations in this module (24)
-
def
classFiber -
theorem
mem_classFiber -
def
fiberCard -
theorem
sum_fiberwise_quotient -
theorem
sum_eq_quotient_sum_classMass -
theorem
equivalent_of_mk_eq -
def
classMass -
theorem
classMass_eq_fiberCard_mul_mu -
theorem
does -
theorem
Z_eq_classPushforward -
theorem
zRS_eq_classPushforward -
abbrev
edgeAB -
abbrev
edgeBA -
def
edgeSwapRelabel -
def
firstEndpointVal -
theorem
firstEndpointVal_edgeAB -
theorem
firstEndpointVal_edgeBA -
theorem
edgeAB_ne_edgeBA -
theorem
exists_nonSingleton_fiber -
theorem
one_lt_fiberCard_edgeClass -
theorem
mu_lt_classMass_edgeClass -
structure
ClassPushforwardStatus -
def
classPushforwardStatus -
theorem
classPushforwardStatus_flags