Removing the structural boundary probe

The probe contributes a suffix of positional occurrences. Its nullary case is a declared point and leaves the exact supplied body table unchanged. These original structural facts keep all original-language constraints and their argument orders intact.

Main results

• Cslib.Complexity.CSP.OrderedBoundary.bodyCertificate_accepted_of_probe: actual body acceptance extracted internally from a supplied probe certificate, with the explicit ports.Nodup guard.
• Cslib.Complexity.CSP.OrderedBoundary.Witness.ofProbe: constructs the complete checked witness.
• Cslib.Complexity.CSP.OrderedBoundary.Witness.forgetHead: deletes one actual boundary marker.

theorem Cslib.Complexity.CSP.OrderedBoundary.occurrences_probeBody {Rel V : Type} (F : Logic.PL.CSP Rel V) (ports : List V) : (probeBody F ports).occurrences = F.occurrences ++ List.map (fun (x : V × ℕ) => match x with | (v, j) => (List.length F, j, v)) ports.reverse.zipIdx

The probe's reversed scope contributes a literal suffix of indexed argument records.

theorem Cslib.Complexity.CSP.OrderedBoundary.length_occurrences_probeBody {Rel V : Type} (F : Logic.PL.CSP Rel V) (ports : List V) : (probeBody F ports).occurrences.length = F.occurrences.length + ports.length

Probe edge counts use the actual boundary word, even when names repeat.

theorem Cslib.Complexity.CSP.OrderedBoundary.incidenceEdgeIndex_probeBody_lt_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (o : (probeBody F ports).Occurrence) : incidenceEdgeIndex o < F.occurrences.length ↔ ↑o.fst < List.length F

A source occurrence belongs to the body prefix exactly when its constraint position precedes the structural probe center. This concerns positions, not distinct scope records.

theorem Cslib.Complexity.CSP.OrderedBoundary.constraint_of_probe_occurrence {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (o : (probeBody F ports).Occurrence) (ho : F.occurrences.length ≤ incidenceEdgeIndex o) : ↑o.fst = List.length F

A deleted probe occurrence lies at the one appended constraint center.

theorem Cslib.Complexity.CSP.OrderedBoundary.probe_occurrence_eq_of_var_eq {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (hn : ports.Nodup) (o p : (probeBody F ports).Occurrence) (ho : F.occurrences.length ≤ incidenceEdgeIndex o) (hp : F.occurrences.length ≤ incidenceEdgeIndex p) (hv : o.var = p.var) : o = p

Distinct named boundary ports supply at most one probe occurrence at each variable. Body occurrences may repeat labels and constraint records arbitrarily.

theorem Cslib.Complexity.CSP.OrderedBoundary.probe_dart_eq_of_body_vertex {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (hn : ports.Nodup) (d a b : (incidenceGraph (probeBody F ports)).Dart) (hd : ↑d.1 < F.occurrences.length) (ha : F.occurrences.length ≤ ↑a.1) (hb : F.occurrences.length ≤ ↑b.1) (hav : a.vertex = d.vertex) (hbv : b.vertex = d.vertex) : a = b

At a vertex touched by a body dart, distinct boundary names leave at most one probe dart. Repeated body visits and cutvertices are unrestricted. The probe center is excluded by its actual constraint position, rather than by an assumed free-port injection.

theorem Cslib.Complexity.CSP.OrderedBoundary.rotate_probeBody_short_returns {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (hn : ports.Nodup) (r : (incidenceGraph (probeBody F ports)).RotationSystem) (d : (incidenceGraph (probeBody F ports)).Dart) (hd : ↑d.1 < F.occurrences.length) : ↑(r.rotate d).1 < F.occurrences.length ∨ ↑(r.rotate (r.rotate d)).1 < F.occurrences.length

A body dart returns to the body within two clockwise rotation steps when the named boundary word is duplicate-free. No face/genus premise or body-degree bound is needed.

theorem Cslib.Complexity.CSP.OrderedBoundary.probeBody_certificate_short_returns {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (ports : List V) (hn : ports.Nodup) (c : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph (probeBody F ports)) c = true) (i : ℕ) : i < 2 * F.occurrences.length → c.successor.getD i 0 < 2 * F.occurrences.length ∨ c.successor.getD (c.successor.getD i 0) 0 < 2 * F.occurrences.length

The supplied accepted table has the same two-step first-return property, at its actual body dart prefix. The length comes from occurrences, not encoded labels or successor entries.

theorem Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix_eq_self_of_verifyRotation {G : Graph} {c : Graph.RotationCertificate} (h : Graph.RotationCertificate.verifyRotation G c = true) : restrictPrefix c.successor.length c = c

An accepted raw rotation funds restriction to its full table and stays literally equal. The empty table is included; no source label or table entry supplies an iteration clock.

theorem Cslib.Complexity.CSP.OrderedBoundary.verifyRotationCertificate_probeBody_nil {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (c : Graph.RotationCertificate) : verifyRotationCertificate (probeBody F []) c = verifyRotationCertificate F c

A zero-port probe is only an isolated constraint point. Its raw ordered numerical certificate is accepted for the literal original-language body without changing the table.

theorem Cslib.Complexity.CSP.OrderedBoundary.bodyCertificate_eq_of_probe_nil {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {c : Graph.RotationCertificate} (h : verifyRotationCertificate (probeBody F []) c = true) : bodyCertificate F c = c

At zero ports the canonical executable body restriction returns the very same accepted raw table, including an empty body and arbitrary original nullary constraints.

theorem Cslib.Complexity.CSP.OrderedBoundary.bodyCertificate_accepted_of_probe {Rel V : Type} [DecidableEq V] (F : Logic.PL.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

Acceptance of the actual augmented probe table internally supplies acceptance of its canonical body restriction when the boundary names are distinct. Nullary and disconnected body constraints are retained, and the empty body needs no nonempty-alphabet premise.

def Cslib.Complexity.CSP.OrderedBoundary.Witness.ofProbe {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {ports : List V} (hn : ports.Nodup) (c : Graph.RotationCertificate) (h : verifyRotationCertificate (probeBody F ports) c = true) : Witness F ports

Construct the full actual-body boundary witness directly from its supplied probe table. Body acceptance is proved internally; this is not a template-planarity provider premise.

theorem Cslib.Complexity.CSP.OrderedBoundary.verifyRotationCertificate_restrictPrefix_probe_cons {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (p : V) (ports : List V) (c : Graph.RotationCertificate) (h : verifyRotationCertificate (probeBody F (p :: ports)) c = true) : verifyRotationCertificate (probeBody F ports) (restrictPrefix (2 * (probeBody F ports).occurrences.length) c) = true

Deleting the first marker computes an accepted probe for the inherited remaining word. The body, all original relation scopes and their clockwise argument rotations are retained.

def Cslib.Complexity.CSP.OrderedBoundary.Witness.forgetHead {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {p : V} {ports : List V} (w : Witness F (p :: ports)) (hn : ports.Nodup) : Witness F ports

Forget the first boundary marker by deleting its actual final probe argument. The original body is unchanged, including repeated body variables and closed components.