2.13. Frozen XOR Queries and Checked Recovery🔗

Start a standalone client with these ordinary runtime imports:

import CslibFrontier.Computability.PolyTime.Graph.RotationSystem.Recognition.Query
import
  CslibFrontier.Computability.PolyTime.Graph.RotationSystem.Recognition.Recovery

The namespace is Cslib.Complexity.Graph.RotationRecognition. Cslib.Complexity.Graph.RotationRecognition.FixedRotationInput stores an existing listed graph and one optional complete clockwise dart word per vertex. Validity requires declarations List.range n, endpoints below n, an order table of length n, and duplicate-free full fibers at prescribed vertices. none leaves a vertex free; some [] prescribes an isolated vertex. The full cyclic successor is fixed without reflection. A directed Consecutive block constrains only internal adjacencies, without closing its last entry to its first.

The actual query validates and calls the native XOR solver. These small examples check an isolate and reject a missing table entry:

open Cslib.Complexity.Graph.RotationRecognition in
example : query ⟨⟨[0], []⟩, [some []]⟩ = true := by⊢ query { graph := { vertices := [0], edges := [] }, orders := [some []] } = true decide +kernelAll goals completed! 🐙

open Cslib.Complexity.Graph.RotationRecognition in
example : recover ⟨⟨[0], []⟩, []⟩ = none := by⊢ recover { graph := { vertices := [0], edges := [] }, orders := [] } = none decide +kernelAll goals completed! 🐙

Each listed edge is replaced by three indexed segments. Prescribed endpoints freeze their first/last segments; middle segments stay movable. Independent unordered segment pairs give affine rows of width at most four. Query acceptance means exactly valid input and solvability of these concrete equations:

open Cslib.Complexity Cslib.Complexity.Graph.RotationRecognition in
example (I : FixedRotationInput) :
    query I = true ↔ Valid I ∧ XORSAT.Satisfiable (compile I) :=
  query_eq_true_iff I

The finite semantics and budget examples also use the chapter's ordinary imports CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Recognition.CSPBounds and CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Recognition.RecoveryBudget. CSPBounds publicly imports Recognition.Moves. A finite witness has one bit per segment/vertex pair, with actual zeros at frozen coordinates:

open Cslib.Complexity.Graph.RotationRecognition in
example (I : FixedRotationInput) :
    query I = true ↔ Valid I ∧ ∃ moves : Moves (frame I),
      FrozenMoves (frame I) moves ∧ MoveEquations (frame I) moves :=
  query_eq_true_iff_exists_frozen_moves I

These equations reconstruct Schaefer, Toward a Theory of Planarity, §§5.3–5.4, pp. 399–401. Their identification with drawings is open. The proposed use of Fulek–Kynčl–Pálvölgyi, arXiv:1612.00688v3, Theorem 1, p. 2, is also unformalized; see the source mapping. Contiguous candidate recovery is original.

recover tests append candidates on ephemeral splits. A split redirects the selected ends to a fresh hub, appends a nonloop connector, and prescribes the hub's full order block ++ [2m], leaving the source free. The connector need not be a bridge. The outer state keeps the original graph and current order table; query systems do not accumulate. Returned tables pass the existing numerical genus-zero checker and the original full-order guard:

open Cslib.Complexity Cslib.Complexity.Graph.RotationRecognition in
example {I : FixedRotationInput} {c : Graph.RotationCertificate}
    (h : recover I = some c) :
    Graph.RotationCertificate.verifyGenusZero I.graph c = true ∧
      verifyFixed I c = true :=
  recover_sound h

open Cslib.Complexity Cslib.Complexity.Graph.RotationRecognition in
example {I : FixedRotationInput} {c : Graph.RotationCertificate}
    (h : recover I = some c) : Feasible I ∧
      c.successor.length = 2 * I.graph.2.length :=
  ⟨recover_feasible h, length_recover_successor h⟩

ofCSP uses the actual dense incidence graph. Variables are free; indexed constraints prescribe their actual cyclic scope orders, retaining repeated variables, duplicate constraints and nullaries. Relation semantics and arity metadata are ignored. recoverCSP additionally checks the original CSP order:

open Cslib.Logic.PL Cslib.Complexity
  Cslib.Complexity.Graph.RotationRecognition in
example {F : CSP Unit ℕ} {c : Graph.RotationCertificate}
    (h : recoverCSP F = some c) :
    Cslib.Complexity.CSP.verifyRotationCertificate F c = true :=
  recoverCSP_sound h

Even a false nullary relation can return a certificate; satisfiability is a separate semantic question:

open Cslib.Logic.PL Cslib.Complexity.Graph.RotationRecognition in
example : recoverCSP ([(false, [])] : CSP Bool ℕ) = some ⟨[]⟩ :=
  by⊢ recoverCSP [(false, [])] = some { successor := [] } decide +kernelAll goals completed! 🐙

none may mean invalid input, a false XOR query, exhausted candidates or a failed final guard. It implies neither nonplanarity nor CSP unsatisfiability. The actual runtime certificates cover every raw input, including malformed orders and arbitrarily large binary names; no solver or resource provider is supplied:

open Cslib.Complexity Cslib.Complexity.Graph.RotationRecognition
  Turing.MultiTapeTM in
example : ComputableInPolyTime query encFixedRotationInput encBool :=
  query_polyTime

open Cslib.Complexity Cslib.Complexity.Graph
  Cslib.Complexity.Graph.RotationRecognition Turing.MultiTapeTM in
example : ComputableInPolyTime recover encFixedRotationInput
    (encOption encRotationCertificate) :=
  recover_polyTime

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.Graph
  Cslib.Complexity.Graph.RotationRecognition Turing.MultiTapeTM in
example : ComputableInPolyTime (recoverCSP (Rel := Unit) (V := ℕ))
    (encCSP encUnit encNat) (encOption encRotationCertificate) :=
  recoverCSP_polyTime encUnit encNat

With m original edges, the initial query and charged candidate scans total at most 1 + 2m²; fixed constraint vertices improve this to 1 + m² for CSPs, where m is the actual scope-occurrence count. These charges are not runtime exponents:

open Cslib.Complexity Cslib.Complexity.Graph.RotationRecognition in
example (I : FixedRotationInput) :
    1 + recoveryWork (List.range I.graph.1.length) (some I) ≤
      1 + 2 * I.graph.2.length ^ 2 :=
  recoveryWork_le I

open Cslib.Logic.PL Cslib.Complexity
  Cslib.Complexity.Graph.RotationRecognition in
example (F : CSP Unit ℕ) :
    1 + recoveryWork (List.range (CSP.incidenceGraph F).1.length)
      (some (ofCSP F)) ≤ 1 + (CSP.incidenceGraph F).2.length ^ 2 :=
  recoveryWork_ofCSP_le F

All sizes include framing and binary labels. Put K = B + 1 for the original CSP encoded length B. Initial XOR storage is at most 9K² * (32 * (log₂(9K²) + 1) + 21) bits. A split has the same bound under its validity guard; arbitrary malformed split blocks do not satisfy this premise:

open Cslib.Logic.PL Cslib.Complexity
  Cslib.Complexity.Graph.RotationRecognition Turing.MultiTapeTM in
example (F : CSP Unit ℕ) (v : ℕ) (block : List ℕ)
    (h : Valid (split (ofCSP F) v block)) :
    let K := (encCSP encUnit encNat F).length + 1
    (XORSAT.encoding (compile (split (ofCSP F) v block))).length ≤
      9 * K ^ 2 * (32 * (Nat.log2 (9 * K ^ 2) + 1) + 21) :=
  length_encoding_compile_split_ofCSP_le encUnit encNat F v block h

Successful output has 2m successors and full encoded length at most 2m * (4m + 1). The outer fold preserves the original graph and table width. Dense labels never erase distinct occurrences. Dvořák–Kupec's constraint-set model and indexed duplicate-preserving CSPs need a separate model bridge.

The full objective in issue #3091 stays open. Required proofs are Valid I → (XORSAT.Satisfiable (compile I) ↔ Feasible I), split feasibility equivalent to original numerical genus zero plus Realizes and internal Consecutive block, and geometric/source correspondence including frozen switches and Hanani–Tutte. The split equivalence must preserve clockwise order, use nonloop contraction and clean up duplicate declarations. No complete planarity recognizer or final native planarity P theorem follows from the runtime and success-soundness results above.