edgeSign_cases
plain-language theorem explainer
For every bounded complex the edge sign takes values in {1, −1, 0}. Anyone building the tilted-numerator witness for non-equivariant posting of μ cites this trichotomy. The proof is a case split on edge count: fewer than two edges forces zero; otherwise it reduces to the two-argument sign lemma.
Claim. For every bounded complex $K$, the edge sign of $K$ equals $1$, equals $-1$, or equals $0$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor μ with a Boltzmann numerator that is not identically one, by making the orbit sum of the factors equal the orbit count while individual terms differ. The module answers in the witness direction: an edge-label transposition (twist, swapping letters 0 and 1) splits orbits into cancelling halves.
The edge sign is the discrete weight that records how a labeled complex sits relative to that transposition. On complexes with fewer than two edge letters it is defined to be silent (value 0); that is the scope clause of the whole construction. The sibling two-argument comparison sign supplies the ±1 values once at least two edge letters are present.
Upstream, the posting identity already reduces “posts μ” to “numerator has orbit mean one” with no equivariance hypothesis. Equivariance would force the numerator constant on orbits, hence identically one; the sign device is what lets mean one hold without constancy.
proof idea
Unfold the definition of the edge sign. Case on whether the complex has strictly more than one edge letter.
If yes, the definition reduces to the two-argument comparison sign, and the sibling trichotomy for that sign supplies the claim.
If no, the definition is the constant zero branch, so the third disjunct holds by reflexivity.
why it matters
The immediate parent is the positivity lemma for the tilted numerator: that proof cases on this trichotomy and finishes each branch by linear arithmetic under the tilt bound |t| < 1. Positivity is required before the cancellation identity (a complex and its twist carry numerators averaging to one) can be stated cleanly.
In the Recognition gravity stack this closes the remaining Gap-2 case left open by the equivariant posting theorem and by the floor module’s exhibition of a non-equivariant cost class. It is local scaffolding for the witness family, not a forcing-chain landmark (T0–T8), but it is what makes non-constant orbit-mean-one numerators constructible rather than conjectural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.