edgeRelabel
plain-language theorem explainer
Edge-index renaming on a bounded complex: apply a permutation of the edge labels while freezing vertex counts, tetrahedron data, and incidence pairs. Gauge motion at the labeled level. Builds the twist involution that splits orbits for the non-equivariant posting witness. Proof shape is a pure structure copy with edgeVerts precomposed by the permutation.
Claim. Given a bounded complex $K$ on bound $B$ with $n_E$ edges and a permutation $\sigma$ of $\{0,\ldots,n_E-1\}$, the edge-relabeled complex has the same vertex, edge, and tetrahedron counts (and the same size bounds and tetrahedron-vertex map), while its edge-incidence map is $e \mapsto K.\mathrm{edgeVerts}(\sigma(e))$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ when its Boltzmann numerator is not identically one, by making the orbit sum of those factors equal the orbit count while individual terms differ. The sharp condition is orbit mean one of the numerator; equivariance forces constancy on orbits, hence mean one collapses to identically one.
A BoundedComplex B is a finite labeled complex (vertex, edge, and tetrahedron counts with bounds, plus incidence maps edgeVerts and tetVerts). Gauge equivalence identifies complexes that differ only by relabeling. The module needs an involution of the labeled carrier that stays inside each gauge class, so orbit sums can cancel in pairs.
edgeRelabel is that labeled-level gauge motion: rename edges by any permutation of the edge index set, leave vertices and tets alone. The Freudenthal-style edgeVerts maps elsewhere in the tree are unrelated incidence tables; here the name is the complex's own edge-incidence field.
proof idea
Definition by structure fields, not a tactic proof. Copy nV, nE, nT and the three bound hypotheses from $K$. Keep tetVerts unchanged. Set the new edge incidence to K.edgeVerts \circ \sigma, so edge letter $e$ inherits the incidence pair formerly attached to $\sigma(e)$. No lemmas are invoked; well-typedness is immediate from $\sigma : \mathrm{Perm}(\mathrm{Fin}, K.nE)$.
why it matters
This is the primitive gauge motion behind the witness that closes Gap 2 in the non-equivariant direction. Downstream, twist is the special case that swaps edge letters $0$ and $1$ via edgeRelabel K (swap01 K.nE). The theorem twist_twist then shows the twist is an involution, because renaming by $\sigma\circ\sigma=\mathrm{id}$ recovers $K$, so the twist is a permutation of the labeled carrier along which class sums reindex.
Together with class-mass identities (classMass_postedWeight, mu_eq_orbitCard_mul_gibbsWeight), that involution lets a sign-flipping cost average to orbit mean one without being constant on orbits. The equivariant collapse (orbitMeanOne_forces_one_of_invariant) is thereby isolated as mean one plus constancy; only constancy fails for the witness family. No T0–T8 forcing step is claimed here; the declaration is local scaffolding for the gravity posting-cost gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.