CapShellCompatibility
plain-language theorem explainer
Compatibility between a capped phase family and an exact-shell phase: at every complexity cap B the phased quotient sum equals the nonduplicating exact-shell cutoff through shell B. Continuum-blocker and FullTheoryLedger work cite it as the missing cross-API bridge premise for Gap 2. It is a Prop structure with one equality field, not a proved identity.
Claim. A family of phase models at each complexity cap is compatible with a phase on exact path classes when, for every natural number $B$, the finite phased quotient path sum at cap $B$ equals the exact-shell complexity cutoff summed through shell $B$.
background
Module P2-a isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum. Two APIs sit side by side. The fixed-cap side uses triangulation classes at bound $B$ and a phase model at each cap (a CapPhaseFamily), yielding a sequence of finite phased quotient sums. Completeness of $\mathbb{C}$ makes convergence equivalent to the Cauchy criterion for that sequence.
The cap-free side uses exact complexity shells: ExactPathClass n is the set of combinatorially distinct exact complexes of complexity exactly $n$, with no bound type in the definition. Summing exact shells in range B gives a telescoping cutoff whose Cauchy property is equivalent to uniform smallness of late contiguous shell blocks (ordered-tail cancellation). Zero phase fails that cancellation with an explicit witness.
The two finite sums are not definitionally equal: one runs over capped quotient classes, the other over exact shells $n \le B$. This structure names the smallest cross-API obligation that identifies them at every cap, preserving measure and phase.
proof idea
No proof body: the declaration is a Prop-valued structure. It packages a single field, an equality of complex numbers holding for every natural cap $B$, between the phased capped quotient sequence of the given cap phase family and the exact-shell complexity cutoff of the given shell phase. Downstream theorems discharge or assume that field; the structure itself only states the interface.
why it matters
This is the named missing bridge in the Gap 2 cutoff-limit blocker. Under the compatibility hypothesis, convergence of the existing phased quotient sequence is equivalent to exact-shell tail cancellation (no desired limit is assumed). FullTheoryLedger records the blocker as two obligations: oscillatory tail cancellation on exact shells, and this cap-to-shell sum equality.
CapShellBridge later supplies a canonical transport from any exact-shell phase to a capped phase family and proves the equality by finite-sum reindexing along a carrier equivalence that preserves $1/|\mathrm{Aut}|$. That closes the bridge premise for the ledger receipt gap2_capshell_bridge_discharged, while leaving continuum geometry, mesh refinement, derived measure, and full gap2_continuum_and_measure open. The structure therefore sits at the API seam between quotient-first path sums and the panel-locked exact-shell decomposition in the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.