edgeSign
plain-language theorem explainer
Assigns each labeled complex a real sign by comparing the packed endpoint keys of its first two edge letters, returning 0 when fewer than two edges exist. This is the sole label-dependent (non class-invariant) ingredient in the Gap-2 non-equivariant posting witness. Downstream proofs use it to build a twist-odd tilted numerator whose orbit mean is one while individual terms need not be. The body is a one-line conditional on edge count composed with the antisymmetric comparison.
Claim. For a bounded labeled complex $K$, define $\mathrm{edgeSign}(K) \in \mathbb{R}$ by comparing the packed endpoint keys of edge letters $0$ and $1$: if $K$ has more than one edge, return $+1$, $-1$, or $0$ according as $\mathrm{key}_0 < \mathrm{key}_1$, $\mathrm{key}_1 < \mathrm{key}_0$, or equality; otherwise return $0$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ when its Boltzmann numerator is not identically one. The equivariant route forces the numerator to be constant on each gauge orbit, so orbit-mean one collapses to identically one. Without equivariance, mean one with non-constant terms is possible if an orbit splits into cancelling halves.
The module builds that split via an involution twist that swaps edge letters 0 and 1 while preserving gauge class. The comparison sign of two naturals is the difference of indicators ($+1$ if $x<y$, $-1$ if $y<x$, $0$ if equal), deliberately written so swapping arguments is a one-line ring identity. Endpoint keys pack each edge's vertex pair into a single natural, total in the letter index, and vanish when the letter is absent.
edgeSign is the only place the witness reads a label rather than a class invariant: it feeds the first two keys into that comparison, or returns zero on complexes with fewer than two edges.
proof idea
Definitional one-liner. If the edge count exceeds one, apply the antisymmetric natural comparison to the packed keys of letters 0 and 1; otherwise return zero. No lemmas are invoked at the definition site; subsequent theorems unfold this conditional and invoke key-transport under twist together with the swap identity for the comparison.
why it matters
This is the label-reading hinge of the Gap-2 witness. The twist-flip theorem shows the sign negates under edge-letter transposition, so any real function built as an odd function of the sign (in particular the tilted numerator $1 + t\cdot\mathrm{edgeSign}$) is twist-odd. The cancellation lemma then forces its class mass to vanish, which is exactly the surplus needed for orbit-mean one without pointwise one.
Downstream, the tilted numerator, its positivity and mean-one identities, the explicit evaluation on the loop-and-bridge complex, and the hostile probe that a constant tilt of one breaks the identity all route through this definition. It closes the open case left by the equivariant posting theorem: non-equivariant costs can post $\mu$ with non-unit individual Boltzmann factors, via a one-parameter family controlled by this sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.