edgeSign_loopAndBridge
plain-language theorem explainer
On the minimal loop-and-bridge complex (three vertices, two edges), the edge-label sign equals +1: the first edge key is strictly less than the second. Anyone building the non-equivariant posting witness or its tilt/twist probes cites this evaluation. The proof unfolds the sign, inserts the two decided key values, and finishes by numeric comparison.
Claim. Let $K_0$ be the bounded complex with three vertices and two edges (one loop and one bridge). Writing $\mathrm{edgeSign}(K)$ for the comparison sign of the endpoint keys of the first two edge letters of $K$ (and $0$ if fewer than two edges), one has $\mathrm{edgeSign}(K_0)=1$.
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 answers in the witness direction: posting $\mu$ is exactly orbit-mean-one of the numerator, a strict weakening of "identically one"; equivariance forced constancy, which is what fails here.
The witness reads labels only through $\mathrm{edgeSign}$: if the complex has more than one edge, compare the keys at edge letters $0$ and $1$ via $\mathrm{sgnLt}$ (indicator difference: $+1$ if $x<y$, $-1$ if $y<x$, else $0$); otherwise return $0$. That is the sole non-class-invariant input to the tilted cost.
The complex $K_0=\mathrm{loopAndBridge}$ is the smallest example whose two edge letters must be charged differently by a centered cost: $n_V=3$, $n_E=2$, $n_T=0$. Upstream facts fix its keys: $\mathrm{keyAt}(K_0,0)=0$ and $\mathrm{keyAt}(K_0,1)=5$.
proof idea
Unfold $\mathrm{edgeSign}$. The guard $1<n_E(K_0)$ holds by decide on the concrete edge count $2$, so the definition reduces to $\mathrm{sgnLt}(\mathrm{keyAt},K_0,0,,\mathrm{keyAt},K_0,1)$. Rewrite with the two decided key lemmas ($0$ and $5$), unfold $\mathrm{sgnLt}$, and close by norm_num: $0<5$ yields $+1$.
why it matters
This single evaluation is the base orientation of the witness complex. Downstream, tiltedNumer_loopAndBridge rewrites the tilted numerator at $K_0$ to $1+t$, so any nonzero tilt is visibly non-unit: the open non-equivariant case is inhabited. Hostile probes reuse it twice: probe_twist_moves_loopAndBridge shows twist genuinely moves $K_0$ because $\mathrm{edgeSign}$ flips under twist and cannot equal its own negative when the value is $+1$; probe_tilt_one_breaks_the_identity uses the flipped sign $-1$ at the twist to show that $|t|<1$ is load-bearing (at $t=1$ the twisted numerator hits $0$, which no exponential equals).
In the Gap 2 chain this pins the concrete half of the canceling orbit pair that lets mean-one hold without pointwise one, closing the case left open by the equivariant posting theorem and the non-equivariant floor example.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.