boundedToShell_exactToBounded
plain-language theorem explainer
For $n\le B$, attaching the three cap proofs to an exact complex of shell signature $s$ and then forgetting the cap recovers the original exact-shell class $(n,s,[K])$. Cited by anyone assembling the CapShellBridge inverse laws that underwrite CapShellCompatibility. The proof is structural: unfold both maps, kill proof fields by irrelevance, and close the quotient by the reflexive relabeling.
Claim. Let $n\le B$, let $s$ be a shell signature at level $n$, and let $K$ be an exact complex whose vertex, edge, and triangle counts match $s$. Then forgetting the cap after attaching it returns the exact-shell class $\langle n,\,s,\,[K]\rangle$: the shell index is $n$, the signature is unchanged, and the quotient class is that of $K$.
background
Module SevenGaps.CapShellBridge builds the missing carrier equivalence behind CapShellCompatibility. 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 two quotient carriers and are mutual inverses there.
A shell signature packages the three counts $(n_V,n_E,n_T)$ together with the equality that their maximum equals the shell index $n$. An exact complex is a finite incidence structure realizing those counts exactly. The map exactToBounded reattaches the three $\le B$ proofs; boundedToShell reads off the exact complexity as a shell index in ${0,\ldots,B}$ and packages the residual exact complex as a quotient class under incidence-preserving relabeling.
No continuum limit, substrate phase, or physical interpretation is assumed: the bridge is purely combinatorial.
proof idea
Destructure the shell signature $s$ into its three count components and the maximality proof, then further unpack each count as a subtype. After dsimp on the signature projections, substitute the shell index $n$ from the maximality equality. Unfold boundedToShell, boundedShellIndex, boundedShellSig, exactToBounded, and complexity; the three cap proofs disappear by proof irrelevance and the incidence data is definitionally identical. The remaining quotient equality is discharged by Quotient.sound applied to the reflexive exact-relabeling witness ExactRelabel.refl K.
why it matters
This is one half of the carrier inverse pair. Downstream, capToShell_shellToCap invokes it after quotient induction to obtain the right-inverse law on exact-shell classes: forgetting then reattaching the cap is the identity on ShellsUpTo B. Together with the companion left inverse, the two maps give a bijection of quotient carriers that preserves automorphism cardinality and therefore the $1/|\mathrm{Aut}|$ class measure.
That equivalence lets an arbitrary exact-shell phase transport to a PhaseModel at every cap $B$, after which reindexing the finite quotient sum proves equality with exactComplexityCutoff phase B (shell range $B+1$). The construction is the combinatorial backbone of Seven Gaps P2.3 and of ZqContinuumBlocker.CapShellCompatibility; it does not itself assert any continuum or physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.