Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.ZqShellBalanceBlocker

show as:
view Lean formalization →

Module isolating the shell-local balance forced by a uniform oscillatory tail on the phased quotient path sum: exact single-shell amplitudes must tend to zero. Gravity and QG ledger work cites it when discharging the continuum cutoff on Z_q sums. The argument is definitional plus implication lemmas linking oscillatory tails, eventual agreement, and vanishing shell amplitude; it does not bound long-block accumulation.

claimIf a phased quotient path-sum tail is uniformly oscillatory, then the exact amplitude on each fixed shell tends to zero (shell-local balance). Eventual agreement of phase models preserves this vanishing; eventual zero phase and compact support below a cutoff are incompatible with a genuine oscillatory tail. The condition is necessary for continuum completion but does not control accumulation over long shell blocks.

background

This sits in the Seven Gaps gravity stack, under the phased-quotient continuum program. The upstream module ZqContinuumBlocker isolates analytic and API obligations for removing the complexity cutoff from the phased quotient path sum: fixed-cap phase models give a sequence of finite quotient sums, and completeness of $\mathbb{C}$ makes existence of the limit equivalent to the Cauchy criterion.

Here the focus narrows to shell-local balance. An oscillatory tail means the phase structure keeps oscillating at large shell index rather than settling. Exact-shell amplitude is the contribution of one fixed shell in that sum. The module packages predicates for vanishing shell amplitude, eventual agreement of two phase models, eventual zero phase, and support below a finite cutoff, together with the elementary relations among them.

The module doc states the intended meaning directly: any uniform oscillatory tail forces individual exact-shell amplitudes to tend to zero, and that necessary condition alone does not control accumulation over long blocks.

proof idea

Definition-and-lemma module rather than a single deep theorem. Core objects are the shell-amplitude-vanishes predicate and the oscillatory-tail predicate; a main implication shows that an oscillatory tail forces shell amplitudes to vanish. Congruence lemmas transfer exact shell amplitude and oscillatory-tail status across eventual agreement of phase models. Separate blockers show that eventual zero phase and support confined below a cutoff each rule out an oscillatory tail. One-shell block packaging collects the local vanishing statement for use by continuum and ledger layers. No heavy analysis: mostly predicate definitions, rewriting, and implication chaining.

why it matters in Recognition Science

Feeds the full-theory ledger (FullTheoryLedger), the Phase 0c machine-checked status record for the quantum-gravity campaign: boolean flags flip only when target theorems are kernel-checked and axiom-audited. Closing the phased-quotient continuum path is one of the Seven Gaps pillars; shell-local balance is a necessary analytic obligation on that path, sitting under the P2-a continuum blocker.

In the Recognition gravity program this is bookkeeping for removing cutoffs from discrete path sums so continuum limits can be stated without hidden complexity caps. It does not by itself finish Cauchy completeness or long-block estimates; those remain separate obligations. Its place is to make the shell-vanishing half of the oscillatory-tail story explicit and reusable.

scope and limits

used by (1)

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