shellToCap_capToShell
plain-language theorem explainer
Left inverse for the carrier maps between capped triangulation classes at bound B and exact complexity shells 0..B. Anyone assembling the headline capped-to-shell equivalence cites this identity. The proof is quotient induction that reduces to the already-proved representative-level left inverse.
Claim. For every natural number $B$ and every equivalence class $q$ of bounded triangulations at complexity cap $B$, sending $q$ to its exact shell and then back to a capped class recovers $q$.
background
Module P2.3 of Seven Gaps builds the missing carrier bridge behind CapShellCompatibility. At 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 proofs. Both directions keep incidence data and relabeling witnesses, so they descend to the two quotient carriers.
TriangulationClass B is the quotient of bounded complexes at cap $B$. ShellsUpTo B is the disjoint union of exact-shell quotients for shells $0,\ldots,B$. The forward map on classes lifts the representative map that forgets the cap and records the exact shell; the reverse map reattaches caps. The module claims these are inverse on the quotients and preserve automorphism cardinality (hence the $1/|\mathrm{Aut}|$ class measure).
No continuum limit, phase model, or target-sum equality is assumed at this layer; only the combinatorial carrier equivalence.
proof idea
Term-mode proof by quotient induction. Apply Quotient.inductionOn to the capped class $q$, introducing a bounded representative $K$. Discharge the goal by the already-proved representative identity shellToCap_boundedToShell K, which states that capping after forgetting the cap returns the original bounded class. No further case splits or measure arguments appear.
why it matters
Supplies the left_inv field of the headline carrier equivalence capShellEquiv, whose doc-comment states that bounded quotient classes at cap $B$ are exactly the disjoint union of exact quotient shells $0,\ldots,B$. That equivalence is the combinatorial backbone of CapShellCompatibility in the Zq continuum blocker: reindexing the finite quotient sum along the carrier map equates the capped sum to exactComplexityCutoff phase B (shell range $B+1$).
Within Seven Gaps gravity, this closes the P2.3 bridge without assuming substrate phases or physical continuum interpretations. It is pure carrier algebra feeding automorphism-weighted class measures and later phase transport from exact shells into PhaseModel at every cap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.