Directed cyclic reindexing of an actual last constraint scope

Every scope-position permutation supplies a numerical incidence isomorphism. Ordered argument compatibility additionally requires commuting with the positive cyclic successor; that condition excludes reflection at higher arity. Body constraints and their indexed occurrences are unchanged. The selected scope is structural when used for a boundary probe.

theorem Cslib.Complexity.CSP.argumentSuccessor_reindexLastScopeOccurrenceEquiv {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (hq : ∀ (j : Fin n), q ((finRotate n) j) = (finRotate n) (q j)) (o : (F ++ [(r, List.ofFn scope)]).Occurrence) : (F.reindexLastScopeOccurrenceEquiv r scope q) (argumentSuccessor o) = argumentSuccessor ((F.reindexLastScopeOccurrenceEquiv r scope q) o)

A last-scope reindexing intertwines actual clockwise argument succession when its positional permutation commutes with the positive cycle. Arity zero remains vacuous.

noncomputable def Cslib.Complexity.CSP.reindexLastScopeRotation {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (rho : (incidenceGraph (F ++ [(r, List.ofFn scope)])).RotationSystem) : (incidenceGraph (F ++ [(r, List.ofFn (scope ∘ ⇑q))])).RotationSystem

Construct the target rotation from the actual source, with an explicit positional scope bijection. This supplies no order claim for an arbitrary noncyclic scope permutation.

theorem Cslib.Complexity.CSP.numericalGenusZero_reindexLastScopeRotation {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (rho : (incidenceGraph (F ++ [(r, List.ofFn scope)])).RotationSystem) (hr : rho.NumericalGenusZero) : (reindexLastScopeRotation F r scope q rho).NumericalGenusZero

Numerical genus is retained internally on the actual target incidence graph, including closed components, nullaries, repeated variable names and empty scopes.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_reindexLastScopeRotation {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (hq : ∀ (j : Fin n), q ((finRotate n) j) = (finRotate n) (q j)) (rho : (incidenceGraph (F ++ [(r, List.ofFn scope)])).RotationSystem) (hr : RespectsArgumentOrder rho) : RespectsArgumentOrder (reindexLastScopeRotation F r scope q rho)

Clockwise source order is retained with the explicit positive-cycle commutation hypothesis; no target order or genus provider is assumed.

noncomputable def Cslib.Complexity.CSP.reindexLastScopeCertificate {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph (F ++ [(r, List.ofFn scope)])) c = true) : Graph.RotationCertificate

Static finite table obtained by the explicit occurrence conjugacy of the decoded raw source. This constructor makes no uniform native runtime assertion.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_reindexLastScopeCertificate {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (hq : ∀ (j : Fin n), q ((finRotate n) j) = (finRotate n) (q j)) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph (F ++ [(r, List.ofFn scope)])) c = true) (h : verifyRotationCertificate (F ++ [(r, List.ofFn scope)]) c = true) : verifyRotationCertificate (F ++ [(r, List.ofFn (scope ∘ ⇑q))]) (reindexLastScopeCertificate F r scope q c hrot) = true

The actual target checker accepts the constructed conjugated table when the source check accepts and the supplied scope permutation preserves the positive cyclic successor.

theorem Cslib.Complexity.CSP.getD_reindexLastScopeCertificate_of_step {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (q : Equiv.Perm (Fin n)) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph (F ++ [(r, List.ofFn scope)])) c = true) (o p : (F ++ [(r, List.ofFn scope)]).Occurrence) (side other : Bool) (hstep : c.successor.getD (incidenceDart o side).index 0 = (incidenceDart p other).index) : (reindexLastScopeCertificate F r scope q c hrot).successor.getD (incidenceDart ((F.reindexLastScopeOccurrenceEquiv r scope q) o) side).index 0 = (incidenceDart ((F.reindexLastScopeOccurrenceEquiv r scope q) p) other).index

Each actual supplied source-table step becomes its exact reindexed target-table step. This supports complete generated-table inspection without reducing choice-based inverse coordinates or assuming a target certificate.