Finite ordered incidence rotation certificates

The graph and argument occurrences are exactly those of the existing CSP incidence model. The constraint-side successor follows the original scope order, including repeated variables and identical constraint records. Nullary constraints have no argument ports; their order test is vacuous and no zero-length face is invented. A false nullary relation requires a separate satisfiability guard, which is not an order condition.

This verifies a supplied rotation with componentwise numerical Euler. It does not recognize geometric planarity, construct an embedding from a bare CSP, normalize nullary constraints, identify disconnected outer faces, or prove an ordinary planar-CSP complexity classification. The source mapping is the ordered incidence multigraph of Fulla–Živný, arXiv:1602.06323v3, Section 2.1, paragraph preceding Definition 1. The geometric face model of [KKR18], Definition 12, p. 6 is a later correspondence obligation. Fulla–Živný use weighted valued constraints of positive arity; this decision-CSP interface omits weights and retains nullary scopes as an explicit extension, without asserting their geometric face correspondence.

Main results

• Cslib.Complexity.CSP.verifyArgumentOrder_eq_true_iff: exact original cyclic argument order.
• Cslib.Complexity.CSP.exists_bounded_rotationCertificate_iff: bounded certificate completeness.
• Cslib.Complexity.CSP.computableInPolyTime_verifyRotationCertificate: native supplied-certificate verification, with arbitrary encoded source variable labels.

def Cslib.Complexity.CSP.argumentPositions {Rel V : Type} (F : Logic.PL.CSP Rel V) : List (ℕ × ℕ)

Constraint and scope positions of each existing argument occurrence, in edge-list order.

def Cslib.Complexity.CSP.scopeLength {Rel V : Type} (F : Logic.PL.CSP Rel V) (i : ℕ) : ℕ

A constraint's actual scope length, read from the input list. Missing constraints return zero; relation arities are never used as clocks.

def Cslib.Complexity.CSP.argumentNextIndex {Rel V : Type} (F : Logic.PL.CSP Rel V) (i j : ℕ) : ℕ

Edge position of the next argument, with last-to-first wraparound in its original scope.

theorem Cslib.Complexity.CSP.argumentPositions_nodup {Rel V : Type} (F : Logic.PL.CSP Rel V) : (argumentPositions F).Nodup

Distinct occurrences have distinct position pairs, even with repeated variable labels.

theorem Cslib.Complexity.CSP.scopeLength_occurrence {Rel V : Type} {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : scopeLength F ↑o.fst = F[↑o.fst].2.length

The executable length reader uses the occurrence's actual scope.

theorem Cslib.Complexity.CSP.argumentNextIndex_occurrence {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : argumentNextIndex F ↑o.fst ↑o.snd = incidenceEdgeIndex (argumentSuccessor o)

The native next-index calculation is precisely the existing cyclic argument successor.

def Cslib.Complexity.CSP.verifyArgumentOrder {Rel V : Type} (F : Logic.PL.CSP Rel V) (c : Graph.RotationCertificate) : Bool

Verify the constraint-side successor at every actual argument occurrence.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.encCSPRotationCertificate {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Logic.PL.CSP Rel V × Graph.RotationCertificate ↪ List Bool

Framed CSP followed by its finite graph-rotation certificate. The source variable encoding is explicit; graph labels and certificate successor indices remain binary.

def Cslib.Complexity.CSP.verifyRotationCertificate {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (c : Graph.RotationCertificate) : Bool

Verify supplied numerical genus zero and the original cyclic argument order together.

theorem Cslib.Complexity.CSP.verifyArgumentOrder_eq_true_iff {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {c : Graph.RotationCertificate} (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) c = true) : verifyArgumentOrder F c = true ↔ RespectsArgumentOrder (Graph.RotationCertificate.decode (incidenceGraph F) c h)

The executed argument-order check is exactly the existing RespectsArgumentOrder predicate on the decoded rotation.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_eq_true_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (c : Graph.RotationCertificate) : verifyRotationCertificate F c = true ↔ ∃ (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) c = true), (Graph.RotationCertificate.decode (incidenceGraph F) c h).NumericalGenusZero ∧ RespectsArgumentOrder (Graph.RotationCertificate.decode (incidenceGraph F) c h)

Exact finite verification on the existing ordered incidence rotation, with no geometric planarity or satisfiability assumption hidden in the statement.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_ofRotation {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hg : r.NumericalGenusZero) (ho : RespectsArgumentOrder r) : verifyRotationCertificate F (Graph.RotationCertificate.ofRotation r) = true

Every existing ordered numerical genus-zero incidence rotation has an accepted finite certificate. Original scope positions are retained; no embedding construction is assumed.

theorem Cslib.Complexity.CSP.exists_bounded_rotationCertificate_iff {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (∃ (r : (incidenceGraph F).RotationSystem), r.NumericalGenusZero ∧ RespectsArgumentOrder r) ↔ ∃ (c : Graph.RotationCertificate), (Graph.encRotationCertificate c).length ≤ 10 * ((encGraph (incidenceGraph F)).length + 1) ^ 2 ∧ verifyRotationCertificate F c = true

Supplied-certificate completeness with a concrete quadratic bound in the native incidence graph's encoded length. The graph itself is constructed natively from the CSP.

theorem Cslib.Complexity.CSP.polyBounded_rotationCertificateBound {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.PolyBounded (fun (F : Logic.PL.CSP Rel V) => ((encCSP encRel encV) F).length) fun (F : Logic.PL.CSP Rel V) => 10 * ((encGraph (incidenceGraph F)).length + 1) ^ 2

The concrete incidence-certificate bound is polynomial in the source CSP bit length for any fixed relation and variable encodings, including binary natural variable names.

theorem Cslib.Complexity.CSP.argumentNextIndex_polyTime {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CSP Rel V × ℕ) × ℕ) => argumentNextIndex p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (encCSP encRel encV) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary

Compute a cyclic argument successor from unary constraint and argument occurrence indices. The clock comes from actual scope/occurrence lists. This native runtime certificate covers all raw CSPs and indices, including missing positions, without arity or rotation-validity premises.

theorem Cslib.Complexity.CSP.computableInPolyTime_verifyArgumentOrder {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Rel V × Graph.RotationCertificate) => verifyArgumentOrder p.1 p.2) (encCSPRotationCertificate encRel encV) Turing.MultiTapeTM.encBool

The original cyclic argument-order test is native polynomial-time. All counters come from actual constraint, scope and occurrence lists, independently of relation arities and labels.

theorem Cslib.Complexity.CSP.computableInPolyTime_verifyRotationCertificate {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Rel V × Graph.RotationCertificate) => verifyRotationCertificate p.1 p.2) (encCSPRotationCertificate encRel encV) Turing.MultiTapeTM.encBool

Native polynomial-time verification of the supplied incidence rotation, componentwise numerical genus zero and the CSP's actual cyclic argument order. This supplies no solver or recognizer on a bare instance.