Finite reference-frame structure and storage

Prescribed full words select distinct original dart ends, hence distinct fresh star leaves. This module checks the reference-order carriers and bounds their full framed storage. It makes no assertion about realizing the rank crossing bits by a proper plane drawing.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.fixedWord (I : FixedRotationInput) (v : ℕ) : List ℕ

The stored complete word, or the empty selection at a free/missing entry.

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

Original selected dart indices, in dense-center and prescribed-word order.

theorem Cslib.Complexity.Graph.RotationRecognition.fixedWord_spec {I : FixedRotationInput} (hI : Valid I) (v : ℕ) : (fixedWord I v).Nodup ∧ ∀ d ∈ fixedWord I v, d ∈ fiber I.graph v

Valid selections retain exact fiber membership and have no repeated dart.

theorem Cslib.Complexity.Graph.RotationRecognition.selectedDarts_nodup {I : FixedRotationInput} (hI : Valid I) : (selectedDarts I).Nodup

Distinct original centers select disjoint darts, even when listed edges are loops/parallel.

theorem Cslib.Complexity.Graph.RotationRecognition.length_selectedDarts_le {I : FixedRotationInput} (hI : Valid I) : (selectedDarts I).length ≤ 2 * I.graph.edges.length

At most one selected leaf per actual original dart.

theorem Cslib.Complexity.Graph.RotationRecognition.length_centerBlocks (I : FixedRotationInput) : (centerBlocks I).length = I.graph.vertices.length + (selectedDarts I).length

Centers cost one entry each; selected words cost precisely one fresh leaf per dart.

theorem Cslib.Complexity.Graph.RotationRecognition.length_referenceOrder_le {I : FixedRotationInput} (hI : Valid I) : (referenceOrder I).length ≤ I.graph.vertices.length + 4 * I.graph.edges.length

A raw reference order has at most the centers and two copies of the actual dart set.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_referenceOrder_lt {I : FixedRotationInput} (hI : Valid I) {x : ℕ} (hx : x ∈ referenceOrder I) : x < subdivisionSize I

Every reference-order entry is an actual declared subdivision vertex.

theorem Cslib.Complexity.Graph.RotationRecognition.centerBlocks_nodup {I : FixedRotationInput} (hI : Valid I) : (centerBlocks I).Nodup

Center blocks have distinct original centers and distinct fresh selected leaves.

theorem Cslib.Complexity.Graph.RotationRecognition.referenceOrder_enumerates {I : FixedRotationInput} (hI : Valid I) : (referenceOrder I).Nodup ∧ ∀ (x : ℕ), x ∈ referenceOrder I ↔ x ∈ List.range (subdivisionSize I)

The reference order contains every subdivision vertex exactly once, including isolates.

theorem Cslib.Complexity.Graph.RotationRecognition.length_referenceOrder {I : FixedRotationInput} (hI : Valid I) : (referenceOrder I).length = subdivisionSize I

The complete rank table has precisely the declared subdivided vertex count.

def Cslib.Complexity.Graph.RotationRecognition.frozenGraph (I : FixedRotationInput) : Graph

Spanning frozen subgraph on every subdivision vertex, retaining precisely flagged segments.

theorem Cslib.Complexity.Graph.RotationRecognition.frozen_edge_shape {I : FixedRotationInput} (hI : Valid I) {e : ℕ × ℕ} (he : e ∈ (frozenGraph I).edges) : ∃ (center : ℕ) (leaf : ℕ), center < I.graph.vertices.length ∧ I.graph.vertices.length ≤ leaf ∧ leaf < subdivisionSize I ∧ (e = (center, leaf) ∨ e = (leaf, center)) ∧ (I.orders.getD center none).isSome = true ∧ I.graph.incidenceVertices.getD (leaf - I.graph.vertices.length) 0 = center

Every frozen segment joins an original center to its own occurrence-indexed fresh leaf. The original endpoint reader fixes the center uniquely from that leaf. Middle edges are absent.

theorem Cslib.Complexity.Graph.RotationRecognition.frozen_leaf_unique {I : FixedRotationInput} (hI : Valid I) {leaf u v : ℕ} (hl : I.graph.vertices.length ≤ leaf) (hu : (u, leaf) ∈ (frozenGraph I).edges ∨ (leaf, u) ∈ (frozenGraph I).edges) (hv : (v, leaf) ∈ (frozenGraph I).edges ∨ (leaf, v) ∈ (frozenGraph I).edges) : u = v

Every selected subdivision leaf belongs to exactly one center. Together with frozen_edge_shape, this describes disjoint spanning stars and isolated points.

theorem Cslib.Complexity.Graph.RotationRecognition.length_encFrame_le {I : FixedRotationInput} (hI : Valid I) {K : ℕ} (hK : 1 ≤ K) (hn : I.graph.vertices.length ≤ K) (hm : I.graph.edges.length ≤ K) : (encFrame (frame I)).length ≤ 400 * K ^ 2

Full framed algebraic-frame storage is quadratically bounded in uniform original graph sizes. Unary stride, binary endpoint pairs, frozen flags, and binary reference entries count.