toExact_complexity
plain-language theorem explainer
Forgetting the size cap on a bounded complex leaves its complexity unchanged: the exact complexity of the image equals the original capped complexity. Anyone moving data between BoundedComplex and ExactComplex in the exact-shell path-sum construction cites this. The equality is definitional (proof by rfl).
Claim. For every natural number $B$ and every bounded complex $K$ of bound $B$, the exact complexity of the image of $K$ under the forgetful map to exact complexes equals the (capped) complexity of $K$.
background
This module reorganizes the quotient-class path-sum configuration space into exact complexity shells with no size caps in the shell definition, then proves that a shell-resummed path sum with an explicit Gaussian UV regulator $\exp(-\rho n^2)$ converges for every $\rho>0$. The regulator and the action/phase are mathematical parameters, not derived physics; regulator removal remains a named open.
A BoundedComplex B is a labeled complex whose vertex/edge/triangle counts are capped by $B$. The forgetful map sends it to an ExactComplex (cap-free). Complexity is the natural size measure on either side (vertex/edge/triangle data). Exact complexity is the same measure read on the uncapped type. Sibling facts already record that complexity is relabeling-invariant and that exact classes form a setoid under global relabeling.
The local Stage-1 goal is to treat exact shells ExactPathClass n as finite types with an entropy bound, so that regulated shell series can be summed. Transporting complexity across the forgetful map is the bookkeeping step that lets capped and uncapped counts speak the same language.
proof idea
One-line term proof by rfl. Exact complexity of the forgetful image is defined so that it coincides with the capped complexity on the nose; no lemma application or rewriting is required.
why it matters
Stage 1 of the Seven Gaps exact-shell program needs complexity to be stable when one drops the artificial size cap and works in the genuine exact class. This identity is that stability statement. It sits next to relabeling invariance of complexity and the exact-setoid structure, and it underwrites the shell entropy bound: the number of combinatorially distinct exact complexes of complexity $n$ is at most $(n+1)^{12(n+1)}$.
No downstream theorem currently lists this declaration as a direct dependency in the graph, but the surrounding shell machinery (Fintype instances on exact path classes, modulus bounds on regulated shell terms, summability of the UV series) presupposes that complexity labels agree after forgetting caps. Honesty constraints from the module still apply: nothing here is continuum limit, mesh refinement, or regulator removal; those ledger flags stay red.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.