Certified fixed-gadget replacement

Each source constraint is replaced by a fixed equality-free gadget. Original variable v becomes 2*v; auxiliary port j at constraint index i becomes 2*(B*i+j)+1, where B bounds every gadget's auxiliary count. Repeated source variables are allowed. A global exact-arity guard sends malformed inputs to an explicit rejecting target instance. The rejection premise concerns only that fixed instance, not a solver or gadget theorem.

The native multitape polynomial-time certificate uses binary input/output variable indices, unary local template indices and constraint indices, and a finite lookup for the fixed source alphabet. This is the equality-free case of [Che06], Proposition 3.9, arXiv v1, p. 8, with the encoding and malformed-input behavior made explicit.

Main definitions

• Cslib.Logic.PL.CSP.PPGadget.template: uniform local ports for a certified gadget.
• Cslib.Logic.PL.CSP.replaceGadgetsGuarded: exact-arity guarded fixed-gadget replacement.

Main results

• Cslib.Logic.PL.CSP.satisfiable_replaceGadgetsGuarded_iff: total semantic correctness.
• Cslib.Complexity.CSP.computableInPolyTime_replaceGadgetsGuarded: native polynomial time for fixed finite source alphabets, with binary variable names.

def Cslib.Logic.PL.CSP.PPGadget.template {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) : CSP Rel (Bool × ℕ)

Uniform local ports: false denotes a free port and true an auxiliary port. The natural indices are bounded constants, encoded in unary.

def Cslib.Logic.PL.CSP.instantiate {Rel : Type} (B index : ℕ) (scope : List ℕ) (body : CSP Rel (Bool × ℕ)) : CSP Rel ℕ

Instantiate a local template at one source scope and constraint index.

def Cslib.Logic.PL.CSP.replaceGadgets {Src Rel : Type} (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (F : CSP Src ℕ) : CSP Rel ℕ

Replace every source constraint, with disjoint auxiliary namespaces.

def Cslib.Logic.PL.CSP.replaceGadgetsGuarded {Src Rel : Type} (srcArity : Src → ℕ) (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (reject : CSP Rel ℕ) (F : CSP Src ℕ) : CSP Rel ℕ

Exact-arity guarded gadget replacement with an explicit reject instance.

theorem Cslib.Logic.PL.CSP.PPGadget.wellFormed_template {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) : WellFormed arity g.template

Uniform templates retain the well-formedness of the certified gadget.

theorem Cslib.Logic.PL.CSP.wellFormed_instantiate {Rel : Type} {arity : Rel → ℕ} (B index : ℕ) (scope : List ℕ) (body : CSP Rel (Bool × ℕ)) (h : WellFormed arity body) : WellFormed arity (instantiate B index scope body)

Renaming a well-formed gadget preserves exact target arities.

theorem Cslib.Logic.PL.CSP.wellFormed_replaceGadgets {Src Rel : Type} {arity : Rel → ℕ} (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (h : ∀ (r : Src), WellFormed arity (templates r)) (F : CSP Src ℕ) : WellFormed arity (replaceGadgets B templates F)

Replacing with well-formed templates produces well-formed target constraints.

theorem Cslib.Logic.PL.CSP.wellFormed_replaceGadgetsGuarded {Src Rel : Type} {arity : Rel → ℕ} (srcArity : Src → ℕ) (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (h : ∀ (r : Src), WellFormed arity (templates r)) (reject : CSP Rel ℕ) (hr : WellFormed arity reject) (F : CSP Src ℕ) : WellFormed arity (replaceGadgetsGuarded srcArity B templates reject F)

The guarded compiler produces a well-formed result if its fixed reject instance is well formed.

theorem Cslib.Logic.PL.CSP.satisfiable_replaceGadgets_iff {Src Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {srcArity : Src → ℕ} {srcSem : Src → List Bool → Bool} (gadgets : (r : Src) → PPGadget arity sem (booleanRelation srcArity srcSem r)) (B : ℕ) (hB : ∀ (r : Src), (gadgets r).numAux ≤ B) (F : CSP Src ℕ) (hF : WellFormed srcArity F) : Satisfiable sem (replaceGadgets B (fun (r : Src) => (gadgets r).template) F) ↔ Satisfiable srcSem F

Correct gadgets preserve satisfiability on well-formed inputs. Only a uniform bound on the number of auxiliary ports is required.

theorem Cslib.Logic.PL.CSP.satisfiable_replaceGadgetsGuarded_iff {Src Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {srcArity : Src → ℕ} {srcSem : Src → List Bool → Bool} (gadgets : (r : Src) → PPGadget arity sem (booleanRelation srcArity srcSem r)) (B : ℕ) (hB : ∀ (r : Src), (gadgets r).numAux ≤ B) (reject : CSP Rel ℕ) (hreject : ¬Satisfiable sem reject) (F : CSP Src ℕ) : Satisfiable sem (replaceGadgetsGuarded srcArity B (fun (r : Src) => (gadgets r).template) reject F) ↔ WellFormed srcArity F ∧ Satisfiable srcSem F

The exact-arity guard gives total correctness, including malformed inputs. The supplied reject instance must be unsatisfiable.

theorem Cslib.Logic.PL.CSP.wellFormed_satisfiable_replaceGadgetsGuarded_iff {Src Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {srcArity : Src → ℕ} {srcSem : Src → List Bool → Bool} (gadgets : (r : Src) → PPGadget arity sem (booleanRelation srcArity srcSem r)) (B : ℕ) (hB : ∀ (r : Src), (gadgets r).numAux ≤ B) (reject : CSP Rel ℕ) (hreject : ¬(WellFormed arity reject ∧ Satisfiable sem reject)) (F : CSP Src ℕ) : WellFormed arity (replaceGadgetsGuarded srcArity B (fun (r : Src) => (gadgets r).template) reject F) ∧ Satisfiable sem (replaceGadgetsGuarded srcArity B (fun (r : Src) => (gadgets r).template) reject F) ↔ WellFormed srcArity F ∧ Satisfiable srcSem F

Full guarded correctness for the exact-arity CSP decision predicate. A reject target may fail either well-formedness or satisfiability, allowing a fixed malformed constraint.

def Cslib.Logic.PL.CSP.malformedReject {Rel : Type} (arity : Rel → ℕ) (r : Rel) : CSP Rel ℕ

A fixed malformed target for rejecting invalid source scopes. Any target symbol suffices.

theorem Cslib.Logic.PL.CSP.not_wellFormed_malformedReject {Rel : Type} (arity : Rel → ℕ) (r : Rel) : ¬WellFormed arity (malformedReject arity r)

The fixed reject target fails exact arity independently of its semantics.

theorem Cslib.Complexity.CSP.computableInPolyTime_instantiate {Rel : Type} (encRel : Rel ↪ List Bool) (B : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × List ℕ) × Logic.PL.CSP Rel (Bool × ℕ)) => match p with | ((index, scope), body) => Logic.PL.CSP.instantiate B index scope body) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (encCSP encRel (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encUnary))) (encCSP encRel Turing.MultiTapeTM.encNat)

Instantiate a local template in native polynomial time. Local indices and the constraint number are unary; scope variable names and output names are binary.

theorem Cslib.Complexity.CSP.computableInPolyTime_replaceGadgets {Src Rel : Type} [Finite Src] (encSrc : Src ↪ List Bool) (encRel : Rel ↪ List Bool) (B : ℕ) (templates : Src → Logic.PL.CSP Rel (Bool × ℕ)) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.replaceGadgets B templates) (encCSP encSrc Turing.MultiTapeTM.encNat) (encCSP encRel Turing.MultiTapeTM.encNat)

Finite fixed gadget lookup and replacement are native polynomial time, with no computability requirement on the process used to obtain the fixed gadgets.

theorem Cslib.Complexity.CSP.computableInPolyTime_replaceGadgetsGuarded {Src Rel : Type} [Finite Src] (encSrc : Src ↪ List Bool) (encRel : Rel ↪ List Bool) (srcArity : Src → ℕ) (B : ℕ) (templates : Src → Logic.PL.CSP Rel (Bool × ℕ)) (reject : Logic.PL.CSP Rel ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.replaceGadgetsGuarded srcArity B templates reject) (encCSP encSrc Turing.MultiTapeTM.encNat) (encCSP encRel Turing.MultiTapeTM.encNat)

A total native polynomial-time compiler with an explicit malformed-input reject target.