Checked ordered boundaries of actual CSP bodies

A structural probe star meets the listed boundary positions in reverse order. Its center occupies the exterior of the gadget disk; its fixed rotation records orientation. A probe is only certificate scaffolding: it has no relation semantics and is never a constraint in the original-language gadget body. Repeated boundary names retain distinct probe occurrences. Unused free ports become probe leaves. Closed components, isolated nullary constraints, and an empty boundary remain explicit in the existing componentwise numerical checks.

The stored successor list supplies both a rotation of the probe-augmented incidence graph and, by a bounded first-return scan, the rotation of the actual unaugmented body. Both are checked by CSP.verifyRotationCertificate. No embedding oracle, geometric equivalence, or Boolean condition on a nullary relation is built into this interface.

The boundary orientation follows [DK15], Section 2, printed p. 436: port order is the reverse outer boundary order. The probe-star and executable first-return representation are original. Fulla–Živný, arXiv:1602.06323v3, Section 2.1, use ordered incidence graphs of positive-arity valued constraints; our unweighted decision bodies also retain nullaries. Their constraints are indexed, matching the positional list model here. Dvořák–Kupec instead write a set of constraint tuples; we do not deduplicate bodies or identify these source models literally. The nullary extension and probe representation are original.

def Cslib.Complexity.CSP.OrderedBoundary.probeBody {Rel V : Type} (F : Logic.PL.CSP Rel V) (ports : List V) : Logic.PL.CSP (Option Rel) V

Append one structural probe with the reversed boundary word. Old constraint/scope positions are retained; probe arguments are separate positions even at repeated names.

def Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix (darts : ℕ) (c : Graph.RotationCertificate) : Graph.RotationCertificate

Delete a suffix of darts by following successors to the first retained dart. The loop clock is the supplied list length, never a binary entry or vertex label. Invalid tables have total fallback zero; acceptance is checked separately.

theorem Cslib.Complexity.CSP.OrderedBoundary.length_restrictPrefix (darts : ℕ) (c : Graph.RotationCertificate) : (restrictPrefix darts c).successor.length = darts

The canonical body restriction retains exactly its original number of indexed darts.

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

Restrict an augmented table to the actual original-body incidence darts. Probe edges are appended after all original occurrences, independently of variable-name enumeration.

def Cslib.Complexity.CSP.OrderedBoundary.verify {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (c : Graph.RotationCertificate) : Bool

Check the same finite table as an ordered probe rotation and check its canonical restriction as an ordered rotation of the actual body. Each check uses componentwise numerical genus zero, including the isolated-point convention.

structure Cslib.Complexity.CSP.OrderedBoundary.Witness {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) : Type

A single finite table with checked boundary and actual-body rotations.

• certificate : Graph.RotationCertificate

  Successors on actual body darts followed by probe darts.

• accepted : verify F ports self.certificate = true

  Both the original body and augmented boundary checks succeed.

theorem Cslib.Complexity.CSP.OrderedBoundary.verify_eq_true_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (c : Graph.RotationCertificate) : verify F ports c = true ↔ verifyRotationCertificate F (bodyCertificate F c) = true ∧ verifyRotationCertificate (probeBody F ports) c = true

Exact split of the two executed checks.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.body_accepted {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) : verifyRotationCertificate F (bodyCertificate F w.certificate) = true

The witness supplies an accepted certificate for the literal gadget body.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.probe_accepted {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) : verifyRotationCertificate (probeBody F ports) w.certificate = true

The augmented rotation is checked with the literal reversed probe scope.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.body_realization {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) : ∃ (r : (incidenceGraph F).RotationSystem), r.NumericalGenusZero ∧ RespectsArgumentOrder r

The actual unaugmented incidence graph has an ordered componentwise numerical sphere rotation, internally extracted from this witness's concrete successor list.

theorem Cslib.Complexity.CSP.OrderedBoundary.Witness.probe_realization {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) : ∃ (r : (incidenceGraph (probeBody F ports)).RotationSystem), r.NumericalGenusZero ∧ RespectsArgumentOrder r

The structural exterior probe also supplies an actual ordered numerical rotation.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (g : Logic.PL.CSP.PPGadget arity sem R) : Type

An ordered gadget boundary uses all its actual free labels in index order, including unused labels. Existential labels and the actual body are those of PPGadget itself.