Literal certificate transport under injective variable renaming

An injection on occurring variable names preserves the actual dense incidence graph, edge positions and argument-order check. The very same successor table therefore passes exactly the same ordered numerical checker. Repeated variables and constraints retain their positions; the map can behave arbitrarily on unused names. No geometric equivalence is asserted.

theorem Cslib.Logic.PL.CSP.varCNF_relabel {Rel V W : Type} (F : CSP Rel V) (f : V → W) : (relabel f F).varCNF = CNF.relabel f F.varCNF

The positive-CNF adapter commutes with variable renaming, preserving every scope position.

theorem Cslib.Logic.PL.CSP.distinctVars_relabel_of_injOn {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : CSP Rel V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars}) : (relabel f F).distinctVars = List.map f F.distinctVars

Injectivity only on occurring names preserves their first-occurrence order.

theorem Cslib.Logic.PL.CSP.numVars_relabel_of_injOn {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : CSP Rel V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars}) : (relabel f F).numVars = F.numVars

Renaming injectively on the occurring names preserves the distinct-variable count.

theorem Cslib.Logic.PL.CSP.occurrences_relabel {Rel V W : Type} (F : CSP Rel V) (f : V → W) : (relabel f F).occurrences = List.map (fun (x : ℕ × ℕ × V) => match x with | (constraintIndex, argumentIndex, variableName) => (constraintIndex, argumentIndex, f variableName)) F.occurrences

Variable renaming preserves the complete positional occurrence table.

theorem Cslib.Complexity.CSP.incidenceGraph_relabel_of_injOn {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars}) : incidenceGraph (Logic.PL.CSP.relabel f F) = incidenceGraph F

Injectivity on used names preserves the literal listed incidence multigraph.

theorem Cslib.Complexity.CSP.argumentPositions_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (f : V → W) : argumentPositions (Logic.PL.CSP.relabel f F) = argumentPositions F

Renaming variables does not alter positional constraint and argument indices.

theorem Cslib.Complexity.CSP.scopeLength_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (f : V → W) (i : ℕ) : scopeLength (Logic.PL.CSP.relabel f F) i = scopeLength F i

A variable renaming retains every original scope length, including nullary scopes.

theorem Cslib.Complexity.CSP.argumentNextIndex_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (f : V → W) (i j : ℕ) : argumentNextIndex (Logic.PL.CSP.relabel f F) i j = argumentNextIndex F i j

Exact cyclic argument successors survive arbitrary variable renaming.

theorem Cslib.Complexity.CSP.verifyArgumentOrder_relabel {Rel V W : Type} (F : Logic.PL.CSP Rel V) (f : V → W) (c : Graph.RotationCertificate) : verifyArgumentOrder (Logic.PL.CSP.relabel f F) c = verifyArgumentOrder F c

The argument-order checker retains its exact Boolean result on every supplied table.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_relabel_of_injOn {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ F.vars}) (c : Graph.RotationCertificate) : verifyRotationCertificate (Logic.PL.CSP.relabel f F) c = verifyRotationCertificate F c

The same raw certificate has the same acceptance result after an injection on used names. This preserves argument chirality as well as the componentwise numerical genus check.