2.27. Ordered Boundary and Static Gadget Closure🔗

Ordinary imports are CslibFrontier.Logics.Propositional.CSP.Planar.Embedding.AtomBoundary, ...Embedding.Projection, ...Embedding.GadgetCyclic and ...Embedding.Equality. Import ...Embedding.Construction for every existing construction-tree branch. The actual semantic objects remain Cslib.Logic.PL.CSP.PPGadget; numerical boundary witnesses live in Cslib.Complexity.CSP.OrderedBoundary.

A structural probe uses the reversed port word and has no original-language relation semantics. Witness F ports checks both its augmented rotation and the literal first-return restriction to F. GadgetWitness g uses g.body and all canonical free ports, including unused ones. Every atom has a full witness, at arbitrary arity, without a truth or planarity premise:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Complexity in
open Cslib.Complexity.CSP.OrderedBoundary in
example {Rel : Type} (arity : Rel → ℕ)
    (sem : Rel → List Bool → Bool) (r : Rel) :
    GadgetWitness (PPGadget.atom (arity := arity) (sem := sem) r) :=
  Witness.atom arity sem r

The explicit atom/probe table handles arity zero with two isolated centers. A false nullary relation can pass structural checks; this is not a SAT test. Repeated constraint positions are never deduplicated. Atom tests include mirrored numerical rotations rejected by argument order.

Probe-to-body extraction has an explicit duplicate-free port premise. The body may still have repeated names, duplicate constraints and cut vertices:

open Cslib.Logic.PL Cslib.Complexity in
open Cslib.Complexity.CSP Cslib.Complexity.CSP.OrderedBoundary in
example {Rel V : Type} [DecidableEq V] (F : CSP Rel V)
    (ports : List V) (hn : ports.Nodup) (c : Graph.RotationCertificate)
    (h : verifyRotationCertificate (probeBody F ports) c = true) :
    verifyRotationCertificate F (bodyCertificate F c) = true :=
  bodyCertificate_accepted_of_probe F ports hn c h

The last-argument operation proves the full target checker on the original CSP lists. Applied to a probe it removes a boundary marker; it makes no SAT claim for editing a Gamma constraint:

open Cslib.Logic.PL Cslib.Complexity in
open Cslib.Complexity.CSP Cslib.Complexity.CSP.OrderedBoundary in
example {Rel V : Type} [DecidableEq V] (F : CSP Rel V) (r : Rel)
    (scope : List V) (v : V) (c : Graph.RotationCertificate)
    (h : verifyRotationCertificate (F ++ [(r, scope ++ [v])]) c = true) :
    verifyRotationCertificate (F ++ [(r, scope)])
      (restrictPrefix (2 * (F ++ [(r, scope)]).occurrences.length) c) =
        true :=
  verifyRotationCertificate_restrictPrefix_lastArgument F r scope v c h

Witness.forgetAt retains the exact survivor word on the same body, using a directed cycle, deletion and inverse cycle. It requires a valid position and a duplicate-free whole word. The special forgetHead only needs its tail to be duplicate-free; that weaker contract is not asserted for all positions.

open Cslib.Logic.PL Cslib.Complexity in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel V : Type} [DecidableEq V] {F : CSP Rel V}
    {ports : List V} (w : Witness F ports) (k : ℕ)
    (hn : ports.Nodup) (hk : k < ports.length) :
    Witness F (ports.eraseIdx k) :=
  Witness.forgetAt k w hn hk

The gadget constructors internally prove canonical port distinctness and variable-map injection. Projection uses exactly g.project j, hiding the port at auxiliary zero before old auxiliaries. Cyclic rotation is the existing positive-arity Construction.gadget free-label map:

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

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Complexity in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin (n + 1) → Bool)} {g : PPGadget arity sem R}
    (w : GadgetWitness g) :
    GadgetWitness (g.relabelFree (fun i => i + 1)) := w.rotate

Adjacent equality targets the exact existing g.equalDrop; it adds no equality symbol. Consecutive probe arguments supply cofacial variable corners internally. The duplicate marker is removed before Nodup body extraction, retaining the original scopes, nullaries and repeated constraint positions:

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

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

The whole generated NAE table is explicit, not merely an existence claim:

open Cslib.Complexity.CSP.OrderedBoundary in
example :
    equalDropCertificate
      ([((), [0, 1, 2])] : Cslib.Logic.PL.CSP Unit ℕ) 1
      (atomBoundaryCertificate 3) =
        (⟨[8, 3, 0, 5, 6, 1, 4, 9, 2, 7]⟩ :
          Cslib.Complexity.Graph.RotationCertificate) := by⊢ equalDropCertificate [((), [0, 1, 2])] 1 (atomBoundaryCertificate 3) = { successor := [8, 3, 0, 5, 6, 1, 4, 9, 2, 7] }
  decide +kernelAll goals completed! 🐙

CslibFrontierTests/PlanarEqualityBoundary.lean ties that table to the exact original-language NAE body and derives disequality and both OneHot pins. Generic attachment and the complete static grammar are supplied below; expanded-language macros remain separate obligations. The raw table program uses bounded predecessor lookup, an outgoing swap and prefix restriction. Its residual arity is static; it carries no uniform native runtime claim for arbitrary binary arity or language/template size.

First-port projection keeps a simpler literal prefix equation:

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

Empty alphabets and unused huge binary names remain valid structural cases. Here the body is unchanged and position one is removed, not a value:

open Cslib.Logic.PL Cslib.Complexity in
open Cslib.Complexity.CSP.OrderedBoundary in
example : ∃ c : Graph.RotationCertificate,
    verify ([] : CSP Empty ℕ) [2 ^ 250, 9] c = true := by⊢ ∃ c, verify [] [2 ^ 250, 9] c = true
  let w : Witness ([] : CSP Empty ℕ) [2 ^ 250, 7, 9] :=
    Witness.empty _ (by⊢ [2 ^ 250, 7, 9].Nodup decideAll goals completed! 🐙)w:Witness [] [2 ^ 250, 7, 9] := Witness.empty [2 ^ 250, 7, 9] ⋯⊢ ∃ c, verify [] [2 ^ 250, 9] c = true
  let h := Witness.forgetAt 1 w (byw:Witness [] [2 ^ 250, 7, 9] := Witness.empty [2 ^ 250, 7, 9] ⋯⊢ [2 ^ 250, 7, 9].Nodup decideAll goals completed! 🐙) (byw:Witness [] [2 ^ 250, 7, 9] := Witness.empty [2 ^ 250, 7, 9] ⋯⊢ 1 < [2 ^ 250, 7, 9].length decideAll goals completed! 🐙)w:Witness [] [2 ^ 250, 7, 9] := Witness.empty [2 ^ 250, 7, 9] ⋯h:Witness [] ([2 ^ 250, 7, 9].eraseIdx 1) := Witness.forgetAt 1 w ⋯ ⋯⊢ ∃ c, verify [] [2 ^ 250, 9] c = true
  exact ⟨h.certificate, h.accepted⟩All goals completed! 🐙

Original nullary constraints and their truth values remain in the body. Zero-port extraction removes only the isolated structural probe. Literal last-argument tables and dense-variable transport are proved internally. Numerical scope reindexing alone does not preserve ordered acceptance: the actual cycles commute with positive finRotate; higher-arity reflection is rejected.

CslibFrontierTests/PlanarCyclicBoundary.lean proves equality of an entire constructed twelve-entry table from all source dart steps, then executes the full checkers. CslibFrontierTests/PlanarProjectionAll.lean checks exact middle/wrap bodies and semantics, canonical Nodup extraction, degree five, unused ports, an empty alphabet and true/false nullaries.

Every existing RelationMinor.Construction now supplies a witness on exactly its original-language interpreter, recursively including enabling pin and disequality trees:

open Cslib.Logic.PL Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin n → Bool)} (c : Construction arity sem R) :
    GadgetWitness c.gadget := c.orderedWitness

The witness checks the actual body and reversed structural probe; it stores no geometric embedding or supplied target-genus oracle:

open Cslib.Logic.PL Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin n → Bool)} (c : Construction arity sem R) :
    verify c.gadget.body (List.ofFn Sum.inl)
      c.orderedWitness.certificate = true := c.orderedWitness.accepted

Availability also supplies an actual gadget with its witness:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)}
    (h : Available arity sem R) :
    ∃ g : PPGadget arity sem R, Nonempty (GadgetWitness g) :=
  h.nonempty_orderedGadget

There is no finite-language, body-occurrence, degree or connectedness premise. The primitive attachment APIs target the exact existing bodies:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin (n + 1) → Bool)} {g : PPGadget arity sem R}
    (w : GadgetWitness g) (j : Fin (n + 1)) (b : Bool)
    {p : PPGadget arity sem (pin b)} (v : GadgetWitness p) :
    GadgetWitness (g.cofactor j b p) := w.cofactor j b v

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin (n + 2) → Bool)} {g : PPGadget arity sem R}
    {d : PPGadget arity sem disequality}
    (w : GadgetWitness g) (v : GadgetWitness d) :
    GadgetWitness (g.differentDrop d) := w.differentDrop v

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.RelationMinor in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {n : ℕ}
    {R : Set (Fin n → Bool)} {g : PPGadget arity sem R}
    (w : GadgetWitness g) (j : Fin n)
    {d : PPGadget arity sem disequality} (v : GadgetWitness d) :
    GadgetWitness (g.flip j d) := w.flip j v

open Cslib.Logic.PL Cslib.Logic.PL.CSP in
open Cslib.Complexity.CSP.OrderedBoundary in
noncomputable example {Rel : Type} {arity : Rel → ℕ}
    {sem : Rel → List Bool → Bool} {R S : Set (Fin 2 → Bool)}
    {g : PPGadget arity sem R} {h : PPGadget arity sem S}
    (w : GadgetWitness g) (v : GadgetWitness h) :
    GadgetWitness (g.conj h) := w.binaryMeet v

The meet is arity two, with no arbitrary higher-arity intersection claim. Flip uses the enlarged noncanonical port word directly, removes the old marker, swaps names and hides last. Probe corners exist even at unused ports; different-component and cofacial joins derive their guards internally. CslibFrontierTests/PlanarConstructionBoundary.lean exercises all eight branches over one original one-in-three symbol, satisfying/rejecting semantic rows, exact auxiliary scopes, empty/unused attachments and a closed result. Run scripts/build.sh CslibFrontierTests.PlanarConstructionBoundary CslibFrontierTests.PlanarConstructionAudit --wfail --iofail.

These are static finite constructors. General projection/cyclic inverses use finite choice and are intentionally noncomputable. Fixing a language and its templates permits nonuniform certificate preprocessing; it does not prove the input-varying native compiler's target acceptance or framed time bound. Figure 1/NAND boundary tables are macro skeletons until original-language substitution is supplied. OneHot3/CROSS macro expansion, normalization caps and Figure-1 substitution, native target acceptance, geometric/ source comparison, recognition and full #3091 remain open.