2.10. Planar Boolean CSP Prerequisites🔗

Ordered cyclic differences are defined by Cslib.BitString.cyclicDifference. They determine a tuple up to simultaneous complementation and have exactly the even-parity tuples as their image. Cslib.BitString.cyclicIntegral supplies a prefix-parity inverse:

open Cslib Cslib.BitString in
example {n : ℕ} (d : Fin n → Bool)
    (hd : parityOn Finset.univ d = false) :
    cyclicDifference (cyclicIntegral d) = d :=
  cyclicDifference_cyclicIntegral d hd

Cslib.BitString.IsDeltaMatroid requires nonemptiness and one-sided symmetric exchange. Cslib.BitString.IsEvenDeltaMatroid adds common parity, which may be odd. It forces exchange to flip two distinct coordinates:

open Cslib.BitString in
example {ι : Type} [Fintype ι] [DecidableEq ι]
    {R : Set (ι → Bool)} (hR : IsEvenDeltaMatroid R)
    {x y : ι → Bool} (hx : x ∈ R) (hy : y ∈ R)
    {i : ι} (hi : x i ≠ y i) :
    ∃ j, j ≠ i ∧ x j ≠ y j ∧ flipOn {i, j} x ∈ R :=
  hR.exchange hx hy hi

Twists, coordinate transport and feasible two-bit connectivity are also proved. The difference tests show that ternary NAE has an even delta-matroid difference relation. These are mathematical prerequisites. Geometry, recognition and the full planar dichotomy remain open; the complete edge solver appears below.