The full ordered free-port boundary of an arbitrary-arity atom

The structural probe has the literal reversed free scope. Its actual incidence graph is the two-center ordered star, including two isolated centers in the nullary case. The supplied table and its executable body restriction use no rotation search.

def Cslib.Complexity.CSP.OrderedBoundary.atomBoundaryCertificate (n : ℕ) : Graph.RotationCertificate

Supplied atom/probe table for every arity. The proof below checks its actual body and reversed-probe incidence interpretations, rather than searching for an embedding.

theorem Cslib.Complexity.CSP.OrderedBoundary.length_atomBoundaryCertificate (n : ℕ) : (atomBoundaryCertificate n).successor.length = 4 * n

Both stars contribute one edge per free-port position.

theorem Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix_atomBoundaryCertificate (n : ℕ) : restrictPrefix (2 * n) (atomBoundaryCertificate n) = atomBodyCertificate n

The list-funded deletion of the actual probe darts gives exactly the ordered-star body table. Variable corners take two steps; constraint corners take one.

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

Every literal original-language atom internally supplies the full ordered free-port boundary, at arbitrary arity. The actual PP body, original relation symbol and argument order are retained. At arity zero both nullary centers use the separate point convention.

theorem Cslib.Complexity.CSP.OrderedBoundary.atomBoundaryCertificate_accepted {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : verify (Logic.PL.CSP.PPGadget.atom r).body (List.ofFn Sum.inl) (atomBoundaryCertificate (arity r)) = true

The explicit arbitrary-arity atom/probe table passes both actual checks. There is no template-planarity, normalization, pp-definability or rotation-provider premise.