toExact
plain-language theorem explainer
Forgets the size cap on a bounded combinatorial complex, returning an exact complex with the same vertex/edge/tet counts and the same incidence maps. Downstream shell and measure bridges cite it to move from capped triangulation classes into cap-free exact shells. The construction is pure structure packing: copy edge and tet incidence, drop the bound proofs.
Claim. Given a natural number $B$ and a bounded complex $K$ of cap $B$, there is an exact complex with the same numbers of vertices, edges, and tetrahedra whose edge-incidence and tetrahedron-incidence maps are those of $K$. The output type carries no residual dependence on the cap $B$.
background
This module builds exact complexity shells for the Seven Gaps path-sum configuration space: configurations are organized by exact vertex/edge/tet counts with no size caps in the shell type, then a hand-inserted Gaussian UV factor $\exp(-\rho n^2)$ makes the shell series summable for every $\rho>0$. The module is explicit that the regulator is mathematical, not derived physics, and that $\rho\to 0^+$ remains an open named hypothesis.
A bounded complex of cap $B$ is a labeled simplicial configuration whose counts sit under $B$, together with incidence data and the cap inequalities. An exact complex of signature $(v,e,t)$ is the cap-free counterpart: exactly $v$ vertices, $e$ edges, $t$ tetrahedra, with abstract maps edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v, and no inequalities. Because there is no cap, the cross-cap identification problem of the bounded type cannot arise.
The map here is the forgetful bridge from the capped world into that exact type, retaining only incidence and the exact counts $n_V,n_E,n_T$ of the source.
proof idea
Definitional structure construction, not a tactic proof. The fields of the exact complex are filled by the corresponding incidence fields of the bounded complex: edge endpoints and tetrahedron vertex tuples are copied verbatim. The target signature is taken from the source counts $K.nV$, $K.nE$, $K.nT$, so the cap parameter $B$ never appears in the codomain. No lemmas are applied.
why it matters
This is the labeled forgetful map that lets capped triangulation classes enter exact complexity shells. CapShellBridge builds on it heavily: boundedToShell quotients toExact K into the exact relabeling class; autEquivToExact and autCard_toExact show automorphisms (hence $|\mathrm{Aut}|$) are preserved under cap forgetting; mu_eq_exactMu_toExact equates the labeled symmetry-factor measures; and classMu_capToShell / shellAutCard_capToShell lift those equalities to the quotient. In-module, toExact_complexity and toExact_relax record that complexity is unchanged and that relaxing the cap is definitionally invisible on the exact image.
Within the Seven Gaps program this is Stage-1 shell infrastructure: it separates combinatorial incidence from artificial size bounds so shell entropy bounds and the regulated path sum can be stated on genuine cap-free classes. It does not touch continuum limits, physical actions, or regulator removal; those stay open per the module honesty disclosures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.