complexity_congr
plain-language theorem explainer
Equivalent bounded complexes (related by combinatorial relabeling) have equal complexity. Anyone building exact complexity shells or the Gaussian-UV path sum cites this to push the shell index through the quotient. The proof unpacks the equivalence to a single relabeling and rewrites the three size counts that define complexity.
Claim. Let $B\in\mathbb{N}$ and let $K,K'$ be bounded complexes of bound $B$. If $K$ and $K'$ are equivalent under combinatorial relabeling, then their complexities agree: $\mathrm{complexity}(K)=\mathrm{complexity}(K')$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells and studies a Gaussian-UV-regularized path sum. Stage 1 is pure shell structure: complexity must be constant on relabeling classes before one can form shells and count them.
A bounded complex of bound $B$ is a finite combinatorial complex (vertices, edges, tetrahedra, with incidence data) subject to size caps. Its complexity is the scalar built from the three size counts $n_V$, $n_E$, $n_T$. Equivalence means there exists a relabeling (bijections on the three strata compatible with incidence) taking one labeled complex to the other.
The sibling facts used here state exactly that any such relabeling preserves the three counts: $n_V$, $n_E$, and $n_T$ are unchanged. Complexity is therefore a function of those invariants alone.
proof idea
Short tactic proof. From the equivalence hypothesis, obtain a concrete relabeling witness $r$. Unfold the definition of complexity (so the goal is equality of an expression in $n_V,n_E,n_T$). Rewrite with the three preservation lemmas for that relabeling: vertex count, edge count, and tetrahedron count each match on the two sides, and the goal closes.
why it matters
This is THEOREM (S1a) in the module's Stage 1 list: complexity is a relabeling invariant. Downstream it is named explicitly under the shell_structure_proved flag of ExactShellGaugeUVStatus, which packages the grounded Stage-1 kernel (together with the exact setoid, the Fintype instance on exact path classes, shell-index uniqueness, and the relax map into the exact class).
Without this congruence, complexity would not descend to equivalence classes, and the exact shells used by the regulated path sum could not be indexed cleanly. The module is careful about honesty: the Gaussian regulator is inserted by hand, the phase is a free class-invariant parameter, and regulator removal plus continuum limit remain open; this lemma only closes the combinatorial invariance step, not those physics claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.