capShellEquiv
plain-language theorem explainer
Bounded triangulation quotient classes at cap $B$ are canonically bijective with the disjoint union of exact-shell quotient classes of complexity $0$ through $B$. Continuum-blocker and finite-$Z_q$ reindexing arguments in the Seven Gaps gravity stack cite this as the carrier equivalence. The definition packages the already-proved forward and reverse maps with their two inverse laws into a single type equivalence.
Claim. For every natural number $B$, the type of bounded triangulation quotient classes at cap $B$ is equivalent to $\sum_{n=0}^{B}$ (exact path classes of complexity $n$). Explicitly, the forward map sends a bounded class to its exact complexity shell, and the reverse map reattaches the three cap bounds; the two maps are mutually inverse on the quotients.
background
The module builds the missing carrier bridge behind capped-to-exact shell compatibility for the Seven Gaps continuum blocker. 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 living in shell $n\le B$ becomes a bounded complex by reattaching the three inequality proofs that enforce the cap. Both directions keep incidence data and relabeling witnesses, so they descend to the quotient carriers.
ShellsUpTo B is the dependent sum over Fin(B+1) of exact path classes: the off-by-one-safe index set for shells $0,\ldots,B$. The forward map on quotients is the lift of the bounded-to-shell assignment; the reverse map is shell-to-cap. Upstream inverse laws already show these are left and right inverses on the respective quotient types.
No continuum interpretation, substrate phase, or target-sum equality is assumed at this stage: only the finite carrier identification.
proof idea
One-line packaging of an Equiv record. The forward function is the already-defined quotient lift that sends a bounded class to its exact shell; the inverse is the shell-to-cap map that reattaches the three cap proofs. Left-inverse and right-inverse fields are filled by the two previously proved inverse laws (shell-to-cap after cap-to-shell, and cap-to-shell after shell-to-cap). No new algebraic work occurs here.
why it matters
This is the headline carrier equivalence of the CapShellBridge module. Downstream, the finite-sum reindexing theorem uses it to identify the phased capped quotient sum with the exact-shell complexity cutoff through shell $B$. That equality is the sole obligation inside the P2.3 closer, which supplies a canonically transported capped phase family satisfying CapShellCompatibility for every exact-shell phase.
The FullTheoryLedger then cites the compatibility half when certifying the Pillar 2 cutoff-limit blocker: convergence of the capped $Z_q$ sequence is reduced to an oscillatory-tail condition on exact shells, with the nonduplicating shell decomposition justified by this bridge. The construction is combinatorial (quotient carriers and automorphism-aware measures), not a geometric continuum or mesh-refinement limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.