module module moderate

`IndisputableMonolith.Gravity.SevenGaps.CapShellBridge`

Bridge between fixed-cap phase models and exact complexity shells for the Seven Gaps gravity path. It packages shell indices up to a bound B, and the mutual maps among exact, bounded, and cap presentations of those shells. Anyone wiring the phased-quotient continuum limit into the full-theory ledger cites this API. The module is mostly definitional transport and congruence lemmas, not a deep analytic argument.

claimFor a complexity bound $B$, the exact shells of complexity at most $B$ are carried by $\mathrm{Fin}(B+1)$ (indices $0,\ldots,B$). The module supplies the mutual translations among exact shells, bounded-shell signatures, and fixed-cap presentations, together with the natural congruences that these maps compose to the identity on the overlapping data.

background

Seven Gaps work isolates analytic and API obligations needed to drop the complexity cutoff on the phased quotient path sum. The upstream blocker module records that a fixed-cap API already expresses a family of phase models and hence a sequence of finite quotient sums; completeness of $\mathbb{C}$ then reduces existence of the continuum limit to the Cauchy criterion for that sequence.

This module sits one layer down in the data model. Shells are exact complexity strata; a bound $B$ truncates to shells of complexity at most $B$, with $\mathrm{Fin}(B+1)$ as the off-by-one-safe index carrier. Cap presentations are the fixed-cap phase models used by the continuum blocker. Bounded signatures sit between the two, so that exact classes, bounded shells, and caps can be compared without smuggling extra cutoff hypotheses.

Sibling names in the module are the transport maps and their round-trip identities: exact to bounded, bounded to shell, shell to cap, and the corresponding reverse and congruence lemmas.

proof idea

Definition-and-transport module. Core objects are the bounded shell carrier and the maps exactToBounded, boundedToShell, shellToCap (and reverses exactClassToCap, capToShell, etc.). Proof content is mostly definitional equality and congruence: round-trips such as shellToCap after boundedToShell, and boundedToShell after exactToBounded, are discharged by unfolding and Fin-index arithmetic. No analytic Cauchy or continuum argument lives here; that stays in the upstream blocker and downstream ledger.

why it matters in Recognition Science

The full-theory ledger (Phase 0c of the QG full-theory campaign) imports this bridge so that pillar flags for the phased-quotient continuum path can speak in a single vocabulary of caps and shells. Without a checked translation layer, the fixed-cap Cauchy criterion and the exact-shell complexity bookkeeping would remain two parallel APIs. The module therefore closes an interface gap on the gravity side of the Seven Gaps stack rather than proving a new physical law. It does not itself flip a ledger boolean; it makes the target statements of those flags type-check against one another.

scope and limits

Does not prove the phased-quotient path sum is Cauchy or convergent in $\mathbb{C}$.
Does not remove the complexity cutoff; only bridges cap and shell presentations of bounded data.
Does not fix a numerical value of $B$ or derive $B$ from Recognition landmarks.
Does not establish mass, $G$, or other RS constants; gravity ledger use is purely structural.
Does not add axioms or discharge sorry in FullTheoryLedger pillar flags by itself.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker module_import

declarations in this module (28)

abbrev ShellsUpTo L43
def boundedShellIndex L52
def boundedShellSig L56
def boundedToShell L65
def exactToBounded L71
def exactRelabelToBounded L84
def exactClassToCap L95
def shellToCap L104
theorem boundedToShell_congr L110
def capToShell L140
theorem shellToCap_boundedToShell L144
theorem boundedToShell_exactToBounded L165
theorem capToShell_shellToCap L181
theorem shellToCap_capToShell L189
def capShellEquiv L197
def autEquivToExact L207
theorem autCard_toExact L225
theorem mu_eq_exactMu_toExact L230
def shellAutCard L236
theorem shellAutCard_capToShell L240
theorem classMu_capToShell L263
def phaseModelAtCap L288
theorem classPhase_phaseModelAtCap L295
def capPhaseFamily L305
theorem sum_fin_eq_sum_range L312
theorem sum_shellsUpTo_eq_exactComplexityCutoff L329
theorem phasedZq_eq_exactComplexityCutoff L343
theorem capShellCompatibility L372