exactToBounded
plain-language theorem explainer
Converts an exact triangulation complex living in shell n into a B-capped bounded complex whenever n ≤ B, by reattaching the three size inequalities and copying incidence data. Anyone proving the capped-to-exact carrier equivalence or transporting exact-shell phases cites this map. The body is a structure constructor: three le_trans chains plus field copy.
Claim. Given a natural number cap $B$, a shell index $n \le B$, a shell signature $s$ at level $n$, and an exact complex $K$ on the vertex/edge/tetrahedron counts of $s$, form the bounded complex at cap $B$ with the same counts and the same edge and tet incidence maps, whose three size bounds are the composites of the shell-membership inequalities with $n \le B$.
background
Module P2.3 of the Seven Gaps gravity stack builds the carrier bridge behind CapShellCompatibility. Two presentations of finite triangulation data sit side by side: exact complexes, whose vertex/edge/tet cardinalities are fixed by a shell signature at a definite shell index $n$, and bounded complexes at a cap $B$, which carry three proofs that those cardinalities are at most $B$.
A shell signature packages the three Fin-bounded counts together with the shell-index witness. An exact complex on those counts supplies the incidence maps (edge endpoints and tet vertices). A bounded complex at $B$ is the same incidence data plus the three cap inequalities. The module states that both maps preserve incidence and relabeling witnesses, descend to the quotient carriers, and are inverse there, so automorphism cardinalities and the $1/|\mathrm{Aut}|$ class measure are unchanged.
The only arithmetic used here is ordinary $\le$-transitivity on $\mathbb{N}$: each shell count is strictly less than $n+1$, hence $\le n$, and $n\le B$ yields the cap bound.
proof idea
Pure structure construction, not a tactic proof. Set the three cardinality fields of the bounded complex equal to the signature counts of $s$. For each of $hV$, $hE$, $hT$, chain Nat.le_of_lt_succ on the Fin-bound witness inside the shell signature with the hypothesis $n\le B$ via le_trans. Copy edgeVerts and tetVerts verbatim from the exact complex $K$. No incidence or relabeling obligations are discharged here; they are inherited by definition.
why it matters
This is the backward leg of the capped-quotient / exact-shell carrier equivalence that the module exists to supply. Downstream, exactClassToCap lifts it through the exact-setoid quotient to a map into triangulation classes at cap $B$; exactRelabelToBounded shows exact relabelings remain bounded relabelings after the caps are attached; and boundedToShell_exactToBounded proves the round-trip identity (forgetting the cap recovers the original exact-shell class by proof irrelevance).
Together these let an arbitrary exact-shell phase transport to a PhaseModel at every cap, so the finite quotient sum can be reindexed against exactComplexityCutoff phase B (shell range $B+1$). That equality is the content of CapShellCompatibility. No continuum limit, substrate phase, or physical gravity law is assumed; the bridge is purely combinatorial carrier bookkeeping inside the Seven Gaps stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.