Query budgets for contiguous recovery

The bookkeeping charges the entire remaining-candidate list whenever find? is invoked, including its unvisited suffix after the first successful query. It therefore bounds every actual split-query call. It is proof bookkeeping, not a trace stored by the native program. Failure is sticky and completed blocks issue no further queries.

theorem Cslib.Complexity.Graph.RotationRecognition.remaining_append (I : FixedRotationInput) (v : ℕ) (block : List ℕ) (d : ℕ) : remaining I v (block ++ [d]) = (remaining I v block).erase d

Appending one unused candidate removes precisely that dart from the remaining list.

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

Upper charge for extension queries: one full remaining-list scan per nonempty search. The only carried simulated state is the same optional block as in advance.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.extensionWork_none (I : FixedRotationInput) (v fuel : ℕ) : extensionWork I v fuel none = 0

theorem Cslib.Complexity.Graph.RotationRecognition.twice_extensionWork_le (I : FixedRotationInput) (v fuel : ℕ) (block : List ℕ) : 2 * extensionWork I v fuel (some block) ≤ (remaining I v block).length * ((remaining I v block).length + 1)

Twice the charged queries is bounded by the triangular potential of remaining candidates, without a feasibility, validity or successful-search premise.

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

Extension-query charge for the actual starting singleton and actual fiber iteration count.

theorem Cslib.Complexity.Graph.RotationRecognition.twice_wordWork_le (I : FixedRotationInput) (v : ℕ) : 2 * wordWork I v ≤ (fiber I.graph v).length * ((fiber I.graph v).length - 1)

A degree-d free vertex charges at most d(d-1)/2 split queries.

def Cslib.Complexity.Graph.RotationRecognition.recoveryWork : List ℕ → Option FixedRotationInput → ℕ

Charged split queries in the actual outer recovery traversal. Completed fixed vertices and failed states issue no more calls. Each split graph is computed and discarded by advance.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.recoveryWork_none (vertices : List ℕ) : recoveryWork vertices none = 0

theorem Cslib.Complexity.Graph.RotationRecognition.twice_recoveryWork_le (vertices : List ℕ) (I : FixedRotationInput) : 2 * recoveryWork vertices (some I) ≤ (List.map (fun (v : ℕ) => (fiber I.graph v).length * ((fiber I.graph v).length - 1)) vertices).sum

Degree potentials add across the outer fold because successful steps keep the original listed graph. This is independent of all algebraic/topological completeness obligations.

theorem Cslib.Complexity.Graph.RotationRecognition.nodup_flatMap_fiber (G : Graph) (vertices : List ℕ) (hn : vertices.Nodup) : (List.flatMap (fiber G) vertices).Nodup

Distinct listed vertices own disjoint dart fibers, so their total degree is at most 2m, including raw graphs with undeclared endpoints, loops and parallel listed edges.

theorem Cslib.Complexity.Graph.RotationRecognition.sum_fiber_lengths_le (G : Graph) (vertices : List ℕ) (hn : vertices.Nodup) : (List.map (fun (v : ℕ) => (fiber G v).length) vertices).sum ≤ 2 * G.edges.length

Distinct listed vertices have total degree at most 2m, including on raw listed graphs.

theorem Cslib.Complexity.Graph.RotationRecognition.recoveryWork_le (I : FixedRotationInput) : 1 + recoveryWork (List.range I.graph.vertices.length) (some I) ≤ 1 + 2 * I.graph.edges.length ^ 2

The initial query plus all charged extension scans is at most 1+2m² on general all-free graphs, and hence also on any mixture of complete fixed/free vertices.

theorem Cslib.Complexity.Graph.RotationRecognition.twice_recoveryWork_preserves_le (vertices : List ℕ) (original current : FixedRotationInput) (hg : current.graph = original.graph) (hp : PreservesOrders original current) : 2 * recoveryWork vertices (some current) ≤ (List.map (fun (v : ℕ) => if (original.orders.getD v none).isSome = true then 0 else (fiber original.graph v).length * ((fiber original.graph v).length - 1)) vertices).sum

Previously fixed vertices charge zero even while other complete orders are recovered.

theorem Cslib.Complexity.Graph.RotationRecognition.white_fiber_even {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {v d : ℕ} (hv : v < F.numVars) (hd : d ∈ fiber (CSP.incidenceGraph F) v) : d ∈ List.map (fun (x : ℕ) => 2 * x) (List.range (CSP.incidenceGraph F).edges.length)

Every selected white incidence dart has an even binary index, retaining its occurrence.

theorem Cslib.Complexity.Graph.RotationRecognition.recoveryWork_ofCSP_le {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : 1 + recoveryWork (List.range (CSP.incidenceGraph F).vertices.length) (some (ofCSP F)) ≤ 1 + (CSP.incidenceGraph F).edges.length ^ 2

Original CSP recovery charges at most 1+m² queries. Constraint-side words are already complete, so only white vertices contribute, with one white end per actual occurrence.