2.30. Ordered Cyclic-Obstruction Normalization🔗

Cslib.Logic.PL.CSP.Normalization.exists_construction treats arbitrary arity. Its input relation is nonempty and self-complementary, with a cyclic-difference relation failing the even delta-matroid axiom. It proves arity at least four and produces an ordered recipe and an actual gadget over the original relation and disequality. The finite constraint, scope-occurrence and auxiliary bounds compose:

open Cslib.BitString Cslib.Logic.PL.CSP in
example {n : ℕ} (R : Set (Fin n → Bool)) (hne : R.Nonempty)
    (hsc : IsSelfComplementary R)
    (hbad : ¬IsEvenDeltaMatroid (cyclicDifferenceRelation R)) :
    ∃ Q : Set (Fin 4 → Bool), IsStandardizedInconsistent Q ∧
      ∃ g : PPGadget (Normalization.arity n) (Normalization.sem R) Q,
        g.body.length ≤ 1 + 2 * n ∧ g.body.vars.length ≤ 5 * n ∧
          g.numAux ≤ 3 * n - 4 := byn:ℕR:Set (Fin n → Bool)hne:R.Nonemptyhsc:IsSelfComplementary Rhbad:¬IsEvenDeltaMatroid (cyclicDifferenceRelation R)⊢ ∃ Q,
  IsStandardizedInconsistent Q ∧ ∃ g, List.length g.body ≤ 1 + 2 * n ∧ g.body.vars.length ≤ 5 * n ∧ g.numAux ≤ 3 * n - 4
  obtain ⟨_, ⟨c⟩⟩ := Normalization.exists_construction R hne hsc hbadn:ℕR:Set (Fin n → Bool)hne:R.Nonemptyhsc:IsSelfComplementary Rhbad:¬IsEvenDeltaMatroid (cyclicDifferenceRelation R)left✝:4 ≤ nc:Normalization.Construction R⊢ ∃ Q,
  IsStandardizedInconsistent Q ∧ ∃ g, List.length g.body ≤ 1 + 2 * n ∧ g.body.vars.length ≤ 5 * n ∧ g.numAux ≤ 3 * n - 4
  exact ⟨c.target, c.standardized, c.gadget, c.body_bounds.1, c.body_bounds.2,
    c.numAux_bound⟩All goals completed! 🐙

The program uses cyclic rotations, adjacent zero-conditioned identifications and the specific cap identifying old ports 1 and 3 while hiding old port 2. It keeps the resulting free-port order. The initial body contains one original literal and one or two disequality spokes per original port; later steps relabel scopes. The bounds count constraints, scope occurrences and allocated auxiliaries, including unused labels. They assert neither native runtime nor binary encoded size.

This is an original combinatorial reconstruction of the omitted argument behind Dvořák–Kupec Lemma 6, not its full planar-expressibility conclusion. Geometric realization and the full planar theorem remain open. Complete nonvacuous clients are in CslibFrontierTests/PlanarNormalization.lean.