Finite invariants of candidate recovery

These invariants and storage bounds hold independently of a topological query criterion. A failed search may return none; a returned table still passes the existing checker.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_remaining {I : FixedRotationInput} {v d : ℕ} {block : List ℕ} : d ∈ remaining I v block ↔ d ∈ fiber I.graph v ∧ d ∉ block

Remaining candidates are exactly unused darts of the original endpoint fiber.

theorem Cslib.Complexity.Graph.RotationRecognition.nextCandidate_some {I : FixedRotationInput} {v d : ℕ} {block : List ℕ} (h : nextCandidate I v block = some d) : d ∈ remaining I v block ∧ query (split I v (block ++ [d])) = true

A successful first-candidate search retains the exact split-query guard.

theorem Cslib.Complexity.Graph.RotationRecognition.advance_some {I : FixedRotationInput} {v : ℕ} {block result : List ℕ} (h : advance I v (some block) = some result) : remaining I v block = [] ∧ result = block ∨ ∃ d ∈ remaining I v block, query (split I v (block ++ [d])) = true ∧ result = block ++ [d]

An extension either keeps a complete block or appends one unused, actually queried dart.

theorem Cslib.Complexity.Graph.RotationRecognition.advance_invariant {I : FixedRotationInput} {v : ℕ} {block result : List ℕ} (h : advance I v (some block) = some result) (hnd : block.Nodup) (hmem : ∀ d ∈ block, d ∈ fiber I.graph v) : result.Nodup ∧ (∀ d ∈ result, d ∈ fiber I.graph v) ∧ block <+: result ∧ result.length ≤ block.length + 1

Advancing preserves the finite endpoint fiber, duplicate freedom and directed prefix.

theorem Cslib.Complexity.Graph.RotationRecognition.recoverWord_invariant {I : FixedRotationInput} {v : ℕ} {word : List ℕ} (h : recoverWord I v = some word) : word.Nodup ∧ (∀ d ∈ word, d ∈ fiber I.graph v) ∧ word.length ≤ (fiber I.graph v).length

A successful recovered word uses at most the actual fiber length, with no repeated or invalid binary dart index. This holds on malformed input too.

theorem Cslib.Complexity.Graph.RotationRecognition.recoverWord_enumerates {I : FixedRotationInput} {v : ℕ} {word : List ℕ} (h : recoverWord I v = some word) : word.Nodup ∧ ∀ (d : ℕ), d ∈ word ↔ d ∈ fiber I.graph v

Every successful word enumerates its entire original endpoint fiber.

theorem Cslib.Complexity.Graph.RotationRecognition.length_enc_recoverWord {I : FixedRotationInput} {v : ℕ} {word : List ℕ} (h : recoverWord I v = some word) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) word).length ≤ 2 * I.graph.edges.length * (4 * I.graph.edges.length + 1)

Explicit polynomial storage for a recovered binary dart word, including its list framing.

theorem Cslib.Complexity.Graph.RotationRecognition.length_enc_advance (I : FixedRotationInput) (v : ℕ) (state : Option (List ℕ)) : ((Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (advance I v state)).length ≤ ((Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) state).length + 4 * I.graph.edges.length + 1

A raw block step grows storage by at most one bounded dart. Failure discards the block. The bound applies to every accumulator, including malformed or oversized blocks.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.graph_prescribe (I : FixedRotationInput) (v : ℕ) (word : List ℕ) : (prescribe I v word).graph = I.graph

Prescribing an order keeps the original graph unchanged.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_prescribe_orders (I : FixedRotationInput) (v : ℕ) (word : List ℕ) : (prescribe I v word).orders.length = I.orders.length

Prescribing a vertex replaces an entry; it never appends to the original order table.

theorem Cslib.Complexity.Graph.RotationRecognition.length_enc_prescribe_le (I : FixedRotationInput) (v : ℕ) (word : List ℕ) : (encFixedRotationInput (prescribe I v word)).length ≤ (encFixedRotationInput I).length + I.orders.length * (2 * (((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) word).length + 1))

A coarse all-raw storage bound for replacing one order. Counting every table entry makes this bound independent of validity and of the numerical value of the supplied vertex index.

theorem Cslib.Complexity.Graph.RotationRecognition.completeVertex_some {I J : FixedRotationInput} {v : ℕ} (h : completeVertex (some I) v = some J) : J.graph = I.graph ∧ J.orders.length = I.orders.length ∧ (encFixedRotationInput J).length ≤ (encFixedRotationInput I).length + I.orders.length * (2 * (2 * I.graph.edges.length * (4 * I.graph.edges.length + 1) + 1))

A successful outer step retains the original graph/table width and adds only bounded word storage. The statement is unconditional on raw input and algebraic completeness.

def Cslib.Complexity.Graph.RotationRecognition.outerGrowth (I : FixedRotationInput) : ℕ

One outer step's explicit all-raw encoded-storage growth budget.

theorem Cslib.Complexity.Graph.RotationRecognition.completeVertex_fold (I : FixedRotationInput) (vertices : List ℕ) : List.foldl completeVertex (some I) vertices = none ∨ ∃ (J : FixedRotationInput), List.foldl completeVertex (some I) vertices = some J ∧ J.graph = I.graph ∧ J.orders.length = I.orders.length ∧ (encFixedRotationInput J).length + 1 ≤ (encFixedRotationInput I).length + 1 + vertices.length * outerGrowth I

Every finite prefix of the outer fold retains the original graph and order width, with only polynomial storage growth. No query histories or split graphs are retained.

theorem Cslib.Complexity.Graph.RotationRecognition.recoverOrders_some {I J : FixedRotationInput} (h : recoverOrders I = some J) : J.graph = I.graph ∧ J.orders.length = I.orders.length

All original graph edges, including loops and parallel records, are unchanged by successful order recovery. Its table width is unchanged even on malformed input.

theorem Cslib.Complexity.Graph.RotationRecognition.getD_prescribe_other (I : FixedRotationInput) (v u : ℕ) (word : List ℕ) (huv : u ≠ v) : (prescribe I v word).orders.getD u none = I.orders.getD u none

Replacing one entry leaves every other vertex's order unchanged.

def Cslib.Complexity.Graph.RotationRecognition.PreservesOrders (original current : FixedRotationInput) : Prop

Every originally prescribed complete word remains literally unchanged.

theorem Cslib.Complexity.Graph.RotationRecognition.completeVertex_preserves {I J : FixedRotationInput} {v : ℕ} (h : completeVertex (some I) v = some J) : PreservesOrders I J

Completing a free vertex preserves all already prescribed words on every raw input.

theorem Cslib.Complexity.Graph.RotationRecognition.verifyFixed_realizes {I : FixedRotationInput} {c : RotationCertificate} (hrot : RotationCertificate.verifyRotation I.graph c = true) (hfixed : verifyFixed I c = true) : Realizes I (RotationCertificate.decode I.graph c hrot)

Full-order table guard implies the literal Realizes equations on the decoded rotation.

theorem Cslib.Complexity.Graph.RotationRecognition.length_recover_successor {I : FixedRotationInput} {c : RotationCertificate} (h : recover I = some c) : c.successor.length = 2 * I.graph.edges.length

A returned table has exactly one successor per original dart.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_recover_successor_lt {I : FixedRotationInput} {c : RotationCertificate} (h : recover I = some c) {d : ℕ} (hd : d ∈ c.successor) : d < 2 * I.graph.edges.length

A returned successor is an actual original dart index, even on raw malformed input.

theorem Cslib.Complexity.Graph.RotationRecognition.length_enc_recover_le {I : FixedRotationInput} {c : RotationCertificate} (h : recover I = some c) : (encRotationCertificate c).length ≤ 2 * I.graph.edges.length * (4 * I.graph.edges.length + 1)

Full framed binary storage of a returned existing certificate is explicitly quadratic in the original edge count. No trace or query system is included in the output.

theorem Cslib.Complexity.Graph.RotationRecognition.recover_feasible {I : FixedRotationInput} {c : RotationCertificate} (h : recover I = some c) : Feasible I

Successful candidate recovery supplies the existing numerical feasibility predicate, without requiring the missing algebraic completeness criterion.