keyAt_loopAndBridge_zero
plain-language theorem explainer
On the three-vertex loop-and-bridge complex, the packed endpoint key of edge letter 0 is zero (the loop at vertex 0). Anyone computing the edge sign for the non-equivariant posting witness cites this fact. The proof is a one-line kernel decision on the concrete complex data.
Claim. Let $K$ be the three-vertex bounded complex with one loop edge $(0,0)$ and one proper bridge edge $(1,2)$. The packed endpoint key of edge letter $0$ on $K$ equals $0$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the class measure $\mu$ with a Boltzmann numerator that is not identically one. The module answers in the witness direction: a one-parameter tilted cost does so, by making the numerator have orbit mean one without being constant on orbits.
The witness complex is loopAndBridge: three vertices, two edges (a loop at $0$ and a bridge from $1$ to $2$), no triangles. The endpoint-key map packs the ordered pair of vertex indices of edge letter $i$ into a single natural as $u\cdot B+v$, or returns $0$ if letter $i$ is absent. For this complex $B=3$, so the loop $(0,0)$ packs to $0$ and the bridge $(1,2)$ packs to $5$.
Those two keys feed the edge-sign that splits the orbit under the $0\leftrightarrow 1$ letter transposition, producing the non-constant numerator $1+t$.
proof idea
One-line computational proof: decide evaluates the definition of the endpoint-key map on the concrete loopAndBridge data at letter index $0$. The edge exists, its endpoints are both vertex $0$, and $0\cdot B+0=0$.
why it matters
This is a tiny but load-bearing arithmetic fact in the non-equivariant posting witness. Downstream, edgeSign_loopAndBridge rewrites the edge-sign definition through this zero key and the companion key $5$ at letter $1$, then evaluates the sign comparison to obtain $+1$. That sign makes the tilted numerator $1+t$ rather than $1$, so the orbit mean can be one while individual Boltzmann factors differ.
In the Gap 2 story this closes the case left open by the equivariant posting theorem: equivariant costs post $\mu$ only when the numerator is identically one, but a non-equivariant cost can post $\mu$ with a non-constant numerator of orbit mean one. The loop-and-bridge complex is the smallest carrier on which the two edge letters must carry different endpoint keys, forcing a nontrivial sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.