Finite crossover gadgets

This module verifies the conjunctions in [DK15], §4, printed pp. 440–441, Figure 1. Ports 0,1,2,3 correspond to the cyclic boundary order v₁,v₂,v₃,v₄. Figure 1(a) uses R(m,v₃,v₄,v₁), R(v₃,m̄,v₁,v̄₂), N(m,m̄), N(v̄₂,v₂); Figure 1(b) uses NEAR-CROSS(v₁,v₂,m,v₄), NEAR-CROSS(v₃,v₄,m,v₂). These are actual CSP.PPGadget bodies, with exact scope widths and existential auxiliaries.

Only finite relation semantics is proved here: no embedding, planar substitution, normalization from non-delta-matroids (the source's Lemma 6, stated without proof), hardness or runtime certificate is supplied. No expressibility theorem is assumed.

Main definitions

• Cslib.BitString.cross, Cslib.BitString.nearCross: ordered four-port relations.
• Cslib.BitString.IsStandardizedInconsistent: the hypothesis on Figure 1(a)'s relation.
• Cslib.BitString.standardizedRelation: all eight possible standardized relations.
• Cslib.Logic.PL.CSP.Crossover.figureOneA: Figure 1(a) as a primitive-positive gadget.
• Cslib.Logic.PL.CSP.Crossover.figureOneB: Figure 1(b) as a primitive-positive gadget.

Main results

• Cslib.BitString.isStandardizedInconsistent_iff: exhaustive three-bit classification.
• Cslib.Logic.PL.CSP.Crossover.figureOneA_target: the first target is CROSS or NEAR-CROSS.

def Cslib.BitString.cross : Set (Fin 4 → Bool)

CROSS connects opposite ports in cyclic order: 0=2 and 1=3.

@[instance_reducible]

instance Cslib.BitString.instDecidablePredForallFinOfNatNatBoolMemSetCross : DecidablePred fun (x : Fin 4 → Bool) => x ∈ cross

def Cslib.BitString.nearCross : Set (Fin 4 → Bool)

NEAR-CROSS adds 0001 and 1110 to CROSS, in the same cyclic port order.

@[instance_reducible]

instance Cslib.BitString.instDecidablePredForallFinOfNatNatBoolMemSetNearCross : DecidablePred fun (x : Fin 4 → Bool) => x ∈ nearCross

def Cslib.BitString.IsStandardizedInconsistent (R : Set (Fin 4 → Bool)) : Prop

Standardized inconsistency in [DK15], §4, printed p. 440. The relation is self-complementary, contains CROSS, and has only the specified tuples.

def Cslib.BitString.standardizedRelation (p q r : Bool) : Set (Fin 4 → Bool)

The eight standardized relations. Bits p,q,r select the complementary pairs 0001/1110, 0010/1101, 0011/1100, respectively, in addition to CROSS.

@[instance_reducible]

instance Cslib.BitString.instDecidableStandardizedRelation (p q r : Bool) : DecidablePred fun (x : Fin 4 → Bool) => x ∈ standardizedRelation p q r

theorem Cslib.BitString.isStandardizedInconsistent_iff (R : Set (Fin 4 → Bool)) : IsStandardizedInconsistent R ↔ ∃ (p : Bool) (q : Bool) (r : Bool), R = standardizedRelation p q r

The three optional complementary pairs exhaust the standardized condition.

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

The alphabet for Figure 1(a): the given four-ary relation and binary disequality.

• relation : Symbol

  The standardized relation.

• disequality : Symbol

  Boolean disequality.

@[instance_reducible]

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

def Cslib.Logic.PL.CSP.Crossover.arity : Symbol → ℕ

Declared widths of the two Figure 1(a) symbols.

def Cslib.Logic.PL.CSP.Crossover.sem (R : Set (Fin 4 → Bool)) [DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] : Symbol → List Bool → Bool

Width-guarded interpretation of the given relation and Boolean disequality.

def Cslib.Logic.PL.CSP.Crossover.figureOneABody : CSP Symbol (Fin 4 ⊕ Fin 3)

Figure 1(a)'s four constraints. Auxiliary indices 0,1,2 are m,m̄,v̄₂. The order inside each scope is the numbered order in the figure.

def Cslib.Logic.PL.CSP.Crossover.figureOneARelation (R : Set (Fin 4 → Bool)) [DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] : Set (Fin 4 → Bool)

Figure 1(a)'s existential boundary relation, using the existing CSP evaluator.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Crossover.instDecidablePredForallFinOfNatNatBoolMemSetFigureOneARelation (R : Set (Fin 4 → Bool)) [DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] : DecidablePred fun (x : Fin 4 → Bool) => x ∈ figureOneARelation R

def Cslib.Logic.PL.CSP.Crossover.figureOneA (R : Set (Fin 4 → Bool)) [DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] : PPGadget arity (sem R) (figureOneARelation R)

The first figure as a well-formed primitive-positive gadget for its boundary relation.

theorem Cslib.Logic.PL.CSP.Crossover.figureOneARelation_standardized (p q r : Bool) : figureOneARelation (BitString.standardizedRelation p q r) = if (p || q) = true then BitString.nearCross else BitString.cross

Exhaustive finite semantics of Figure 1(a). The third optional pair has no effect; either of the first two optional pairs produces precisely NEAR-CROSS.

theorem Cslib.Logic.PL.CSP.Crossover.figureOneA_target (R : Set (Fin 4 → Bool)) [inst : DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] (h : BitString.IsStandardizedInconsistent R) : figureOneARelation R = BitString.cross ∨ figureOneARelation R = BitString.nearCross

Under exactly the standardized hypothesis, the actual first figure defines CROSS or NEAR-CROSS. No planar expressibility premise or conclusion is used.

theorem Cslib.Logic.PL.CSP.Crossover.figureOneARelation_eq (R : Set (Fin 4 → Bool)) [inst : DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] (h : BitString.IsStandardizedInconsistent R) : figureOneARelation R = if decide (![false, false, false, true] ∈ R ∨ ![false, false, true, false] ∈ R) = true then BitString.nearCross else BitString.cross

The exact first target can be selected by inspecting only 0001 and 0010 in R.

def Cslib.Logic.PL.CSP.Crossover.figureOneAStandardized (R : Set (Fin 4 → Bool)) [DecidablePred fun (x : Fin 4 → Bool) => x ∈ R] (h : BitString.IsStandardizedInconsistent R) : PPGadget arity (sem R) (if decide (![false, false, false, true] ∈ R ∨ ![false, false, true, false] ∈ R) = true then BitString.nearCross else BitString.cross)

Figure 1(a) with its explicitly identified CROSS or NEAR-CROSS target. The body still has exactly the four constraints displayed in the source.

def Cslib.Logic.PL.CSP.Crossover.nearSem : Unit → List Bool → Bool

The width-guarded NEAR-CROSS interpretation for Figure 1(b)'s single symbol.

def Cslib.Logic.PL.CSP.Crossover.figureOneBBody : CSP Unit (Fin 4 ⊕ Fin 1)

Figure 1(b)'s two constraints; its one auxiliary is m.

theorem Cslib.Logic.PL.CSP.Crossover.figureOneB_correct (a : Fin 4 → Bool) : a ∈ BitString.cross ↔ ∃ (b : Fin 1 → Bool), eval nearSem (Sum.elim a b) figureOneBBody = true

Figure 1(b) defines precisely CROSS, with existential m.

def Cslib.Logic.PL.CSP.Crossover.figureOneB : PPGadget (fun (x : Unit) => 4) nearSem BitString.cross

The actual Figure 1(b) primitive-positive gadget from NEAR-CROSS to CROSS.