keyAt_twist
plain-language theorem explainer
Reading an edge key on a twisted labeled complex equals reading the key of the transposed edge index on the original complex. Anyone tracking the Gap-2 non-equivariant posting witness cites this when moving endpoint keys across the 0↔1 letter swap. The proof unfolds the key formula on both sides and uses that twist acts by swap01 on edge indices.
Claim. Let $K$ be a bounded labeled complex with edge bound $B$, and let $i,j$ be edge indices below the edge count of $K$. If the $0\leftrightarrow 1$ index transposition sends $i$ to $j$, then the endpoint key of edge $i$ on the twisted complex equals the endpoint key of edge $j$ on $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: an edge-label transposition twist swaps letters $0$ and $1$ on a labeled complex, preserves gauge class, and is an involution, so orbits can split into cancelling halves with mean one.
A key at an edge index packs the two endpoint vertex values into a single natural number (first endpoint times $B$ plus second). The twist of $K$ has the same edge count; its edge-vertex table is the original table read after the index map swap01. The present lemma is the bookkeeping step that moves keys across that relabeling for an arbitrary exchanged pair $(i,j)$.
Upstream, keyAt_of_lt is the definitional expansion of the key under an edge-index bound; swap01 is the concrete transposition of the first two edge slots used to build the twist.
proof idea
Tactic proof in four short steps. First, the edge-count bound for $i$ transfers unchanged to the twisted complex. Expand both sides by keyAt_of_lt: each key is first-endpoint value times $B$ plus second-endpoint value. The remaining identity is that the twisted edge-vertex pair at $i$ equals the original pair at $j$; that follows by unfolding the definition of twist (edgeVerts composed with swap01) and rewriting with the hypothesis that swap01 sends $i$ to $j$. Substitute the three equalities.
why it matters
This is the general transposition lemma for endpoint keys under the Gap-2 witness involution. Downstream, keyAt_twist_zero and keyAt_twist_one are the two one-line specializations (indices $0$ and $1$), which feed the sign of a labeled complex: the comparison of the first two edge keys, designed to flip under twist.
That sign flip is what lets a non-constant numerator still have orbit mean one, closing the open case left by the equivariant posting theorem (equivariant_posts_mu_iff_numerator_one) and by the floor module's exhibition of a non-equivariant cost class. In the broader Seven Gaps gravity program, it is scaffolding for the non-equivariant half of the posting-cost derivation rather than a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.