capToShell_shellToCap
plain-language theorem explainer
Right inverse law: on exact-shell quotient classes of index at most B, attaching the three cap proofs and then forgetting the cap recovers the original class. Anyone assembling the carrier equivalence between bounded triangulation classes and the disjoint union of shells 0..B cites this. The proof is quotient induction plus the forget-after-attach identity on exact complexes.
Claim. For every natural number $B$ and every exact-shell quotient class $x$ whose shell index lies in $\{0,\ldots,B\}$, mapping $x$ to a bounded triangulation class by reattaching the three cap proofs and then forgetting the cap returns $x$.
background
Module Seven Gaps P2.3 builds the missing carrier equivalence behind CapShellCompatibility. At cap $B$, a bounded complex has 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 proofs. Both maps carry incidence data and relabeling witnesses, so they descend to the two quotient carriers.
ShellsUpTo B is the dependent sum over shell indices in $\mathrm{Fin}(B+1)$ of exact path classes: the off-by-one-safe carrier for shells $0,\ldots,B$. The forward map on bounded quotient classes lifts the forgetful map from capped complexes to exact shells; the reverse map attaches caps.
Upstream, the pointwise identity that forgetting a just-attached cap recovers the original exact-shell class is already proved: proof fields vanish by irrelevance and incidence data is unchanged. That lemma is the computational engine here.
proof idea
Destructure the shell class as an index $n<B+1$, a shell signature, and a quotient class of exact complexes. Run quotient induction on that class to obtain a concrete exact complex $K$. Reduce the goal to the already-proved forget-after-attach identity, feeding it the inequality $n\le B$ (from $n<B+1$), the signature, and $K$. No new algebra: pure structure unpacking plus that one lemma.
why it matters
This is the right-inverse half of the headline carrier equivalence: bounded quotient classes at cap $B$ are exactly the disjoint union of exact quotient shells $0,\ldots,B$. The equivalence packages the two maps with this law and its left-inverse twin as the inverse proofs.
That equivalence is the bridge required by CapShellCompatibility. It preserves automorphism cardinality, hence the $1/|\mathrm{Aut}|$ class measure, and lets an arbitrary exact-shell phase transport to a phase model at every cap. Reindexing the finite quotient sum along the equivalence then matches the exact-complexity cutoff whose shell range is $B+1$.
No continuum limit, substrate phase, or physical interpretation is assumed; the result is pure finite carrier bookkeeping inside the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.