Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseSubstrate

show as:
view Lean formalization →

Defines the Fin-8 tick-phase substrate used in Gap2 gravity work: phase $2\pi\,t/8$ on each tick, eighth roots of unity, shell fibers by tick, and mass-balance predicates. Downstream tail blockers and certified phase-close APIs import it as the carrier for exact-shell phase accounting. Content is definitions plus elementary root-of-unity sum identities, not a deep existence proof.

claimFor each tick $t\in\{0,\ldots,7\}$, attach phase $\theta_t=2\pi t/8$ and root $\omega^t=e^{i\theta_t}$. Partition an exact shell into tick fibers; fiber mass is the measure of each fiber. Equidistribution (constant class measure across ticks) implies mass balance. The eight roots sum to zero and $\omega\neq 1$ with $\omega^8=1$.

background

Gap2 in the Seven Gaps gravity program must control oscillatory tails on exact $Z_q$ shells without assuming phase cancellation by fiat. The upstream shell-balance blocker records finite exact shells, positive class masses, and a fixed-cap pairing witness, but supplies no substrate that resolves phases inside every late shell.

This module is that substrate. It ties phases to the Recognition eight-tick octave: each discrete tick carries phase $2\pi\cdot\mathrm{tick}/8$ and the matching eighth root of unity. Shells are sliced into tick fibers; fiber mass and the predicate that those masses balance (equal across the eight ticks) are the bookkeeping objects later used to force shell amplitudes to vanish.

Local setting is pure discrete phase geometry on $\mathrm{Fin},8$, not continuum posting histories or full RCL cost calculus.

proof idea

Primarily a definition module. It introduces tick-derived phase, the exponential form, tick roots, exact-shell phase substrate structure, fibers, equidistribution, fiber mass, and the mass-balanced predicate. Supporting lemmas are elementary complex arithmetic: the primitive eighth root is not 1, its eighth power is 1, and the sum of the eight tick roots vanishes. A short implication shows that constant class measure (card equidistribution) yields mass balance. No heavy analysis or existence argument lives here.

why it matters in Recognition Science

Closes the missing phase carrier named by the Zq shell-balance blocker so Gap2 can talk about exact-shell phases without a bare cancellation hypothesis. Downstream, the tick-phase tail blocker uses all-shell mass balance to make every exact-shell amplitude identically zero (contiguous-block sums vanish). The certified Fin-8 phase-close API banks provenance-honest close surfaces after the antipodal-shift route was killed. The substrate audit demands headline theorems stay inside standard classical axioms. The posting-history continuum residual imports the same vocabulary while remaining an open equal-strength API on actual histories. Landmark link: T7 eight-tick octave as the discrete phase clock.

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)