twist_edgeVerts
plain-language theorem explainer
On a bounded complex, twisting (transposing edge letters 0 and 1) moves edge-vertex incidence by the same transposition of edge indices: the twisted complex at e has the same endpoint pair as the original at swap01(e). Used when tracking how the Gap-2 twist involution acts on incidence data in the non-equivariant posting witness. Holds by definitional equality (rfl).
Claim. Let $K$ be a bounded complex over the bichromatic interface and let $e$ be an edge index in $\{0,\ldots,n_E(K)-1\}$. Write $\mathrm{twist}(K)$ for the complex obtained by transposing edge letters $0$ and $1$, and $\mathrm{swap}_{01}$ for that transposition on edge indices. Then the endpoint pair of $\mathrm{twist}(K)$ at $e$ equals the endpoint pair of $K$ at $\mathrm{swap}_{01}(e)$.
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, by making the orbit sum of numerator terms equal the orbit cardinality while individual terms differ. The module answers in the witness direction: mean-one numerators are exactly the posting condition, and equivariance was only supplying constancy on orbits.
The witness device is an involution twist of the labeled carrier that preserves gauge classes: it relabels by swapping edge letters 0 and 1 via edgeRelabel and the index map swap01. Two structural facts make the construction work: twist stays in the same class (it is a pure relabeling), and twist composed with itself is the identity, so it permutes the carrier.
edgeVerts here is the edge-to-endpoint incidence of the complex (which vertices bound each labeled edge), not the Finset-of-vertices helper from rung descent. The present lemma records how that incidence transforms under twist.
proof idea
Term-mode proof by rfl. Unfolding the definition of twist (edge relabeling by swap01 on the edge alphabet) makes the two sides of the equality definitionally identical: the twisted complex's incidence table is exactly the original table precomposed with the letter transposition on edge indices.
why it matters
This is a small structural identity in the Gap-2 non-equivariant posting apparatus. The module settles the open case left by the equivariant posting theorem: whether orbit-mean-one numerators can arise without pointwise-one factors. The twist involution splits orbits into canceling halves via a sign that flips under the 0-1 edge transposition; tracking incidence under that transposition is bookkeeping the witness needs.
No downstream consumers are recorded yet in the graph. Within the module it sits beside twist_twist (involution), class-mass identities, and the mean-one characterization of posting $\mu$. It does not itself touch the forcing chain (T5-T8) or the RCL; it is local gravity/posting-layer scaffolding for the seven-gaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.