Bounded contiguous-block candidate recovery

Each candidate is tested by the concrete frozen XOR query. Selected dart ends are redirected to one fresh hub, whose complete prescribed order is the block followed by a fresh connector end. The connector need not be a graph-theoretic bridge. Earlier complete orders stay on the original graph. Split query graphs are ephemeral: the loop stores only the current orders and block.

This finite self-reduction is original. Completeness requires the still separate full-query criterion and a split/nonloop-contraction theorem for directed consecutive blocks. Neither is assumed here. Every returned candidate is guarded by the existing numerical certificate checker; the CSP entry additionally runs the existing original-argument-order checker.

Main definitions

• Cslib.Complexity.Graph.RotationRecognition.split: ephemeral complete fixed/free query.
• Cslib.Complexity.Graph.RotationRecognition.recover: guarded existing graph certificate.
• Cslib.Complexity.Graph.RotationRecognition.recoverCSP: guarded original CSP certificate.

def Cslib.Complexity.Graph.RotationRecognition.redirectEnd (hub : ℕ) (block : List ℕ) (dart old : ℕ) : ℕ

Redirect one binary dart end exactly when it is selected in the block.

def Cslib.Complexity.Graph.RotationRecognition.split (I : FixedRotationInput) (v : ℕ) (block : List ℕ) : FixedRotationInput

Redirect exactly the selected binary dart ends to a fresh hub n, retaining every old edge position/end tag, then append connector (n,v). The hub's complete word is block ++ [2m]. For the intended split contract v is free and the nonempty duplicate-free block lies at v.

def Cslib.Complexity.Graph.RotationRecognition.remaining (I : FixedRotationInput) (v : ℕ) (block : List ℕ) : List ℕ

Darts still available as the next clockwise member of the current directed block.

def Cslib.Complexity.Graph.RotationRecognition.nextCandidate (I : FixedRotationInput) (v : ℕ) (block : List ℕ) : Option ℕ

First feasible append candidate, using the implemented native XOR query on each split.

def Cslib.Complexity.Graph.RotationRecognition.advance (I : FixedRotationInput) (v : ℕ) (state : Option (List ℕ)) : Option (List ℕ)

One block extension. A completed block is retained; failed search remains none.

def Cslib.Complexity.Graph.RotationRecognition.recoverWord (I : FixedRotationInput) (v : ℕ) : Option (List ℕ)

At most one extension per incident dart; an empty fiber is an empty complete word.

def Cslib.Complexity.Graph.RotationRecognition.prescribe (I : FixedRotationInput) (v : ℕ) (word : List ℕ) : FixedRotationInput

Replace one order-table entry without growing the table. All other entries are retained.

def Cslib.Complexity.Graph.RotationRecognition.completeVertex (state : Option FixedRotationInput) (v : ℕ) : Option FixedRotationInput

Complete a free vertex; prior full orders are left intact. Failed candidate search is sticky.

def Cslib.Complexity.Graph.RotationRecognition.recoverOrders (I : FixedRotationInput) : Option FixedRotationInput

Recover original-graph full words, storing no query systems or earlier split graphs.

def Cslib.Complexity.Graph.RotationRecognition.certificate (I : FixedRotationInput) : RotationCertificate

The binary successor table assembled from complete words on the original graph.

def Cslib.Complexity.Graph.RotationRecognition.verifyFixed (I : FixedRotationInput) (c : RotationCertificate) : Bool

Guard complete prescribed orders directly on a supplied successor table.

def Cslib.Complexity.Graph.RotationRecognition.recover (I : FixedRotationInput) : Option RotationCertificate

Validate the input, test its actual XOR system, recover candidates, and guard the resulting original-graph table with the existing numerical checker and the original complete orders.

def Cslib.Complexity.Graph.RotationRecognition.freePrefix (G : Graph) (k : ℕ) : FixedRotationInput

Keep a prefix of dense vertices free and prescribe full fiber orders at the remaining vertices. The raw binary cutoff is only compared, never used as a scan length.

def Cslib.Complexity.Graph.RotationRecognition.ofCSP {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : FixedRotationInput

Dense incidence input: variable vertices are free; each constraint position fixes its entire actual occurrence word. Relation semantics and declared relation arities are never inspected.

def Cslib.Complexity.Graph.RotationRecognition.recoverCSP {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : Option RotationCertificate

Bare CSP candidate recovery with the existing original CSP checker as its final guard.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_split_vertices (I : FixedRotationInput) (v : ℕ) (block : List ℕ) : (split I v block).graph.vertices.length = I.graph.vertices.length + 1

Split queries add exactly one vertex, regardless of binary names in malformed raw input.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_split_edges (I : FixedRotationInput) (v : ℕ) (block : List ℕ) : (split I v block).graph.edges.length = I.graph.edges.length + 1

Split queries retain every listed edge and append exactly one connector.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_certificate (I : FixedRotationInput) : (certificate I).successor.length = 2 * I.graph.edges.length

A constructed table has exactly one successor per original binary dart index.

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

Every returned graph candidate passes the existing numerical checker unconditionally.

theorem Cslib.Complexity.Graph.RotationRecognition.recoverCSP_sound {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {c : RotationCertificate} (h : recoverCSP F = some c) : CSP.verifyRotationCertificate F c = true

Every returned CSP candidate passes precisely the existing original CSP checker.