boundedToShell
plain-language theorem explainer
Forward map sending a B-capped bounded complex to the exact-shell carrier of complexity at most B. It records exact complexity as an index in Fin(B+1), keeps the shell signature, and places the underlying exact complex in the relabeling quotient. Used by the capped-to-shell quotient lift, automorphism and class-measure preservation, and phase transport at a cap. The body is a three-field sigma constructor from the index, signature, and toExact quotient class.
Claim. For $B\in\mathbb{N}$ and a bounded complex $K$ of cap $B$, form the pair in $\sum_{n\le B}\mathrm{ExactPathClass}(n)$ whose shell index is the exact complexity of $K$ (as an element of $\{0,\ldots,B\}$), whose signature is the exact $(n_V,n_E,n_T)$ data of $K$, and whose class is the relabeling quotient of the exact complex obtained by forgetting the three cap inequalities.
background
Module P2.3 of Seven Gaps builds the carrier bridge behind CapShellCompatibility. At fixed cap $B$, a bounded complex is an incidence structure with three size bounds $\max(n_V,n_E,n_T)\le B$. An exact complex lives at a fixed signature with no cap slack. The two sides are related by forgetting or reattaching those inequalities while keeping incidence data and relabeling witnesses.
ShellsUpTo B is the sigma type $\sum_{n:\mathrm{Fin}(B+1)}\mathrm{ExactPathClass},n$: shell indices $0,\ldots,B$ paired with exact path classes. Upstream helpers package the data: boundedShellIndex turns complexity into a Fin(B+1) witness via the three cap lemmas; boundedShellSig rebuilds the exact signature with the corresponding strict bounds; toExact drops the cap proofs to an exact complex.
No continuum limit, target-sum identity, or physical phase is assumed here; the object is purely the labeled forward carrier map.
proof idea
Definitional packing, not a tactic proof. The value is the sigma triple whose first component is boundedShellIndex K (complexity as Fin(B+1)), whose second is boundedShellSig K (exact signature of the three sizes), and whose third is Quotient.mk _ (toExact K) (the exact complex after forgetting caps, entered into the exact relabeling quotient). All inequalities needed for the Fin and signature bounds come from the three hypoteses already stored on the bounded complex.
why it matters
This is the labeled forward half of the capped-quotient to exact-shell bridge that closes CapShellCompatibility. Downstream, boundedToShell_congr shows it respects bounded relabeling, so it lifts to capToShell on triangulation classes. The inverse direction is witnessed by boundedToShell_exactToBounded and shellToCap_boundedToShell. Quotient-level consequences include shellAutCard_capToShell (automorphism cardinality preserved) and classMu_capToShell (the $1/|\mathrm{Aut}|$ class measure matches). phaseModelAtCap transports an arbitrary exact-shell phase to a PhaseModel at every cap by evaluating through this map. Reindexing finite quotient sums along the resulting equivalence yields equality with exactComplexityCutoff phase B (shell range $B+1$), without assuming continuum physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.