Documentation

CslibFrontier.Logics.Propositional.CSP.Planar.Embedding.Equality

Adjacent equality restriction on the actual original-language body #

The first two free labels are identified at the corners supplied by their consecutive probe arguments. The duplicate probe marker is then deleted before actual-body extraction uses distinct surviving ports. The body is exactly the existing PPGadget.equalDrop, with no equality relation added to the language. This original static realization retains arbitrary body degree, repeated occurrences, nullaries and closed components.

source
def Cslib.Complexity.CSP.OrderedBoundary.equalDropCertificate {Rel V : Type} (F : Logic.PL.CSP Rel V) (n : ℕ) (c : Graph.RotationCertificate) :
Graph.RotationCertificate

Literal adjacent-equality table program: swap the last probe corner with the predecessor of the penultimate probe end, then remove the last probe edge. The clocks are the actual body/boundary counts and supplied table length, never an encoded label. The residual arity n is a static parameter; no uniform binary-arity runtime bound is claimed.

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

    Identify the first two free ports on exactly PPGadget.equalDrop. Their structural probe arguments internally supply cofacial corners; the first duplicate marker is removed before deriving the actual-body certificate with canonical distinct surviving free ports.

    Instances For
      source
      theorem Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.equalDrop_certificate {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} (w : GadgetWitness g) :
      w.equalDrop.certificate = equalDropCertificate g.body n w.certificate

      The supplied adjacent-equality witness uses exactly the explicit outgoing swap and bounded prefix restriction on the original raw table. No rotation search or embedding provider appears in this generated-table equation.