Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.ClassPushforward

show as:
view Lean formalization →

Bookkeeping layer for Seven Gaps path sums: fibers of the quotient from labeled configurations to triangulation classes, fiber cardinalities, and class masses. Rewrites a labeled configuration sum as a sum over classes weighted by class mass. Cited by the quotient-first Z object and the Freudenthal torus class-mass consistency gate. Arguments are finite-sum rewrites and fiberwise counting on the Fintype BoundedComplex.

claimFor a bounded complex $B$ with quotient map to triangulation classes $q$, the class fiber is $\{x : [x]=q\}$, with class mass $\mathrm{mass}(q)=|\mathrm{fiber}(q)|\cdot\mu$. The labeled path-sum equals the class pushforward $\sum_q \mathrm{mass}(q)$, and likewise for the RS path-sum $Z_{\mathrm{RS}}$.

background

Lane 2 of Seven Gaps builds a proved path-sum measure $Z_{\mathrm{RS}}$ on the scoped configuration class BoundedComplex B. Upstream, that class is a Fintype via an explicit coding equivalence, so all sums are finite and classical decidability is enough for noncomputable bookkeeping.

This module sits between the labeled configuration space and the quotient by triangulation class. The labeled fiber of a class $q$ is every element of the underlying type that maps to $q$. Fiber cardinality and class mass (fiber size times the path weight) are the elementary pushforward data.

The Recognition setting is gravity-side path-sum bookkeeping for the seven-gaps program: convert sums over labeled complexes into sums over classes, with automorphism or stabilizer factors appearing only after this pushforward is in place.

proof idea

Definition-heavy module with short finite-sum lemmas, not a single deep theorem. Fibers and membership are classical subtypes of the quotient map. Fiber cardinality is the Fintype card of that subtype. Class mass is defined as fiber card times the configuration weight $\mu$.

The main identities are fiberwise sum rewrites: a sum over labeled configurations equals the sum over classes of the sum over the fiber, which collapses to a sum of class masses. Equivalence of quotient representatives is used to show well-definedness on classes. Two wrapper equalities identify the ordinary path-sum $Z$ and the RS path-sum $Z_{\mathrm{RS}}$ with this class pushforward form.

why it matters in Recognition Science

Supplies the QUOTIENT_BOOKKEEPING primitives locked by the Seven Gaps panel. Downstream, QuotientFirstZ builds the quotient-first object $Z_q B w_q=\sum_q (1/|\mathrm{Aut}(\mathrm{out}, q)|)\cdot w_q(q)$, which needs class-level masses rather than labeled sums. FreudenthalTorusClassMass uses the same pushforward to compare labeled versus class mass for the canonical torus and to gate the $N^{-3}$ suppression claim in a well-posed form.

Without this layer, path-sum identities stay stuck on labeled configurations and cannot feed class-level gravity gates. It does not itself prove dynamical suppression or mass formulae; it only makes the change of summation domain rigorous.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (24)