keyAt_twist_zero
plain-language theorem explainer
If a bounded complex has at least two edges, the packed endpoint key of letter 0 on the 0–1 edge transposition equals the key of letter 1 on the original complex. Gravity Gap-2 arguments that track how edgeSign transforms under twist cite this specialization. The proof is a one-line application of the general key-through-twist lemma plus the fact that swap01 sends 0 to 1.
Claim. Let $K$ be a bounded complex on the bichromatic interface $B$ with edge count $n_E(K)>1$. Write $\mathrm{twist}(K)$ for the complex obtained by swapping edge letters $0$ and $1$. Then the packed endpoint key of letter $0$ on $\mathrm{twist}(K)$ equals the packed endpoint key of letter $1$ on $K$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the census measure $\mu$ with a Boltzmann numerator that is not identically one. The module settles this in the witness direction by an involution twist that swaps edge letters 0 and 1 while preserving gauge class, so orbit means can cancel without every term being one.
The packed key keyAt K i encodes the ordered endpoint pair of edge letter $i$ as a single natural (or 0 if $i$ is out of range). The general lemma keyAt_twist states that reading a key through the twist reads the transposed letter: whenever swap01 sends index $i$ to $j$, one has keyAt (twist K) i = keyAt K j.
Here $B$ is the bichromatic ordered-edge interface of the polarized diamond field, and $n_E$ is the edge-count observable on the complex. The hypothesis $1 < n_E(K)$ guarantees both letters 0 and 1 exist, so the transposition is well-defined on those indices.
proof idea
From $1 < K.nE$ deduce $0 < K.nE$ by omega. Feed that bound, the given bound $1 < K.nE$, and the identity swap01_apply_zero (which says swap01 sends index 0 to index 1) into the general lemma keyAt_twist. The conclusion is exactly keyAt (twist K) 0 = keyAt K 1. No further rewriting is needed.
why it matters
This is the zero-index half of the key exchange used by edgeSign_twist, whose docstring records the parent claim: the twist exchanges edge letters 0 and 1, so it exchanges their keys, and the comparison is antisymmetric, yielding edgeSign (twist K) = -edgeSign K. That sign flip is the cancellation device for the non-equivariant posting witness: orbit halves cancel under the involution while the class is preserved.
In the Gap-2 forcing picture this closes the case left open by the equivariant posting theorem (mean-one plus constancy). Equivariant costs force the numerator to be identically one; the twist family shows mean one alone is enough when terms are allowed to vary. The result sits inside the gravity seven-gaps stack that feeds the Recognition census measure, not the T0–T8 geometric forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.