shellToCap
plain-language theorem explainer
Backward carrier map sending an exact-shell path class of complexity at most B to a bounded triangulation class at cap B. Anyone working the capped-quotient versus exact-shell bridge cites this as the invFun half of the headline equivalence. The body is a one-line application of the single-shell backward map after converting the Fin index bound into n ≤ B.
Claim. For $B \in \mathbb{N}$ and $x$ in the disjoint union of exact path classes with shell index $n \le B$, return the corresponding class in the quotient of bounded complexes of complexity $\le B$ by vertex relabeling.
background
Module CapShellBridge builds the missing carrier equivalence behind CapShellCompatibility (Seven Gaps, P2.3). At a fixed cap $B$, a bounded complex has a unique exact complexity $\max(n_V,n_E,n_T)\le B$; conversely an exact complex in shell $n\le B$ becomes bounded by reattaching the three cap inequalities. Both directions keep incidence data and relabeling witnesses, so they descend to quotients.
ShellsUpTo B is the sigma type $\sum_{n:\mathrm{Fin}(B+1)}\mathrm{ExactPathClass},n$: exact shells indexed safely by $0,\ldots,B$. TriangulationClass B is the quotient of labeled bounded complexes by the relabeling setoid (combinatorially distinct triangulations). The sibling exactClassToCap is the backward map on a single exact-signature quotient: given $n\le B$ and a shell signature, it lifts exactToBounded through the exact setoid into the bounded relabeling quotient.
proof idea
Pure definitional wrapper. Unpack $x:\mathrm{ShellsUpTo},B$ as a Fin-indexed shell $n$ together with a shell signature and an exact path class. Convert x.1.isLt via Nat.le_of_lt_succ into the inequality $n\le B$, then feed that inequality plus the signature and class into exactClassToCap. No new quotient reasoning occurs here; all lifting work lives in exactClassToCap / exactToBounded.
why it matters
This is the invFun of the headline carrier equivalence capShellEquiv: bounded quotient classes at cap $B$ are exactly the disjoint union of exact quotient shells $0,\ldots,B$. The inverse laws shellToCap_capToShell and capToShell_shellToCap (and the intermediate shellToCap_boundedToShell) all route through it. That equivalence lets an arbitrary exact-shell phase transport to a PhaseModel at every cap and lets the finite quotient sum reindex onto exactComplexityCutoff phase B, preserving automorphism cardinality and hence the $1/|\mathrm{Aut}|$ class measure. No continuum limit or physical interpretation is claimed; the bridge is purely combinatorial carrier bookkeeping for the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.