relabel_nT_eq
plain-language theorem explainer
A relabeling of two B-bounded complexes forces equal tetrahedron counts. Anyone treating complexity as a shell coordinate, or building quotient path-sum shells, cites this as the tet half of the invariance. The proof is a short Fintype cardinality transfer through the tetrahedron bijection of the relabeling.
Claim. Let $K$ and $K'$ be $B$-bounded complexes and let $r$ be a relabeling between them (compatible bijections on vertices, edges, and tetrahedra). Then the tetrahedron counts agree: $n_T(K) = n_T(K')$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies a Gaussian-UV-regularized path sum. Honesty tags in the module doc stress that the regulator is inserted by hand, the action/phase is a free parameter on classes, and regulator removal remains a named open.
A BoundedComplex B is a labeled finite complex with vertex, edge, and tetrahedron counts at most $B$. Complexity is the shell coordinate: the max of those three counts. A relabeling supplies bijections on the three finite index types (including a tetrahedron equivalence) compatible with incidence data.
The tetrahedron count $n_T$ is the free label that enters that max. Parallel lemmas already force equal vertex and edge counts under relabeling; this is the tet counterpart.
proof idea
Term-mode proof in three steps. Apply Fintype.card_congr to the tetrahedron equivalence r.tEquiv of the relabeling, obtaining equality of Fintype.card on the two tet index types. Simplify with Fintype.card_fin so both sides become the underlying Fin cardinals, which are exactly K.nT and K'.nT. Discharge by that equality. No induction and no simpliciality hypotheses.
why it matters
Stage 1 of the exact-shell program needs complexity to be a well-defined function on relabeling classes. This lemma is the tetrahedron leg of that invariance: complexity_congr (THEOREM S1a) unfolds complexity and rewrites by the three count equalities, including this one. Downstream, boundedToShell_congr in the cap-shell bridge uses the same count equalities so the forward labeled map respects bounded relabeling.
Without equal $n_T$, the exact path class at complexity $n$ would not be stable under the setoid, and the Fintype/entropy bounds on shells would not descend to classes. The module still does not claim continuum limits or physical regulator removal; those stay open. This is pure combinatorial invariance inside the shell scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.