swap01_apply_zero
plain-language theorem explainer
On Fin n with n>1, the 0↔1 edge-label transposition sends index 0 to index 1. Anyone evaluating the Gap-2 twist (edge relabel by that transposition) on the zero edge cites this. The proof unfolds the conditional definition, takes the 1<n branch, and applies the standard left-swap identity.
Claim. Let $n\in\mathbb{N}$ with $1<n$ (hence also $0<n$). Write $\sigma_n$ for the permutation of $\{0,\ldots,n-1\}$ that swaps $0$ and $1$ when $1<n$ and is the identity otherwise. Then $\sigma_n(0)=1$.
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 count while individual terms differ. The module settles this in the witness direction via an edge-label involution.
The device is twist: relabel a bounded complex by transposing edge letters 0 and 1. That transposition is packaged as a bare permutation of Fin n (stated on n rather than on the complex's edge count so that twist-of-twist reduces cleanly). When $1<n$ it is the swap of 0 and 1; otherwise it is the identity.
This lemma records the elementary evaluation of that permutation at 0. Downstream, the twist's action on edge keys is reduced to this evaluation.
proof idea
Term-mode, three steps. Unfold the definition of the Fin-n transposition. Rewrite with the positive branch of the decidable 1 < n test (hypothesis h), so the goal becomes the left action of Equiv.swap on the pair of Fin points 0 and 1. Close by Equiv.swap_apply_left.
why it matters
The non-equivariant witness needs a concrete involution of the labeled carrier that preserves gauge classes and splits orbits into cancelling halves. The 0↔1 edge transposition is that involution; evaluating it at the zero edge is the first arithmetic step.
Parent use is keyAt_twist_zero: under $1 < K.nE$, the key at edge 0 of the twisted complex equals the key at edge 1 of the original. That identity is exactly this lemma fed into the general keyAt_twist congruence. From there the sign that flips under the twist, and the orbit-mean-one but non-constant numerator, become checkable.
In the broader Gap-2 story this is scaffolding arithmetic inside the witness that non-equivariant costs can post $\mu$ with numerator not identically one, the case left open by the equivariant posting theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.