Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker

show as:
view Lean formalization →

Banks the Gap2 R4 automorphism-fiber parity blocker: on an exact complexity shell the equal-automorphism-cardinality fiber is even under the Fin-8 antipodal split p ↦ p+4. Continuum-residual and certified Fin-8 phase-close work cite it. The argument defines shell automorphism cardinality and class mass, pairs low/high ticks by a +4 equivalence, and concludes even fiber cardinality.

claimOn an exact complexity shell $c$, set $\mathrm{shellAutCard}(c)=|\mathrm{ExactAut}(\mathrm{out}\,c)|$ and $\mathrm{classMu}(c)=1/\mathrm{shellAutCard}(c)$. The tail automorphism fiber is even: Fin-8 ticks split into low and high halves related by $t\mapsto t+4$, and fiber cardinality is even (parity blocker for the antipodal mass-balance route).

background

Gap2 sits inside the Seven Gaps gravity stack. Exact complexity shells (from the exact-shell / Gaussian-UV module) organize the quotient-class path-sum configuration space without size caps; the shell-resummed sum with regulator $\exp(-\rho n^2)$ converges for every $\rho>0$. The capped-quotient bridge supplies the carrier equivalence between bounded complexes at cap $B$ and exact shells $n\le B$.

Class mass on a shell is the reciprocal of automorphism cardinality of the outgoing exact complex: equal $\mathrm{classMu}$ means equal $|\mathrm{ExactAut}|$. The antipodal-balance bridge states the sufficiency half of the R4 weakening: eventually, opposite Fin-8 fibers $p$ and $p+4$ carry equal class mass. The phased-quotient cutoff blocker isolates the Cauchy criterion needed to drop complexity cutoffs from the path sum.

This module packages the equal-automorphism-cardinality fiber and the parity obstruction that appears when that fiber is split by the tick antipode.

proof idea

Definition layer first: automorphism-fiber buckets, the identity $\mathrm{classMu}=1/\mathrm{shellAutCard}$, and the converse cardinality recovery from equal class mass. Tick sets are split into low and high halves; valuation lemmas record that adding four sends low ticks to high and conversely. An equivalence identifies the two halves. Cardinality of the paired tick set is therefore even, which upgrades to evenness of the tail automorphism fiber and to the named parity blocker used by downstream Gap2 APIs.

why it matters in Recognition Science

Closes a mechanical Gap2 R4 obligation on automorphism-fiber parity after the antipodal mass-balance bridge. Downstream, the certified Fin-8 phase-close API banks the provenance-honest R5 surface once matching / tail-antipodal-shift flip routes were killed; the continuum-measure residual DAG names ordered residuals for Pillar-2 measure and continuum-limit recovery; the posting-history continuum residual keeps an equal-strength open API on actual posting histories. An audit module requires headline theorems to print within propext, Classical.choice, and Quot.sound only. In the broader RS gravity chain this is infrastructure for removing cutoffs and recovering continuum measure, not a mass or alpha claim.

scope and limits

used by (4)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (23)