Documentation

CslibFrontier.Logics.Propositional.CSP.Planar.Embedding.Projection

Ordered existential projection on actual gadget bodies #

Hiding any selected free port deletes its structural boundary marker, then applies the exact PPGadget.project variable map. The first-port specialization retains its simpler literal prefix program; arbitrary positions use finite cyclic transport and restore survivor order. Original relation arguments are unchanged, and the newly hidden port precedes the old auxiliary block. All numerical and argument-order checks are supplied internally by the source witness and actual last-edge surgery.

source
theorem Cslib.Complexity.CSP.OrderedBoundary.projectPort_injective (n a : ℕ) (j : Fin (n + 1)) :
Function.Injective (Logic.PL.CSP.PPGadget.substitutePort a (Logic.PL.CSP.PPGadget.hidePort j))

Hiding one free port is injective on all labels: its fresh auxiliary comes first, and every old auxiliary remains in the separate following block.

source
def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.projectHead {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} (w : GadgetWitness g) :
GadgetWitness (g.project 0)

The existing semantic gadget's first-port projection has an internally supplied ordered actual-body realization. Its output body is exactly PPGadget.project, with one fresh hidden label before the old auxiliaries; no auxiliary relation symbol or embedding provider is added.

Instances For
    source
    theorem Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.projectHead_certificate {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} (w : GadgetWitness g) :
    w.projectHead.certificate = restrictPrefix (2 * (g.body.occurrences.length + n)) w.certificate

    The first-port projection's supplied certificate is exactly the original table restricted to its body and remaining probe occurrences. This equation exposes the actual program without exposing proof-only construction helpers.

    source
    noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.project {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} (w : GadgetWitness g) (j : Fin (n + 1)) :
    GadgetWitness (g.project j)

    Existential deletion of any selected free port has an internally supplied ordered realization on exactly the existing semantic PPGadget.project j body. The original argument scopes are retained; the hidden port becomes fresh auxiliary zero. All surviving free-port names and their inherited order are proved through the actual constructors.

    Instances For