keyAt_loopAndBridge_one
plain-language theorem explainer
On the three-vertex loop-and-bridge complex, the packed endpoint key of edge letter 1 equals 5. Gravity and Gap-2 readers cite it when assembling the edge-sign witness that a non-equivariant letter cost can still post mu. The proof is a one-line decidability check on the finite complex data.
Claim. Let $K$ be the bounded complex on three vertices with two edges (one loop and one proper bridge). Packing the ordered endpoint pair of edge letter $1$ into a single natural number via $v_1\cdot 3 + v_2$ yields $5$.
background
Gap 2 asks whether a letter cost can post the measure factor $\mu$ even when it is not equivariant, so its Boltzmann numerator need not be identically one. The module settles the witness direction: a one-parameter family does post $\mu$ with orbit-mean-one but non-constant numerator.
The device is an edge-label transposition on labeled complexes. To build a sign that flips under that transposition one needs a concrete complex whose two edge letters attach to different endpoint pairs. loopAndBridge is that complex: three vertices, two edges (one loop, one proper edge), no triangles.
keyAt K i packs the ordered endpoint pair of edge letter $i$ into one natural: $v_1\cdot B + v_2$ when the letter exists, else $0$. Here $B=3$. The packing is total in the letter index by design.
proof idea
One-line wrapper: by decide. Lean evaluates the finite BoundedComplex 3 data for loopAndBridge (two edges, concrete edgeVerts) and checks that the packed key at letter index 1 equals 5. No lemmas beyond the definitions of keyAt and loopAndBridge are required.
why it matters
Feeds edgeSign_loopAndBridge, which unfolds the edge-sign on this complex and rewrites both keyAt facts (letters 0 and 1) before a numeric comparison of the packed keys. That sign is the witness ingredient showing a non-equivariant cost can split an orbit into cancelling halves while keeping orbit-mean numerator one, hence still post $\mu$.
In the Gap-2 story this closes the case left open by the equivariant posting theorem: equivariance forced constancy on orbits, and mean-one plus constancy gave identically one. Here constancy fails, mean-one survives, and posting still holds. The result is local bookkeeping inside the gravity seven-gaps ladder, not a T0–T8 forcing step, but it removes an obstruction on the posting-cost route to the measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.