twistRel
plain-language theorem explainer
The edge-letter transposition (swap of labels 0 and 1) is a genuine relabeling from any bounded complex to its twist: identity on vertices and tetrahedra, with incidence preserved. Anyone working the Gap-2 non-equivariant posting witness cites this to keep the twist inside a single gauge class. The construction is a structure instance: edge commutation reduces to involutivity of the swap, and tetrahedron commutation is reflexivity.
Claim. For every bounded complex $K$, the map that fixes vertices and tetrahedra and swaps edge letters $0$ and $1$ is a relabeling $K\to\mathrm{twist}(K)$: the two incidence-commutation identities hold, so the twisted complex lies in the same gauge class as $K$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ with a Boltzmann numerator that is not identically one. The module answers in the witness direction by building an involution on labeled carriers that preserves gauge classes and splits orbits into cancelling halves.
That involution is twist: transpose edge letters 0 and 1 via swap01, leaving vertices and tetrahedra fixed. A relabeling is a triple of equivalences (vertices, edges, tetrahedra) that commute with the incidence maps edgeVerts and the tetrahedron attachment. The present declaration supplies exactly those data from $K$ onto $\mathrm{twist}(K)$.
The surrounding sharp criterion is already settled for every cost: posting $\mu$ is equivalent to the numerator having orbit mean one. Equivariant costs force the numerator constant on orbits, hence identically one; the twist is the device that lets mean-one hold without constancy.
proof idea
Structure instance for Relabel K (twist K). Vertex and tetrahedron equivalences are Equiv.refl. The edge equivalence is swap01 on the edge index set of $K$. Edge commutation is the identity edgeVerts(\mathrm{swap}(\mathrm{swap}\, e))=\mathrm{edgeVerts}(e)$, discharged by rewriting with involutivity of swap01`. Tetrahedron commutation is definitional reflexivity.
why it matters
This is the gauge-class membership half of the Gap-2 witness. Downstream, twist_equivalent packages it as $K\sim\mathrm{twist}(K)$, and tiltedCost_not_equivariant feeds twistRel loopAndBridge into history-cost invariance to prove the tilted one-parameter family is label-asymmetric: cost differs on a pair of gauge-equivalent complexes, so the cost is not equivariant.
Together with twist_twist (involution) and the orbit-mean-one criterion, it closes the open case left by the equivariant posting theorem: a non-equivariant cost can post $\mu$ with non-constant numerator. In the Recognition gravity stack this is the concrete mechanism that separates "mean one" from "identically one" on gauge orbits of bounded complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.