Ordered incidence certificates under relation-symbol maps

The incidence graph and exact argument-order checker depend on the positional scopes. Relation-symbol maps therefore retain the same accepted raw certificate. These structural facts permit tags for the exterior probe; arity and SAT semantics remain separate properties of an actual language interpretation.

theorem Cslib.Complexity.CSP.incidenceGraph_mapRelation {Rel Other V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (f : Rel → Other) : incidenceGraph (List.map (fun (x : Logic.PL.Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) = incidenceGraph F

A symbol map leaves every actual listed vertex and indexed edge unchanged.

theorem Cslib.Complexity.CSP.argumentPositions_mapRelation {Rel Other V : Type} (F : Logic.PL.CSP Rel V) (f : Rel → Other) : argumentPositions (List.map (fun (x : Logic.PL.Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) = argumentPositions F

The native position table is unchanged by a relation-symbol map.

theorem Cslib.Complexity.CSP.scopeLength_mapRelation {Rel Other V : Type} (F : Logic.PL.CSP Rel V) (f : Rel → Other) (i : ℕ) : scopeLength (List.map (fun (x : Logic.PL.Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) i = scopeLength F i

Scope widths are retained at every position, including missing and nullary entries.

theorem Cslib.Complexity.CSP.verifyArgumentOrder_mapRelation {Rel Other V : Type} (F : Logic.PL.CSP Rel V) (f : Rel → Other) (c : Graph.RotationCertificate) : verifyArgumentOrder (List.map (fun (x : Logic.PL.Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) c = verifyArgumentOrder F c

The argument-order check retains its literal result on every raw table.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_mapRelation {Rel Other V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (f : Rel → Other) (c : Graph.RotationCertificate) : verifyRotationCertificate (List.map (fun (x : Logic.PL.Constraint Rel V) => match x with | (r, scope) => (f r, scope)) F) c = verifyRotationCertificate F c

Symbol maps keep the exact acceptance result, without changing any scope or dart.