Literal original-language atoms of arbitrary arity

The incidence graph of a single constraint on distinct indexed free labels is the ordered star, with its full argument rotation. The indexing proofs below concern the actual CSP list and positional occurrence table, including the nullary constraint center.

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

Finite table for the actual atom's body, supplied by the unbounded ordered-star rotation.

theorem Cslib.Complexity.CSP.OrderedBoundary.incidenceGraph_atom {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : incidenceGraph (Logic.PL.CSP.PPGadget.atom r).body = Graph.RotationSystem.starGraph (arity r)

The actual original-language PP atom has precisely the unbounded ordered-star graph.

theorem Cslib.Complexity.CSP.OrderedBoundary.singleScopeCertificate_accepted {Rel V : Type} [DecidableEq V] (r : Rel) (scope : List V) (hn : scope.Nodup) : verifyRotationCertificate [(r, scope)] (atomBodyCertificate scope.length) = true

A single original constraint on distinct scope names has this supplied ordered numerical table. The relation label and truth value play no role in the graph check.

theorem Cslib.Complexity.CSP.OrderedBoundary.atomBodyCertificate_accepted {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : verifyRotationCertificate (Logic.PL.CSP.PPGadget.atom r).body (atomBodyCertificate (arity r)) = true

The supplied table passes the actual atom's ordered numerical checker at every arity, including zero and one. No planarity or rotation provider is a premise.

theorem Cslib.Complexity.CSP.OrderedBoundary.atomBody_realization {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : ∃ (rot : (incidenceGraph (Logic.PL.CSP.PPGadget.atom r).body).RotationSystem), rot.NumericalGenusZero ∧ RespectsArgumentOrder rot

Every literal original-language atom internally supplies an ordered numerical realization of its actual body. An outer free-port boundary additionally needs its probe rotation.

def Cslib.Complexity.CSP.OrderedBoundary.Witness.empty {Rel V : Type} [DecidableEq V] (ports : List V) (hn : ports.Nodup) : Witness [] ports

An empty body with distinct boundary labels has a fully supplied ordered boundary of any arity. All its ports are unused; the structural probe supplies their actual corners.