relax
plain-language theorem explainer
Cap relaxation embeds any bounded incidence complex at bound B into the larger-bound class at any B' ≥ B, leaving vertex/edge/tet counts and incidence maps unchanged. Gravity and path-sum authors cite it to move fixed witnesses (e.g. one tetrahedron) across caps without rewriting data. The construction is a structure copy that only re-proves the three size inequalities by transitivity of ≤.
Claim. If $B \le B'$ and $K$ is a bounded incidence complex with cap $B$ (vertex, edge, and tetrahedron counts each at most $B$), then the same incidence data defines a bounded complex with cap $B'$: counts and edge/tet vertex maps are identical, and the three bound inequalities hold by transitivity of $\le$.
background
In the SevenGaps path-sum setup, a bounded complex at cap $B$ is a finite incidence configuration: counts $n_V, n_E, n_T \le B$, plus maps listing the two endpoints of each edge and the four vertices of each tetrahedron. The superclass is garbage-inclusive (degenerate edges, missing skeleton edges, repeated tet vertices are allowed). This module carves out the simplicial subclass by four combinatorial conditions: distinct edge endpoints, no multi-edges as unordered pairs, four distinct tet vertices, and skeleton closure (every tet pair appears as an edge).
Caps are bookkeeping: the same geometric configuration can sit under many $B$. Cap relaxation is the canonical inclusion of the $B$-capped class into every larger-cap class. Only the three inequalities $n_V, n_E, n_T \le B'$ need work; they follow from $n_\bullet \le B$ and $B \le B'$ via le_trans. Incidence fields are copied definitionally.
The local Phase 0b goal is a nonempty finite simplicial subclass with a genuine 3D witness, not only the empty complex.
proof idea
Definitional structure construction, not a tactic proof. Copy $n_V, n_E, n_T$, edgeVerts, and tetVerts from the input complex. Discharge the three bound fields by le_trans on the original inequalities $n_\bullet \le B$ with the hypothesis $B \le B'$. No rewriting of incidence data; equality of those fields is definitional.
why it matters
Without relaxation, every simplicial witness would be locked to one numeric cap. Downstream, relax_isSimplicial shows the simplicial predicate is invariant (it reads only incidence, which is preserved definitionally). That feeds exists_simplicial_with_tet: for every $B \ge 6$, relax the explicit one-tetrahedron complex (full 1-skeleton) to cap $B$, proving the simplicial subclass is nonempty for dimensional reasons, not only via the empty complex.
In ExactShellGaugeUV, toExact_relax records that the map to the cap-free exact class identifies all relaxed copies (definitional equality), so path-sum complexity is cap-independent. This is pure combinatorial scaffolding for the gravity/path-sum configuration class; it does not itself invoke J-cost, $\varphi$, or the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.