Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseSubstrate

show as:
view Lean formalization →

Defines the Fin-8 tick-phase substrate for Gap 2 gravity: each discrete tick carries phase $2\pi\,k/8$ and an eighth root of unity, with fibers and mass-balance predicates on exact shells. Gravity and QG residual work cites it when closing oscillatory-tail phase obligations without a cancellation assumption. The module is mostly definitions plus elementary root-of-unity and equidistribution lemmas that feed certified close and tail-blocker APIs.

claimFor each tick $k \in \{0,\ldots,7\}$, attach phase $\theta_k = 2\pi k/8$ and root $\omega_k = e^{i\theta_k}$. On an exact shell, form the tick fiber and fiber mass; the shell is tick-mass-balanced when fiber masses are equal across the eight phases. Card-equidistribution at constant measure implies mass balance. The eighth roots satisfy $\omega^8 = 1$, $\omega \neq 1$ for nontrivial generators, and $\sum_{k=0}^{7} \omega_k = 0$.

background

Gap 2 in the Seven Gaps gravity program concerns continuum and oscillatory-tail obligations on $Z_q$ shells. The upstream shell-balance blocker attacks the phase part of OscillatoryTail without assuming cancellation: carrier facts give finite exact shells, positive class masses, large shell mass, and a fixed-cap pairing witness, but not a substrate action that resolves phases inside every late shell.

This module supplies that substrate in Fin-8 language. Recognition Science forces an eight-tick octave (forcing chain T7, period $2^3$), so phases live on the discrete circle of order 8. The derived phase is $2\pi\cdot\mathrm{tick}/8$ radians; the corresponding complex root is the standard eighth root of unity. Fibers partition shell mass by tick class; mass-balance says those eight masses agree.

Local setting is definitional infrastructure plus small algebraic lemmas (nontriviality, order eight, sum-to-zero), not a full continuum residual proof.

proof idea

Primarily a definition module. Core objects are the tick-derived phase, its exponential root, exact-shell substrate structure, tick fibers, equidistribution and fiber-mass predicates, and the mass-balanced predicate.

Supporting lemmas are elementary: eighth roots are nontrivial when appropriate, raise to the eighth power to 1, and sum to zero over the full Fin-8 orbit (geometric sum / cyclotomic identity). One implication lemma shows that constant-measure card equidistribution on ticks yields tick-fiber mass balance. No deep analytic argument lives here; downstream modules import these names to state certified close surfaces and tail blockers.

why it matters in Recognition Science

Closes the missing phase substrate named by the Zq shell-balance blocker so later Gap 2 work can talk about phases inside exact shells without smuggling cancellation. Downstream, the certified Fin-8 phase-close API banks a provenance-honest R5 surface after the antipodal-shift / matching route was killed; the tick-phase tail blocker hardens the R4 residual by using all-shell mass balance to force exact-shell amplitudes (and contiguous-block sums) to vanish.

The posting-history continuum residual imports the same language for an equal-strength continuum package on actual posting histories. An axiom audit module checks that headline theorems stay inside the standard classical quotient axioms. In framework terms this is the discrete eight-tick (T7) handle on oscillatory gravity residuals, not a mass-ladder or alpha-band claim.

scope and limits

used by (4)

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 (35)