The four-label parity identities

The per-step sign parity of the canonical-route ledger reduces to two pure order-combinatorics identities on four distinct labels: x, xb (old partners) and y, yb (old partners), the step re-pairing to the new chords {x, y} and {xb, yb}. The canonical direction at a u-end is "u's old partner < u", and the step is separated exactly when the directions at the x-end and the y-end differ. In the separated case the two anti-canonicality indicators of the new chords (each read at its recorded end) plus the step's intrinsic sign match the crossing change mod 2; in the non-separated case the y-side directions are toggled by the anchor flip, whose own flip cancels the intrinsic sign, leaving the bare toggled count.

Both identities are pure order case-bashes: six Ne.lt_or_lt splits, transitivity pruning of the intransitive tournaments (a tournament on four vertices is transitive iff it has no directed triangle), and a uniform decision of all indicators from the six resolved comparisons.

theorem RS.fourLabel_parity_sep {α : Type} [LinearOrder α] {x xb y yb : α} (hxxb : x ≠ xb) (hyyb : y ≠ yb) (hxy : x ≠ y) (hxyb : x ≠ yb) (hxby : xb ≠ y) (hxbyb : xb ≠ yb) (hsep : (xb < x) ≠ (yb < y)) : (((if if x < y then xb < x else yb < y then 1 else 0) + if if xb < yb then x < xb else y < yb then 1 else 0) + 1) % 2 = ((if chordPairCrossSym (x, xb) (y, yb) then 1 else 0) + if chordPairCrossSym (x, y) (xb, yb) then 1 else 0) % 2

The separated four-label parity identity: when the canonical directions at the x-end and the y-end differ, the two anti-canonicality indicators of the new chords plus the intrinsic sign of the step match, mod 2, the crossing change of the re-paired chords.

theorem RS.fourLabel_parity_nonsep {α : Type} [LinearOrder α] {x xb y yb : α} (hxxb : x ≠ xb) (hyyb : y ≠ yb) (hxy : x ≠ y) (hxyb : x ≠ yb) (hxby : xb ≠ y) (hxbyb : xb ≠ yb) (hsame : (xb < x) = (yb < y)) : ((if if x < y then xb < x else ¬yb < y then 1 else 0) + if if xb < yb then x < xb else ¬y < yb then 1 else 0) % 2 = ((if chordPairCrossSym (x, xb) (y, yb) then 1 else 0) + if chordPairCrossSym (x, y) (xb, yb) then 1 else 0) % 2

The non-separated four-label parity identity: when the canonical directions at the x-end and the y-end agree, the anchor flip toggles the y-side directions and cancels the intrinsic sign, so the bare toggled anti-canonicality count matches, mod 2, the crossing change of the re-paired chords.