capToShell
plain-language theorem explainer
Forward carrier map sending each combinatorially distinct bounded triangulation at cap B to an exact shell of complexity at most B. Anyone citing the capped-to-exact shell equivalence or the finite-sum reindexing for Zq uses this map as the toFun. It is the quotient lift of the labeled forget-cap map, justified by the congruence that relabel-equivalent bounded complexes share a shell class.
Claim. For each $B \in \mathbb{N}$, there is a well-defined map from the quotient of bounded complexes of complexity at most $B$ by relabeling isomorphism to the disjoint union, over shell indices $n \le B$, of exact path classes of complexity $n$.
background
Module P2.3 builds the missing carrier bridge behind CapShellCompatibility. At a fixed cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$. Forgetting the three cap inequalities yields an exact complex in some shell $n\le B$; conversely, an exact complex with $n\le B$ regains a bounded complex by reattaching those inequalities. Both directions keep incidence data and relabeling witnesses.
TriangulationClass B is the quotient of labeled bounded complexes by the relabeling setoid: combinatorially distinct triangulations. ShellsUpTo B is the dependent sum $\Sigma_{n:\mathrm{Fin}(B+1)}\mathrm{ExactPathClass},n$, so shells $0,\ldots,B$ with an off-by-one-safe index. The labeled forward map forgets the cap proofs, packages the exact signature, and enters the exact relabeling quotient. The congruence lemma states that this labeled map is constant on bounded relabeling classes, so it descends.
proof idea
One-line definition by Quotient.lift. The underlying function is the labeled forget-cap map (exact index, signature, and quotient class of the exact complex). The lift is licensed by the congruence theorem: if two bounded complexes are relabel-equivalent, their images under the labeled map coincide in ShellsUpTo B. No further case analysis appears at this declaration.
why it matters
This is the forward half of the headline carrier equivalence: bounded quotient classes at cap $B$ are exactly the disjoint union of exact shells $0,\ldots,B$. That equivalence is assembled by pairing this map with the backward attach-cap map and the two inverse laws.
Downstream, automorphism cardinality and the $1/|\mathrm{Aut}|$ class measure are shown invariant under the map; an arbitrary exact-shell phase transports to a phase model at every cap; and reindexing the finite quotient sum along the carrier equivalence yields equality of the phased capped sum with the exact-complexity cutoff through shell $B$. The module explicitly assumes no continuum limit, substrate phase, or physical continuum reading: only the discrete carrier and measure bridge needed for the Seven Gaps Zq blocker chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.