Actual CSP last-argument deletion and the boundary restriction program

The positional incidence transports retain the literal generated table, even when dense variable and constraint names change. This identifies actual CSP deletion with the existing bounded boundary scan. Accepted raw certificates supply their own exact clock length. Target rotation validity, clockwise argument order and componentwise numerical genus are proved internally. In gadget recipes this structural deletion removes a probe argument; original-language relation scopes and their semantics are retained separately by the recipe.

Main results

• Cslib.Complexity.CSP.OrderedBoundary.ofRotation_deleteLastArgumentRotation: exact output table.
• Cslib.Complexity.CSP.OrderedBoundary.verifyRotationCertificate_restrictPrefix_lastArgument: ordered numerical target acceptance from the actual supplied source certificate.

theorem Cslib.Complexity.CSP.OrderedBoundary.length_accepted_lastArgument_certificate {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (c : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph (F ++ [(r, scope ++ [v])])) c = true) : c.successor.length = 2 * ((F ++ [(r, scope)]).occurrences.length + 1)

An accepted source table funds the scan by its actual occurrence count, including the one final argument being removed. This applies directly to raw supplied certificates.

theorem Cslib.Complexity.CSP.OrderedBoundary.ofRotation_deleteLastArgumentRotation {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (ρ : (incidenceGraph (F ++ [(r, scope ++ [v])])).RotationSystem) : Graph.RotationCertificate.ofRotation (deleteLastArgumentRotation F r scope v ρ) = restrictPrefix (2 * (F ++ [(r, scope)]).occurrences.length) (Graph.RotationCertificate.ofRotation ρ)

Actual CSP scope deletion produces exactly the boundary program's table. The equality accounts for changing dense vertex names through positional dart transport.

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

On an accepted raw numerical source certificate, the literal boundary restriction passes the actual target numerical checker. Dense renaming, repeated variables and nullary or disconnected constraints are handled internally by positional transport.

theorem Cslib.Complexity.CSP.OrderedBoundary.verifyArgumentOrder_restrictPrefix_lastArgument {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (c : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph (F ++ [(r, scope ++ [v])])) c = true) (ho : verifyArgumentOrder (F ++ [(r, scope ++ [v])]) c = true) : verifyArgumentOrder (F ++ [(r, scope)]) (restrictPrefix (2 * (F ++ [(r, scope)]).occurrences.length) c) = true

An accepted raw source rotation retains its clockwise cyclic argument order under the actual last-argument restriction program. The source checker supplies the scan clock.

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

Full ordered numerical acceptance of the computed target certificate on the original CSP lists. Source acceptance is the only certificate premise: target rotation, argument order and componentwise numerical genus are all proved internally.