toExact_relax
plain-language theorem explainer
Relaxing a size cap on a bounded complex leaves its exact (cap-free) image unchanged by definitional equality. Exact-shell path-sum work cites this to identify all capped copies of one incidence configuration. The proof is pure reflexivity of the forgetful map.
Claim. If $B \le B'$ and $K$ is a complex with vertex/edge/tetrahedron counts bounded by $B$, then forgetting the cap after relaxing $K$ to the larger bound $B'$ yields the same exact complex (same incidence data, no cap in the type) as forgetting the cap of $K$ itself.
background
This module organizes quotient-class path-sum configuration space into exact complexity shells with no size caps in the shell definition, and studies a Gaussian-UV-regulated path sum. Honesty constraints are binding: the regulator $\exp(-\rho n^2)$ is inserted by hand, the action/phase is a free parameter on classes, and regulator removal ($\rho \to 0^+$) remains a named open.
A bounded complex carries vertex, edge, and tetrahedron counts capped by some $B$. Its complexity is $\max(n_V,n_E,n_T)$, the shell coordinate. The forgetful map sends a bounded complex to an exact complex with the same incidence data; the target type does not mention $B$. Cap relaxation embeds a $B$-bounded complex into a larger bound $B' \ge B$ without changing incidence.
Exact complexes and their independent relabeling equivalence form the setoid underlying exact path classes. Cap-free shells are the objects that later receive the per-class measure and the regulated shell series.
proof idea
One-line term proof by rfl. Both sides build an exact complex by copying edgeVerts and tetVerts from the underlying labeled data. Cap relaxation only widens the bound parameter and does not touch incidence fields, so the two forgetful images are definitionally equal.
why it matters
Stage 1 of the exact-shell program needs cap-independence: shells are defined without size caps, so every capped presentation of the same configuration must land on one exact image. This theorem is listed among the kernel results grounding the status flag shell_structure_proved on ExactShellGaugeUVStatus (alongside complexity congruence, the exact setoid, finiteness of shells, and uniqueness of the shell index).
It is bookkeeping, not continuum physics. The module explicitly keeps continuum-limit and full-theory ledger flags false: complexity cutoffs are not mesh refinement. The result still matters locally because the regulated path sum is summed over exact classes; without cap collapse, the same geometric configuration would be double-counted under different artificial bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.