Exact finite split input contracts

The connector is an arbitrary nonloop edge, not necessarily a bridge. This module concerns indexed endpoints and raw validity only. Numerical feasibility under the split requires the separate contraction theorem and is not asserted here.

theorem Cslib.Complexity.Graph.RotationRecognition.getD_freePrefix (G : Graph) (k v : ℕ) (hd : G.vertices = List.range G.vertices.length) (hv : v < G.vertices.length) : (freePrefix G k).orders.getD v none = if v < k then none else some (fiber G v)

Exact complete/free entry at every declared dense vertex.

theorem Cslib.Complexity.Graph.RotationRecognition.valid_freePrefix (G : Graph) (k : ℕ) (hd : G.vertices = List.range G.vertices.length) (he : ∀ v ∈ G.incidenceVertices, v < G.vertices.length) : Valid (freePrefix G k)

Dense closed graphs produce valid complete fixed/free words after any binary free cutoff.

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

The original CSP incidence entry is valid for arbitrary relation semantics/declared arity, including all nullary constraint positions and repeated scope occurrences.

theorem Cslib.Complexity.Graph.RotationRecognition.edgeEndpoint_split_old (I : FixedRotationInput) (v : ℕ) (block : List ℕ) (i : ℕ) (hi : i < I.graph.edges.length) (side : Bool) : (split I v block).graph.edgeEndpoint i side = redirectEnd I.graph.vertices.length block (2 * i + side.toNat) (I.graph.edgeEndpoint i side)

Old listed edge positions and end tags are retained exactly by split redirection.

theorem Cslib.Complexity.Graph.RotationRecognition.edgeEndpoint_split_connector (I : FixedRotationInput) (v : ℕ) (block : List ℕ) (side : Bool) : (split I v block).graph.edgeEndpoint I.graph.edges.length side = if side = true then v else I.graph.vertices.length

The connector's first/false end is the fresh hub and its second/true end is the old vertex.

theorem Cslib.Complexity.Graph.RotationRecognition.endpoint_split_old (I : FixedRotationInput) (v : ℕ) (block : List ℕ) (d : ℕ) (hd : d < 2 * I.graph.edges.length) : (split I v block).graph.incidenceVertices.getD d 0 = redirectEnd I.graph.vertices.length block d (I.graph.incidenceVertices.getD d 0)

Exact binary endpoint redirection for every original dart index.

theorem Cslib.Complexity.Graph.RotationRecognition.endpoint_split_connector (I : FixedRotationInput) (v : ℕ) (block : List ℕ) (side : Bool) : (split I v block).graph.incidenceVertices.getD (2 * I.graph.edges.length + side.toNat) 0 = if side = true then v else I.graph.vertices.length

Exact binary endpoint at either end of the appended connector.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_fiber_split_hub {I : FixedRotationInput} (hI : Valid I) {v : ℕ} (hv : v < I.graph.vertices.length) {block : List ℕ} (hb : ∀ d ∈ block, d ∈ fiber I.graph v) (d : ℕ) : d ∈ fiber (split I v block).graph I.graph.vertices.length ↔ d ∈ block ∨ d = 2 * I.graph.edges.length

The hub owns precisely the selected original ends and the connector's false end.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_fiber_split_other {I : FixedRotationInput} {v u : ℕ} (hu : u < I.graph.vertices.length) (huv : u ≠ v) {block : List ℕ} (hb : ∀ d ∈ block, d ∈ fiber I.graph v) (d : ℕ) : d ∈ fiber (split I v block).graph u ↔ d ∈ fiber I.graph u

A different old vertex retains exactly its original dart fiber.

theorem Cslib.Complexity.Graph.RotationRecognition.valid_split {I : FixedRotationInput} (hI : Valid I) {v : ℕ} (hv : v < I.graph.vertices.length) (hfree : I.orders.getD v none = none) {block : List ℕ} (hnd : block.Nodup) (hb : ∀ d ∈ block, d ∈ fiber I.graph v) : Valid (split I v block)

Raw split validity requires no numerical or geometric feasibility theorem. Prescribed old vertices retain complete orders, and the hub receives exactly the full selected word/connector.