Chord re-pairing parity: the bridge and the crossing table

Three pieces of pure order-combinatorics glue on top of the two coexisting crossing predicates:

• the bridge between the cut-style predicate CrossesCut (ChordParity.lean) and the chord-style predicate ChordPairCross (PathLedger.lean), under the normalization hypotheses of chordPairCross_iff_xor;
• the mutual-crossing table for four strictly ordered points in ChordPairCross vocabulary — parallel and nested chords do not cross, interleaved chords do;
• the summed transfer: over a finite family of normalized third chords avoiding the four points, re-pairing two chords preserves the total crossing parity (third_chord_reparity per element).

The bridge between the two crossing predicates

theorem RS.crossesCut_iff_chordPairCross {α : Type} [LinearOrder α] {x y u w : α} (huw : u < w) (hux : u ≠ x) (hwy : w ≠ y) : CrossesCut x y (u, w) ↔ ChordPairCross x y u w

The bridge: the cut-style crossing predicate of ChordParity.lean agrees with the chord-style crossing predicate of PathLedger.lean, for a chord recorded low-to-high whose ends avoid the matching ends of the cut.