Original-input bounds for sparse rotation queries

All bounds use the existing framed CSP encoding, including relation records, binary variable names and actual ordered scope lists. Nullary points are funded by constraint framing. No bound on a source label's numerical value, or on declared relation arity, is used.

theorem Cslib.Complexity.Graph.RotationRecognition.scopes_add_constraints_le {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (F : Logic.PL.CSP Rel V) : (List.map (fun (c : Logic.PL.Constraint Rel V) => c.2.length) F).sum + List.length F ≤ ((encCSP encRel encV) F).length

Actual scope occurrences plus constraint positions are bounded by the full CSP bit length.

theorem Cslib.Complexity.Graph.RotationRecognition.incidence_sizes_le {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (F : Logic.PL.CSP Rel V) : (CSP.incidenceGraph F).vertices.length ≤ ((encCSP encRel encV) F).length ∧ (CSP.incidenceGraph F).edges.length ≤ ((encCSP encRel encV) F).length

Dense incidence vertices and listed occurrences are each bounded by original encoded size.

theorem Cslib.Complexity.Graph.RotationRecognition.frame_sizes_split_le {I : FixedRotationInput} {B : ℕ} (hn : I.graph.vertices.length ≤ B) (hm : I.graph.edges.length ≤ B) (v : ℕ) (block : List ℕ) : (frame (split I v block)).vertexCount ≤ 3 * (B + 1) ∧ (frame (split I v block)).segments.length ≤ 3 * (B + 1)

Any one-hub split of an original bounded graph has at most 3(B+1) subdivided vertices and segments. The statement is all-raw and does not require a feasibility premise.

theorem Cslib.Complexity.Graph.RotationRecognition.length_encoding_compile_le_of_sizes {I : FixedRotationInput} (hI : Valid I) {K : ℕ} (hn : (frame I).vertexCount ≤ 3 * K) (hm : (frame I).segments.length ≤ 3 * K) : (XORSAT.encoding (compile I)).length ≤ 9 * K ^ 2 * (32 * ((9 * K ^ 2).log2 + 1) + 21)

Explicit full framed-system bit bound for every valid query with the uniform segment and vertex budgets. It includes equation pairs, binary labels, right-hand sides and outer framing.

theorem Cslib.Complexity.Graph.RotationRecognition.length_encoding_compile_split_ofCSP_le {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (F : Logic.PL.CSP Rel V) (v : ℕ) (block : List ℕ) (h : Valid (split (ofCSP F) v block)) : (XORSAT.encoding (compile (split (ofCSP F) v block))).length ≤ 9 * (((encCSP encRel encV) F).length + 1) ^ 2 * (32 * ((9 * (((encCSP encRel encV) F).length + 1) ^ 2).log2 + 1) + 21)

A valid original CSP split query has the full memo bit bound with K=B+1.

theorem Cslib.Complexity.Graph.RotationRecognition.length_encFrame_split_ofCSP_le {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (F : Logic.PL.CSP Rel V) (v : ℕ) (block : List ℕ) (h : Valid (split (ofCSP F) v block)) : (encFrame (frame (split (ofCSP F) v block))).length ≤ 400 * (((encCSP encRel encV) F).length + 1) ^ 2

The temporary original-CSP frame, including reference order and frozen flags, has quadratic full framed storage in the original binary input length.

theorem Cslib.Complexity.Graph.RotationRecognition.length_encoding_compile_ofCSP_le {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (F : Logic.PL.CSP Rel V) : (XORSAT.encoding (compile (ofCSP F))).length ≤ 9 * (((encCSP encRel encV) F).length + 1) ^ 2 * (32 * ((9 * (((encCSP encRel encV) F).length + 1) ^ 2).log2 + 1) + 21)

Full framed XOR storage of the initial bare original-CSP query.