2.12. Finite Ordered Rotation Certificates🔗

Cslib.Complexity.Graph.RotationCertificate stores one binary successor index per indexed dart. Its checker validates a supplied permutation and vertex rotation, then checks Cslib.Complexity.Graph.RotationSystem.NumericalGenusZero: V + F = E + 2 in each edge component. Faces include fixed-point orbits. Isolated vertices use V = 1, E = 0, F = 1 without inventing darts.

The CSP checker also preserves the actual cyclic scope order. A ternary mirror can pass numerical genus zero while failing this order condition:

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.CSP in
example : verifyRotationCertificate
    ([((), [0, 1, 2])] : CSP Unit ℕ) ⟨[0, 3, 2, 5, 4, 1]⟩ = true :=
  by⊢ verifyRotationCertificate [((), [0, 1, 2])] { successor := [0, 3, 2, 5, 4, 1] } = true decideAll goals completed! 🐙

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.CSP in
example : verifyRotationCertificate
    ([((), [0, 1, 2])] : CSP Unit ℕ) ⟨[0, 5, 2, 1, 4, 3]⟩ = false :=
  by⊢ verifyRotationCertificate [((), [0, 1, 2])] { successor := [0, 5, 2, 1, 4, 3] } = false decideAll goals completed! 🐙

Cslib.Complexity.CSP.exists_bounded_rotationCertificate_iff proves that ordered numerical genus-zero rotations exist exactly when a bounded certificate is accepted. The explicit graph bound is 10 * (N + 1)^2 bits for the complete encGraph bit length N; its composition with the incidence construction is polynomial in the original CSP bit length. The full supplied-certificate checker has native polynomial time, including on malformed tables:

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.CSP
  Turing.MultiTapeTM in
example : ComputableInPolyTime
    (fun p : CSP Unit ℕ × Graph.RotationCertificate =>
      verifyRotationCertificate p.1 p.2)
    (encCSPRotationCertificate encUnit encNat) encBool :=
  computableInPolyTime_verifyRotationCertificate encUnit encNat

Original variable labels remain binary. Iteration uses actual list lengths, never a maximum label or supplied successor index. Nullary port order is vacuous; semantic rejection and exact relation arity remain separate guards. These supplied-certificate theorems leave complete bare-instance recognition, geometric correspondence and the dichotomy open. The guarded constructor below adds success soundness. The complete edge solver and finite duality follow.