module module moderate

`IndisputableMonolith.Gravity.SevenGaps.CapShellBridge`

Bridge layer between fixed-complexity caps and shell-indexed carriers for exact phase models in the Seven Gaps gravity stack. Maps bounded shells, exact classes, and cap presentations into one another with congruence lemmas. Cited by anyone wiring the phased-quotient continuum blocker into the full-theory ledger. Mostly definitional transport and inverse pairs, not deep analysis.

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 mutually inverse transports among shell, bounded, exact-class, and fixed-cap presentations of those models, with congruence under the shell map.

background

Seven Gaps work isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. The fixed-cap API already expresses a family of phase models and thus a sequence of finite quotient sums; completeness of $\mathbb{C}$ reduces existence of the continuum limit to a Cauchy criterion (upstream ZqContinuumBlocker).

This module sits under that blocker. It introduces ShellsUpTo B: exact shells whose complexity is at most $B$, with outer carrier $\mathrm{Fin}(B+1)$ so indices $0,\ldots,B$ are off-by-one-safe. Sibling maps (boundedToShell, exactToBounded, shellToCap, capToShell, and the exact-class variants) identify the bounded, exact, and cap presentations used elsewhere in the gravity stack.

Notation is RS gravity-native: shells are discrete complexity layers; caps are fixed cutoffs; "exact" means the untruncated class before the continuum limit is taken.

proof idea

Definition-and-transport module, not a single deep theorem. Core object is the shell carrier ShellsUpTo. Remaining declarations are constructors and inverse pairs: bounded index/signature into shells, exact models into bounded form (including relabeling), exact class into cap, and shell $\leftrightarrow$ cap. Congruence lemmas (boundedToShell_congr, shellToCap_boundedToShell, boundedToShell_exactToBounded) close the diagrams so downstream code can rewrite presentations without changing the underlying phase model.

why it matters in Recognition Science

Feeds FullTheoryLedger, the Phase 0c machine-checked status record of the full quantum-gravity campaign (one boolean per pillar benchmark; flags flip only on kernel-checked, axiom-audited targets). Without a clean cap/shell bridge, the phased-quotient continuum blocker cannot rephrase fixed-cap families as shell-indexed Cauchy sequences in a single API.

In the Seven Gaps plan this is infrastructure for P2-a: removing the complexity cutoff so the path sum can pass from finite quotients to a genuine continuum object. It does not itself prove the Cauchy criterion or flip a ledger flag; it makes those statements speak the same language as the shell-bounded exact models used in the gravity ledger.

scope and limits

Does not prove the phased-quotient sequence is Cauchy or convergent in $\mathbb{C}$.
Does not remove the complexity cutoff; only bridges cap and shell presentations.
Does not define the path-sum functional or the phase model dynamics.
Does not flip any FullTheoryLedger benchmark flag by itself.
Does not address spatial dimension, eight-tick structure, or mass-ladder claims.

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