Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker

show as:
view Lean formalization →

Infrastructure for continuum obstruction on the phased quotient path sum: a free phase at each complexity cap, with no cross-cap coherence. Defines capped amplitudes, oscillatory tails, and Cauchy criteria that reduce continuum existence to tail decay. Gravity and Gap-2 continuum residual modules import it as the shared blocker surface after the zero-phase regulator no-go.

claimAt each complexity cap $B$, a phase family $\theta_B$ yields a phased quotient sequence $Z_q^{(B)}$. Continuum existence is equivalent to a Cauchy criterion on the capped amplitudes $Z_{\mathrm{cap}}(B)$ and to vanishing of the oscillatory tail. Exact-shell amplitudes and exact complexity cutoffs relate the capped object to shell carriers; no cross-cap phase coherence is assumed.

background

Seven Gaps work on the quotient-first path sum $Z_q$ after the zero-phase regulator no-go: the Gaussian-regulated UV object has no $\rho\to 0^+$ limit at vanishing phase. The phase-structure lane adds an oscillatory phase model at fixed complexity cap and proves structure theorems there, while the continuum limit remains open.

This module packages the continuum side of that obstruction. A cap phase family is only a phase choice per complexity bound; it supplies no coherence across caps. From it one builds the phased $Z_q$ sequence, capped amplitudes $Z_{\mathrm{cap}}$, and an oscillatory tail whose decay is equivalent to the Cauchy property of $Z_{\mathrm{cap}}$. Exact shell amplitudes and exact complexity cutoffs connect the capped quotient to shell carriers used elsewhere in the gravity stack.

proof idea

Definition-and-equivalence module rather than a single end theorem. It introduces the cap phase family and the phased sequence, then the predicates for a phased complexity limit and the associated Cauchy criterion, with an iff linking them. Capped amplitude $Z_{\mathrm{cap}}$ is related to the oscillatory tail by a telescoping identity; Cauchy-ness of $Z_{\mathrm{cap}}$ is equivalent to tail control. Exact complexity cutoff and its limit predicate close the bridge toward exact-shell carriers. Upstream phase structure and the zero-phase regulator no-go supply the fixed-cap and no-go context; this file organizes the continuum blocker language those results feed.

why it matters in Recognition Science

Shared continuum-blocker surface for Gap-2 and related Seven Gaps gravity work. CapShellBridge builds the carrier equivalence behind cap-shell compatibility stated here. FullTheoryLedger records campaign status against this infrastructure. Gap2 continuum residual DAG, posting-history continuum residual, certified Fin-8 phase close, tail Aut-fiber parity blocker, metric refinement carrier blocker, and Zq shell balance blocker all import the module to name residuals, close surfaces, or further blockers on measure and continuum recovery.

In the RS gravity program this sits after T-level forcing landmarks only indirectly: it is a QG path-sum obstruction layer (phased $Z_q$, complexity caps), not a derivation of $J$, $\varphi$, or $D=3$. It keeps the continuum limit honestly open unless cross-cap coherence or tail decay is supplied elsewhere.

scope and limits

used by (8)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (26)