Ordered normalization of a cyclic exchange obstruction

This is an original reconstruction of the combinatorial argument missing from [DK15], §4, printed p. 440, Lemma 6 (ICALP 2015 version, DOI 10.1007/978-3-662-47672-7_35). That version supplies the statement only. The source's ordered difference convention is cyclicDifference; its standardized endpoint is the existing IsStandardizedInconsistent. Nonemptiness is explicit, so an empty relation cannot supply a spurious failed exchange.

The finite program records only cyclic rotation, adjacent equality identification and the specific two-difference cap. Its execution changes actual CSP scopes, starting with one literal of the input relation and one or two disequality spokes per port. There are no Boolean constants. This module does not declare a planar expressibility relation or prove a geometric realization, planar substitution, hardness reduction, or running-time bound. Realizing each recorded operation remains separate work.

Main definitions

• Cslib.BitString.CyclicExchangeObstruction: feasible failed-exchange invariant.
• Cslib.Logic.PL.CSP.Normalization.Program: typed finite ordered boundary operations.
• Cslib.Logic.PL.CSP.Normalization.Construction: the twist, rotation and completed recipe.

Main results

• Cslib.Logic.PL.CSP.Normalization.exists_construction: arbitrary-arity normalization.
• Cslib.Logic.PL.CSP.Normalization.Construction.gadget: the actual finite conjunction.
• Cslib.Logic.PL.CSP.Normalization.Construction.numAux_bound: at most 3n-4 auxiliaries.

inductive Cslib.Logic.PL.CSP.Normalization.Symbol : Type

The two symbols used by normalization: one input relation and binary disequality.

• relation : Symbol

  The original relation, of arbitrary arity.

• disequality : Symbol

  Boolean disequality, of arity two.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Normalization.instDecidableEqSymbol : DecidableEq Symbol

theorem Cslib.Logic.PL.CSP.Normalization.Symbol.ofNat_ctorIdx (x : Symbol) : ofNat x.ctorIdx = x

Reconstruct a normalization symbol from its constructor index.

def Cslib.Logic.PL.CSP.Normalization.arity (n : ℕ) : Symbol → ℕ

Declared widths of normalization constraints.

noncomputable def Cslib.Logic.PL.CSP.Normalization.sem {n : ℕ} (R : Set (Fin n → Bool)) : Symbol → List Bool → Bool

Width-guarded interpretation of the original relation and disequality. The classical membership decision is fixed-language preprocessing, with no runtime claim.

@[simp]

theorem Cslib.Logic.PL.CSP.Normalization.sem_relation {n : ℕ} (R : Set (Fin n → Bool)) (x : Fin n → Bool) : sem R Symbol.relation (List.ofFn x) = true ↔ x ∈ R

The input symbol evaluates its tuple in exactly the original port order.

@[simp]

theorem Cslib.Logic.PL.CSP.Normalization.sem_disequality {n : ℕ} (R : Set (Fin n → Bool)) (a b : Bool) : sem R Symbol.disequality [a, b] = true ↔ a ≠ b

Binary disequality has exactly its ordinary Boolean semantics.

def Cslib.Logic.PL.CSP.Normalization.twist {n : ℕ} (R : Set (Fin n → Bool)) (a : Fin n → Bool) : Set (Fin n → Bool)

The initial twist relation: translate all original ports by a fixed feasible tuple.

def Cslib.Logic.PL.CSP.Normalization.twistBody {n : ℕ} (a : Fin n → Bool) : CSP Symbol (Fin n ⊕ Fin (n + n))

A single original constraint and radial disequality chains. The first n auxiliaries are the inner ports; the next n are the middle ports for the two-edge chains. A flipped port uses one disequality; an unchanged port uses two. Free and inner labels remain distinct.

theorem Cslib.Logic.PL.CSP.Normalization.twistBody_size {n : ℕ} (a : Fin n → Bool) : List.length (twistBody a) ≤ 1 + 2 * n ∧ (twistBody a).vars.length ≤ 5 * n

The initial conjunction uses at most 1+2n constraints and total scope width 5n.

theorem Cslib.Logic.PL.CSP.Normalization.wellFormed_twistBody {n : ℕ} (a : Fin n → Bool) : WellFormed (arity n) (twistBody a)

Exact scope widths of the initial conjunction, including arities zero and one.

theorem Cslib.Logic.PL.CSP.Normalization.eval_twistBody_iff {n : ℕ} (R : Set (Fin n → Bool)) (a x : Fin n → Bool) (b : Fin (n + n) → Bool) : eval (sem R) (Sum.elim x b) (twistBody a) = true ↔ (fun (i : Fin n) => b (Fin.castAdd n i)) ∈ R ∧ ∀ (i : Fin n), if a i = true then b (Fin.castAdd n i) ≠ x i else b (Fin.castAdd n i) ≠ b (Fin.natAdd n i) ∧ b (Fin.natAdd n i) ≠ x i

The existential witnesses of the initial twist are exactly the spoke equations and one original relation test. Unused middle ports on flipped spokes are unrestricted.

noncomputable def Cslib.Logic.PL.CSP.Normalization.twistGadget {n : ℕ} (R : Set (Fin n → Bool)) (a : Fin n → Bool) : PPGadget (arity n) (sem R) (twist R a)

The actual twist gadget; it uses one original literal and at most two disequalities per port, with 2n auxiliary labels.

def Cslib.Logic.PL.CSP.Normalization.rotate {n : ℕ} (e : Fin n) (P : Set (Fin n → Bool)) : Set (Fin n → Bool)

A cyclic change of starting port, with orientation preserved.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Normalization.instDecidablePredForallFinBoolMemSetRotate {n : ℕ} (e : Fin n) (P : Set (Fin n → Bool)) [DecidablePred fun (x : Fin n → Bool) => x ∈ P] : DecidablePred fun (x : Fin n → Bool) => x ∈ rotate e P

inductive Cslib.Logic.PL.CSP.Normalization.Program : ℕ → ℕ → Type

A finite typed sequence of the permitted ordered boundary operations. It is executable program data; its constructors are coordinate maps, not planar closure assumptions.

• done (n : ℕ) : Program n n

  Keep the current ordered boundary.

• rotate {n m : ℕ} (e : Fin n) (rest : Program n m) : Program n m

  Change only the cyclic starting port.

• zero {n m : ℕ} (i : Fin (n + 2)) (rest : Program (n + 1) m) : Program (n + 2) m

  Identify adjacent ports and delete the redundant port, with the explicit wraparound map.

• cap {n m : ℕ} (large : 2 ≤ n) (rest : Program (n + 2) m) : Program (n + 4) m

  Identify old ports 1 and 3 and hide old port 2; retain free order 0,1,4,…. The lower bound excludes degenerate short boundaries in the intended geometric realization.

def Cslib.Logic.PL.CSP.Normalization.Program.eval {n m : ℕ} (p : Program n m) (P : Set (Fin n → Bool)) : Set (Fin m → Bool)

Execute the recorded coordinate maps on boundary relations.

def Cslib.Logic.PL.CSP.Normalization.Program.gadget {Rel : Type} {ar : Rel → ℕ} {s : Rel → List Bool → Bool} {n m : ℕ} (p : Program n m) {P : Set (Fin n → Bool)} (g : PPGadget ar s P) : PPGadget ar s (p.eval P)

Compile the recorded operations by relabeling the actual conjunction. The cap adds exactly one fresh auxiliary; rotation and zero deletion add none. No original constraints are replaced.

structure Cslib.BitString.CyclicExchangeObstruction {n : ℕ} (P : Set (Fin (n + 1) → Bool)) (d : Fin (n + 1) → Bool) : Prop

A failed-exchange witness with distinguished difference literally at coordinate 0. The witness may have proper support before zero deletion. Feasibility of both the witness and the zero tuple prevents empty intermediate relations.

• selfComplementary : IsSelfComplementary P

  Complementing all ports preserves membership.

• zero_mem : (fun (x : Fin (n + 1)) => false) ∈ P

  The all-false original tuple is feasible.

• feasible : d ∈ cyclicDifferenceRelation P

  The nonzero difference witness is feasible.

• first : d 0 = true

  The distinguished difference is coordinate 0.

• forbidden (j : Fin (n + 1)) : j ≠ 0 → d j = true → (flipOn {0, j} fun (x : Fin (n + 1)) => false) ∉ cyclicDifferenceRelation P

  Every two-coordinate exchange involving 0 within the witness support fails.

theorem Cslib.BitString.CyclicExchangeObstruction.zero {n : ℕ} {P : Set (Fin (n + 2) → Bool)} {d : Fin (n + 2) → Bool} (h : CyclicExchangeObstruction P d) (i : Fin (n + 2)) (hi : d i = false) : CyclicExchangeObstruction (zeroRestriction i P) (d ∘ differencePort i)

Zero-conditioned deletion preserves the failed-exchange witness and its distinguished edge.

theorem Cslib.BitString.CyclicExchangeObstruction.four_le {n : ℕ} {P : Set (Fin (n + 1) → Bool)} {d : Fin (n + 1) → Bool} (h : CyclicExchangeObstruction P d) : 4 ≤ n + 1

No failed-exchange witness fits on fewer than four cyclic difference coordinates.

theorem Cslib.BitString.CyclicExchangeObstruction.not_isEvenDeltaMatroid {n : ℕ} {P : Set (Fin (n + 1) → Bool)} {d : Fin (n + 1) → Bool} (h : CyclicExchangeObstruction P d) : ¬IsEvenDeltaMatroid (cyclicDifferenceRelation P)

The witnessed failed exchange rules out the even delta-matroid axiom.

theorem Cslib.BitString.CyclicExchangeObstruction.eq_full {P : Set (Fin 4 → Bool)} {d : Fin 4 → Bool} (h : CyclicExchangeObstruction P d) : d = fun (x : Fin 4) => true

At arity four, the witness must be the full set of differences.

theorem Cslib.BitString.CyclicExchangeObstruction.standardized {P : Set (Fin 4 → Bool)} {d : Fin 4 → Bool} (h : CyclicExchangeObstruction P d) : IsStandardizedInconsistent P

The terminal relation is standardized in precisely the recorded cyclic port order.

theorem Cslib.BitString.CyclicExchangeObstruction.cap {n : ℕ} {P : Set (Fin (n + 4) → Bool)} (h : CyclicExchangeObstruction P fun (x : Fin (n + 3 + 1)) => true) (hq : ∀ (k : Fin (n + 4)), 3 ≤ ↑k → (flipOn {0, 1, 2, k} fun (x : Fin (n + 4)) => false) ∉ cyclicDifferenceRelation P) : CyclicExchangeObstruction (capRelation P) fun (x : Fin (n + 1 + 1)) => true

When all candidate quartets fail, the cap preserves the full-support obstruction. Every putative new pair has exactly the two lifts ruled out by the hypotheses.

theorem Cslib.BitString.CyclicExchangeObstruction.quartet {n : ℕ} {P : Set (Fin (n + 4) → Bool)} (h : CyclicExchangeObstruction P fun (x : Fin (n + 3 + 1)) => true) (k : Fin (n + 4)) (hk : (flipOn {0, 1, 2, k} fun (x : Fin (n + 4)) => false) ∈ cyclicDifferenceRelation P) : CyclicExchangeObstruction P (flipOn {0, 1, 2, k} fun (x : Fin (n + 3 + 1)) => false)

Any feasible quartet gives a fresh obstruction witness in the same relation. It is this quartet, not the previous full tuple, that survives the finishing zero restrictions.

theorem Cslib.Logic.PL.CSP.Normalization.exists_program_of_obstruction (n : ℕ) (P : Set (Fin (n + 1) → Bool)) (d : Fin (n + 1) → Bool) (h : BitString.CyclicExchangeObstruction P d) : ∃ (p : Program (n + 1) 4), BitString.IsStandardizedInconsistent (p.eval P)

Normalize an arbitrary-arity obstruction by a finite sequence of the recorded maps. Zero differences are deleted at their greatest remaining index, so a run of zero deletions proceeds in descending order. Each recursive call strictly decreases the actual arity.

theorem Cslib.Logic.PL.CSP.Normalization.isSelfComplementary_twist {n : ℕ} {R : Set (Fin n → Bool)} (hR : BitString.IsSelfComplementary R) (a : Fin n → Bool) : BitString.IsSelfComplementary (twist R a)

Twisting preserves simultaneous complementation of all original ports.

theorem Cslib.Logic.PL.CSP.Normalization.isSelfComplementary_rotate {n : ℕ} {P : Set (Fin n → Bool)} (hP : BitString.IsSelfComplementary P) (e : Fin n) : BitString.IsSelfComplementary (rotate e P)

A cyclic change of starting port preserves self-complementarity.

theorem Cslib.Logic.PL.CSP.Normalization.obstruction_twist_rotate {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (hR : BitString.IsSelfComplementary R) (a b : Fin (n + 1) → Bool) (ha : a ∈ R) (hb : b ∈ R) (e : Fin (n + 1)) (he : BitString.cyclicDifference a e ≠ BitString.cyclicDifference b e) (hf : ∀ (j : Fin (n + 1)), BitString.cyclicDifference a j ≠ BitString.cyclicDifference b j → BitString.flipOn {e, j} (BitString.cyclicDifference a) ∉ BitString.cyclicDifferenceRelation R) : BitString.CyclicExchangeObstruction (rotate e (twist R a)) ((BitString.cyclicDifference b + BitString.cyclicDifference a) ∘ ⇑(finCycle e))

The actual twist and initial cyclic rotation normalize a genuine failed exchange. The tuple a is feasible in the original relation, and every exchange along the difference support of a and b is ruled out by hf.

theorem Cslib.Logic.PL.CSP.Normalization.exists_failed_exchange {n : ℕ} {R : Set (Fin n → Bool)} (hne : R.Nonempty) (hn : ¬BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation R)) : ∃ a ∈ R, ∃ b ∈ R, ∃ (e : Fin n), BitString.cyclicDifference a e ≠ BitString.cyclicDifference b e ∧ ∀ (j : Fin n), BitString.cyclicDifference a j ≠ BitString.cyclicDifference b j → BitString.flipOn {e, j} (BitString.cyclicDifference a) ∉ BitString.cyclicDifferenceRelation R

A nonempty cyclic-difference relation that is not an even delta-matroid has a genuine failed exchange. Even parity is automatic, so neither parity nor emptiness causes the failure.

structure Cslib.Logic.PL.CSP.Normalization.Construction {n : ℕ} (R : Set (Fin n → Bool)) : Type

A completed finite normalization recipe. Its starting tuple is feasible in the input, and the first operation is the specified cyclic rotation of the twisted literal.

• tuple : Fin n → Bool

  Feasible tuple used by the disequality spokes.

• tuple_mem : self.tuple ∈ R

  The twist is chosen at a feasible original tuple.

• start : Fin n

  Original difference moved to boundary coordinate 0.

• reduction : Program n 4

  Finite ordered boundary operations after the initial rotation.

• standardized : BitString.IsStandardizedInconsistent (self.reduction.eval (rotate self.start (twist R self.tuple)))

  The executed relation is standardized in the resulting free-port order.

def Cslib.Logic.PL.CSP.Normalization.Construction.target {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction R) : Set (Fin 4 → Bool)

The four-ary relation defined by the recorded normalization recipe.

noncomputable def Cslib.Logic.PL.CSP.Normalization.Construction.gadget {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction R) : PPGadget (arity n) (sem R) c.target

The executed actual finite gadget for the normalized relation, starting with one original literal and its twist spokes. Its correctness follows at every step from exact scope relabeling.

theorem Cslib.Logic.PL.CSP.Normalization.exists_construction {n : ℕ} (R : Set (Fin n → Bool)) (hne : R.Nonempty) (hR : BitString.IsSelfComplementary R) (hn : ¬BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation R)) : 4 ≤ n ∧ Nonempty (Construction R)

Arbitrary-arity ordered combinatorial normalization, with no expressibility, solver, classification or reduction premise. The result contains an executable finite operation trace and an actual equality-free {R,N} gadget for a standardized four-ary relation. Geometric realization of the recorded operations and the full planar hardness theorem remain separate obligations; this does not assert the planar expressibility conclusion of Lemma 6.

def Cslib.Logic.PL.CSP.Normalization.Program.caps {n m : ℕ} (p : Program n m) : ℕ

Number of caps, each introducing exactly one hidden port.

def Cslib.Logic.PL.CSP.Normalization.Program.reductions {n m : ℕ} (p : Program n m) : ℕ

Number of boundary reductions; the initial cyclic rotation is not counted.

theorem Cslib.Logic.PL.CSP.Normalization.Program.caps_bound {n m : ℕ} (p : Program n m) : 2 * p.caps + m ≤ n

Every cap removes two boundary ports.

theorem Cslib.Logic.PL.CSP.Normalization.Program.reductions_bound {n m : ℕ} (p : Program n m) : p.reductions + m ≤ n

Every nonrotation operation removes at least one boundary port.

theorem Cslib.Logic.PL.CSP.Normalization.Program.gadget_symbols {Rel : Type} {ar : Rel → ℕ} {s : Rel → List Bool → Bool} {n m : ℕ} (p : Program n m) {P : Set (Fin n → Bool)} (g : PPGadget ar s P) : List.map Prod.fst (p.gadget g).body = List.map Prod.fst g.body

Execution keeps exactly the original ordered sequence of relation symbols. Only variable labels in their scopes change.

theorem Cslib.Logic.PL.CSP.Normalization.Program.gadget_width {Rel : Type} {ar : Rel → ℕ} {s : Rel → List Bool → Bool} {n m : ℕ} (p : Program n m) {P : Set (Fin n → Bool)} (g : PPGadget ar s P) : (p.gadget g).body.vars.length = g.body.vars.length

Scope relabeling keeps the exact total number of variable occurrences.

theorem Cslib.Logic.PL.CSP.Normalization.Program.gadget_numAux {Rel : Type} {ar : Rel → ℕ} {s : Rel → List Bool → Bool} {n m : ℕ} (p : Program n m) {P : Set (Fin n → Bool)} (g : PPGadget ar s P) : (p.gadget g).numAux = g.numAux + p.caps

The cap adds precisely one fresh auxiliary label; all old auxiliaries survive.

theorem Cslib.Logic.PL.CSP.Normalization.Construction.numAux_bound {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction R) : c.gadget.numAux ≤ 3 * n - 4

The final gadget has at most 3n-4 auxiliaries, counting the redundant twist labels.

theorem Cslib.Logic.PL.CSP.Normalization.Construction.body_bounds {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction R) : List.length c.gadget.body ≤ 1 + 2 * n ∧ c.gadget.body.vars.length ≤ 5 * n

The final body retains the initial constraint and scope-width bounds.