capShellCompatibility
plain-language theorem explainer
Every exact-shell phase admits a canonically transported capped phase family that meets the missing capped-shell compatibility condition. Gravity workers closing Seven Gaps pillar P2.3 cite this as the bridge discharge. The proof is a one-line packaging of the finite-sum reindexing identity equating phased capped quotient sums with exact complexity cutoffs.
Claim. For every assignment of real phases to exact path classes on each shell $n$, the canonically transported capped phase family is compatible with that assignment: at every bound $B$, the phased capped quotient sum equals the exact-shell complexity cutoff through shell $B$.
background
This module builds the missing carrier bridge behind capped-shell compatibility. At cap $B$, a bounded complex has unique exact complexity $\max(n_V,\max(n_E,n_T))\le B$; conversely an exact complex in shell $n\le B$ becomes bounded by reattaching three cap proofs. Both maps carry incidence data and relabeling witnesses, so they descend to inverse maps on the two quotient carriers (the headline carrier equivalence).
The bridge preserves automorphism cardinality and hence the class measure $1/|\mathrm{Aut}|$. An arbitrary exact-shell phase then transports to a phase model at every cap. Reindexing the finite quotient sum along the carrier equivalence is what yields equality with the exact complexity cutoff, whose shell range is $B+1$. No target-sum equality, convergence statement, substrate phase, or physical continuum interpretation is assumed.
Upstream, the finite-sum reindexing theorem already states that the phased capped quotient sum transported from any exact-shell phase equals its exact-shell cutoff through shell $B$.
proof idea
Term-mode one-liner. Capped-shell compatibility is a structure whose single field is the phased-sum identity. The proof fills that field by applying the headline finite-sum reindexing theorem (phased capped sequence equals exact complexity cutoff) to the given exact-shell phase. Carrier equivalence, automorphism-cardinality preservation, class-measure preservation, and the transported phase family are already proved earlier in the module and are not reopened here.
why it matters
This is the P2.3 closer: every exact-shell phase has a canonical capped transport satisfying the previously missing compatibility premise. Downstream, the Full Theory Ledger records the discharge as a theorem: the missing-bridge premise of the gap-2 cutoff-limit blocker is satisfied for the constructed family (and only that family), via the carrier equivalence preserving $1/|\mathrm{Aut}|$. The ledger is explicit that this is a sub-premise receipt, not a closure of the continuum-and-measure gap. In the Recognition gravity program it sits inside Seven Gaps bookkeeping; it does not invoke the forcing chain T0-T8, the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.