Removing the last argument of the last indexed constraint

The source and target are the actual CSP lists, with every earlier argument and constraint position retained. The temporary graph is exactly the source incidence edge prefix, using the source's dense names. Its explicit dart map to the actual target graph preserves the endpoint-fiber partition even if the removed variable ceases to occur. Declared nullaries and points require no fabricated darts. These are original positional transport facts for boundary projection. Native cyclic-successor formulas retain the inherited directed order. The complete computed-table acceptance theorem is in CSP.OrderedBoundary.verifyRotationCertificate_restrictPrefix_lastArgument.

Main definitions

• Cslib.Complexity.CSP.deleteLastArgumentRotation: explicit target incidence rotation.

Main results

• Cslib.Complexity.CSP.numericalGenusZero_deleteLastArgumentRotation: target numerical genus.
• Cslib.Complexity.CSP.argumentNextIndex_append_last_argument: exact native successor change.

theorem Cslib.Complexity.CSP.argumentPositions_append_last_argument {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) : argumentPositions (F ++ [(r, scope ++ [v])]) = argumentPositions (F ++ [(r, scope)]) ++ [(List.length F, scope.length)]

The actual argument-position table gains precisely the last argument's indexed pair.

theorem Cslib.Complexity.CSP.scopeLength_append_last_argument {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (i : ℕ) : scopeLength (F ++ [(r, scope ++ [v])]) i = scopeLength (F ++ [(r, scope)]) i + if i = List.length F then 1 else 0

Only the last constraint's scope length changes, including a nullary target scope. Missing constraint indices still read zero on both actual input lists.

theorem Cslib.Complexity.CSP.scopeLength_last_constraint {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) : scopeLength (F ++ [(r, scope)]) (List.length F) = scope.length

The last declared constraint has its literal supplied scope length, including zero.

theorem Cslib.Complexity.CSP.argumentNextIndex_append_last_argument {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (o : (F ++ [(r, scope)]).Occurrence) : argumentNextIndex (F ++ [(r, scope ++ [v])]) ↑o.fst ↑o.snd = if ↑o.fst = List.length F ∧ ↑o.snd + 1 = scope.length then (F ++ [(r, scope)]).occurrences.length else argumentNextIndex (F ++ [(r, scope)]) ↑o.fst ↑o.snd

The only old argument whose native successor changes is the former last argument of the last constraint. It now leads to the single appended occurrence.

theorem Cslib.Complexity.CSP.argumentNextIndex_append_last_argument_wrap {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (o : (F ++ [(r, scope)]).Occurrence) (hi : ↑o.fst = List.length F) (hj : ↑o.snd + 1 = scope.length) : argumentNextIndex (F ++ [(r, scope ++ [v])]) (List.length F) scope.length = argumentNextIndex (F ++ [(r, scope)]) ↑o.fst ↑o.snd

The appended argument wraps to the same first argument as the former last argument. The actual old occurrence hypothesis covers precisely the nonempty target scope case.

def Cslib.Complexity.CSP.lastArgumentPrefixGraph {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) : Graph

The actual source incidence prefix before its last argument edge. Its declarations and dense endpoint names are still those of the source, including a now isolated variable.

theorem Cslib.Complexity.CSP.incidenceGraph_append_last_argument {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) : incidenceGraph (F ++ [(r, scope ++ [v])]) = Graph.RotationSystem.lastEdgeGraph (lastArgumentPrefixGraph F r scope v) (List.idxOf v (F ++ [(r, scope ++ [v])]).distinctVars) ((F ++ [(r, scope ++ [v])]).numVars + List.length F)

Source incidence is literally this prefix followed by the selected final edge.

def Cslib.Complexity.CSP.lastArgumentDartEquiv {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) : (lastArgumentPrefixGraph F r scope v).Dart ≃ (incidenceGraph (F ++ [(r, scope)])).Dart

Retained prefix ends and target incidence ends have the same edge/end positions.

theorem Cslib.Complexity.CSP.vertex_lastArgumentDartEquiv_symm {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (o : (F ++ [(r, scope)]).Occurrence) (side : Bool) : ((lastArgumentDartEquiv F r scope v).symm (incidenceDart o side)).vertex = if side = true then (F ++ [(r, scope ++ [v])]).numVars + ↑o.fst else List.idxOf o.var (F ++ [(r, scope ++ [v])]).distinctVars

Literal source-dense endpoint read on an actual retained target argument occurrence.

theorem Cslib.Complexity.CSP.vertex_lastArgumentDartEquiv_symm_eq_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (o p : (F ++ [(r, scope)]).Occurrence) (side other : Bool) : ((lastArgumentDartEquiv F r scope v).symm (incidenceDart o side)).vertex = ((lastArgumentDartEquiv F r scope v).symm (incidenceDart p other)).vertex ↔ (incidenceDart o side).vertex = (incidenceDart p other).vertex

The retained actual occurrences have exactly the same vertex fibers in the source prefix and target graph. This allows repeated labels and disappearing unused variables.

theorem Cslib.Complexity.CSP.lastArgumentDartEquiv_vertex_eq_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (a b : (lastArgumentPrefixGraph F r scope v).Dart) : ((lastArgumentDartEquiv F r scope v) a).vertex = ((lastArgumentDartEquiv F r scope v) b).vertex ↔ a.vertex = b.vertex

The positional dart equivalence has the exact endpoint-fiber contract required by generic rotation transport. No injection on old variable labels is assumed.

theorem Cslib.Complexity.CSP.lastArgumentDartEquiv_reverse {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (a : (lastArgumentPrefixGraph F r scope v).Dart) : (lastArgumentDartEquiv F r scope v) a.reverse = ((lastArgumentDartEquiv F r scope v) a).reverse

Reversal is preserved literally by the retained edge/end map.

def Cslib.Complexity.CSP.lastArgumentSourceRotation {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.RotationSystem.lastEdgeGraph (lastArgumentPrefixGraph F r scope v) (List.idxOf v (F ++ [(r, scope ++ [v])]).distinctVars) ((F ++ [(r, scope ++ [v])]).numVars + List.length F)).RotationSystem

Reinterpret the actual source incidence graph as its retained prefix and last edge. The dart equivalence is literal on edge indices and end tags.

def Cslib.Complexity.CSP.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) : (incidenceGraph (F ++ [(r, scope)])).RotationSystem

Delete the final argument on the original CSP lists. The two explicit transports retain all old edge/end positions while accounting for changed dense vertex names.

theorem Cslib.Complexity.CSP.lastArgumentPrefixGraph_endpoints_declared {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (w : ℕ) : w ∈ (lastArgumentPrefixGraph F r scope v).incidenceVertices → w ∈ (lastArgumentPrefixGraph F r scope v).vertices

The actual retained incidence prefix declares all of its edge endpoints.

theorem Cslib.Complexity.CSP.numericalGenusZero_lastArgumentSourceRotation {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (r : Rel) (scope : List V) (v : V) (ρ : (incidenceGraph (F ++ [(r, scope ++ [v])])).RotationSystem) (hρ : ρ.NumericalGenusZero) : (lastArgumentSourceRotation F r scope v ρ).NumericalGenusZero

Source numerical genus is retained by its literal prefix-plus-last-edge view.

theorem Cslib.Complexity.CSP.numericalGenusZero_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) (hρ : ρ.NumericalGenusZero) : (deleteLastArgumentRotation F r scope v ρ).NumericalGenusZero

Last-argument deletion has actual target numerical genus zero, internally supplied by general edge deletion and positional incidence transport. The source rotation may have repeated variable labels, repeated constraints, arbitrary other components and nullaries.