keyAt
plain-language theorem explainer
Packs the ordered endpoint pair of edge letter i into one natural number (source times vertex bound plus target), or 0 if i is out of range. Downstream edge-sign and twist lemmas cite it as the label-sensitive key that makes a cost non-equivariant. The body is a single dependent if on the edge count.
Claim. Fix a vertex bound $B$ and a bounded complex $K$ with $n_E$ edge letters. For $i \in \mathbb{N}$, if $i < n_E$ and the $i$-th edge has endpoints with values $(u,v)$, the key is $u\cdot B + v$; otherwise the key is $0$. The map is total in $i$ by design.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure $\mu$ with a Boltzmann numerator that is not identically one, by having orbit-mean one without constancy. The equivariant route is already closed: posting $\mu$ is exactly numerator orbit-mean one, and equivariance forces the numerator constant on orbits, hence identically one.
This module builds a witness via an edge-letter transposition twist (swap letters 0 and 1) that preserves gauge classes and is an involution. To get a real function that flips under twist, one needs a label-sensitive comparison of the first two edges. That comparison reads packed endpoint keys rather than class invariants.
A bounded complex $K$ carries an edge list edgeVerts of length $n_E$. Each entry is an ordered pair of vertices in a finite type of size $B$. Packing $(u,v)$ as $u\cdot B + v$ is injective on pairs with values in ${0,\ldots,B-1}$, so distinct endpoint pairs get distinct keys.
proof idea
Pure definition: a dependent if on $i < K.n_E$. In range, project the $i$-th edge pair, take .val on each endpoint, and form source times $B$ plus target. Out of range, return 0. No lemmas; the companion keyAt_of_lt is the dif_pos unfolding.
why it matters
This is the only place the Gap-2 witness reads a label rather than a class invariant. edgeSign compares keyAt K 0 with keyAt K 1 (via sgnLt), and edgeSign_twist shows the sign flips under the letter-0/1 transposition because keys swap and comparison is antisymmetric. That oddness feeds classMass_of_twistOdd: any real function negated by twist has class mass zero, which is the cancellation engine for a one-parameter tilted cost whose numerator has orbit mean one without being identically one.
Concrete checks on the loopAndBridge complex (keyAt_loopAndBridge_zero/one) pin the witness geometry. Together these close the open non-equivariant posting case named by Gap2PostingLayerFloor and the equivariant posting-cost derivation: non-equivariant costs can post $\mu$ with non-constant numerators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.