exactClassToCap
plain-language theorem explainer
Well-defined map sending an exact-shell triangulation class of fixed signature at shell n ≤ B to a capped triangulation class at B. Anyone building the exact-shell ↔ capped-quotient carrier equivalence cites it. Defined by Quotient.lift of the labeled exact-to-bounded map, with well-definedness from the relabeling transport.
Claim. Fix $n \le B$ and a shell signature $s$ of complexity $n$. There is a map from the quotient of exact complexes with signature $s$ (modulo exact relabeling) into the space of triangulation classes at cap $B$, obtained by reattaching the three bound proofs $n_V,n_E,n_T \le B$ and descending through the relabeling setoid.
background
Module P2.3 of the Seven Gaps gravity stack builds the carrier equivalence behind CapShellCompatibility. At a finite cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$. Conversely, an exact complex living in shell $n\le B$ becomes bounded by reattaching the three inequality proofs that its vertex, edge, and triangle counts sit under $B$.
Both directions keep incidence data and relabeling witnesses, so they descend to the two quotient carriers (exact-shell classes versus capped triangulation classes) and are inverse there. The present definition is the backward arrow on a single exact-signature quotient: domain is the quotient by the exact setoid of complexes with fixed signature $s=(n_V,n_E,n_T)$ at shell $n$; codomain is TriangulationClass B.
Upstream labeled maps are exactToBounded (attach the three cap proofs) and exactRelabelToBounded (transport a relabeling witness across that attachment). No continuum limit, phase model, or measure identity is assumed at this layer.
proof idea
One-line Quotient.lift of the labeled map. On representatives, send $K$ to the class of exactToBounded hn s K. Well-definedness: if two exact complexes are related by an exact-setoid witness $r$, apply exactRelabelToBounded hn s r and pass the resulting bounded relabeling to Quotient.sound. No further arithmetic; the work sits in those two sibling maps.
why it matters
First half of the backward carrier arrow. Downstream shellToCap packages it over the full disjoint union of exact shells through $B$ by reading off the shell index and signature from a ShellsUpTo B pair and calling this map. That full backward map, together with the forward boundedToShell direction and the inverse laws, supplies the missing carrier equivalence for ZqContinuumBlocker.CapShellCompatibility.
Once the carriers match, automorphism cardinalities (hence the $1/|\mathrm{Aut}|$ class measure) transport, an arbitrary exact-shell phase becomes a PhaseModel at every cap, and reindexing the finite quotient sum proves equality with exactComplexityCutoff phase B (shell range $B+1$). The module explicitly assumes no target-sum identity, convergence, substrate phase, or physical continuum reading; those sit further downstream in the Seven Gaps chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.