Full fixed rotations on dense listed graphs

This auxiliary input uses the existing listed Graph, indexed darts and rotations. A vertex is free (none) or has its entire clockwise cyclic dart order prescribed (some word). Binary dart indices retain both ends of loops and every parallel occurrence. some [] is the complete order of an isolated point. Raw input is validated before algebraic queries or recovery.

Feasible asks for the existing componentwise numerical genus-zero rotation. No equivalence with a geometric drawing, or with a parity system, is asserted here.

Main definitions

• Cslib.Complexity.Graph.RotationRecognition.FixedRotationInput: raw fixed/free input.
• Cslib.Complexity.Graph.RotationRecognition.Valid: dense closed graph and complete orders.
• Cslib.Complexity.Graph.RotationRecognition.Realizes: literal cyclic successor equations.
• Cslib.Complexity.Graph.RotationRecognition.Consecutive: internal block successor equations.

Main results

• Cslib.Complexity.Graph.RotationRecognition.Valid.edge_endpoints_lt: validity bounds both endpoints of every listed edge by the declared vertex count.

structure Cslib.Complexity.Graph.RotationRecognition.FixedRotationInput : Type

Raw dense listed graph and one optional complete binary dart order per vertex.

• graph : Graph

  The existing graph, retaining indexed edge occurrences.

• orders : List (Option (List ℕ))

  none is free; some word prescribes the complete clockwise cyclic order.

@[instance_reducible]

instance Cslib.Complexity.Graph.RotationRecognition.instDecidableEqFixedRotationInput : DecidableEq FixedRotationInput

def Cslib.Complexity.Graph.RotationRecognition.instDecidableEqFixedRotationInput.decEq (x✝ x✝¹ : FixedRotationInput) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.Graph.RotationRecognition.instReprFixedRotationInput.repr : FixedRotationInput → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.Graph.RotationRecognition.instReprFixedRotationInput : Repr FixedRotationInput

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : FixedRotationInput) => (a.graph, a.orders)) encFixedRotationInput encFixedRotationInputFields 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → FixedRotationInput} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFixedRotationInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_orders_deg : Turing.MultiTapeTM.ComputableInDegree FixedRotationInput.orders encFixedRotationInput (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → FixedRotationInput} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFixedRotationInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_graph_inO : Turing.MultiTapeTM.ComputableInO FixedRotationInput.graph encFixedRotationInput encGraph (fun (a : FixedRotationInput) => (encFixedRotationInput a).length) fun (a : FixedRotationInput) => (encFixedRotationInput a).length

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × List (Option (List ℕ))) => { graph := p.1, orders := p.2 }) encFixedRotationInputFields encFixedRotationInput 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_orders_inO : Turing.MultiTapeTM.ComputableInO FixedRotationInput.orders encFixedRotationInput (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (fun (a : FixedRotationInput) => (encFixedRotationInput a).length) fun (a : FixedRotationInput) => (encFixedRotationInput a).length

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 : γ → List (Option (List ℕ))} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, orders := x1 x }) encIn encFixedRotationInput budget

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_graph_deg : Turing.MultiTapeTM.ComputableInDegree FixedRotationInput.graph encFixedRotationInput encGraph 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_orders_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → FixedRotationInput} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFixedRotationInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).orders) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 : γ → List (Option (List ℕ))} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, orders := x1 x }) encIn encFixedRotationInput

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_orders_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → FixedRotationInput} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFixedRotationInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).orders) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) S✝

def Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput : FixedRotationInput ↪ List Bool

Framed existing binary graph, then a framed list of optional framed binary dart words.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInputFields : Graph × List (Option (List ℕ)) ↪ List Bool

The tuple of the fields of encFixedRotationInput.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_apply (a : FixedRotationInput) : encFixedRotationInput a = encFixedRotationInputFields (a.graph, a.orders)

theorem Cslib.Complexity.Graph.RotationRecognition.encFixedRotationInput_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 : γ → ℕ} {x1 : γ → List (Option (List ℕ))} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, orders := x1 x }) encIn encFixedRotationInput (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

def Cslib.Complexity.Graph.RotationRecognition.fiber (G : Graph) (v : ℕ) : List ℕ

All binary dart indices at a vertex, in edge/end order. The scan uses the actual edge count.

def Cslib.Complexity.Graph.RotationRecognition.Valid (I : FixedRotationInput) : Prop

Raw validity: dense declared vertices, closed endpoints, exact order-table width, and every prescribed word enumerating its entire endpoint fiber exactly once.

theorem Cslib.Complexity.Graph.RotationRecognition.Valid.edge_endpoints_lt {I : FixedRotationInput} (hI : Valid I) {e : ℕ × ℕ} (he : e ∈ I.graph.edges) : e.1 < I.graph.vertices.length ∧ e.2 < I.graph.vertices.length

Both endpoints of every listed edge of a valid input lie below its declared vertex count.

def Cslib.Complexity.Graph.RotationRecognition.validate (I : FixedRotationInput) : Bool

Total finite validity test; malformed binary names and indices are only compared/read.

theorem Cslib.Complexity.Graph.RotationRecognition.validate_eq_true_iff (I : FixedRotationInput) : validate I = true ↔ Valid I

Validation implements the complete fixed/free contract on every raw input.

def Cslib.Complexity.Graph.RotationRecognition.nextInWord (word : List ℕ) (i : ℕ) : ℕ

Next position in a complete cyclic word, with a total zero fallback.

def Cslib.Complexity.Graph.RotationRecognition.Realizes (I : FixedRotationInput) (r : I.graph.RotationSystem) : Prop

A rotation follows every prescribed complete cyclic word literally, without reflection. Empty prescribed words impose no successor equation.

def Cslib.Complexity.Graph.RotationRecognition.Feasible (I : FixedRotationInput) : Prop

The existing numerical feasibility predicate, with all prescribed full orders. This is an internal target for a future proved algebraic criterion, not a new definition of planarity.

def Cslib.Complexity.Graph.RotationRecognition.Consecutive {G : Graph} (r : G.RotationSystem) (block : List ℕ) : Prop

Only successive entries inside the directed block are constrained. In particular, a proper block's last entry is not required to return to its first entry.

theorem Cslib.Complexity.Graph.RotationRecognition.consecutive_singleton {G : Graph} (r : G.RotationSystem) (d : ℕ) : Consecutive r [d]

A singleton block has no internal successor equation.

theorem Cslib.Complexity.Graph.RotationRecognition.mem_fiber {G : Graph} {v d : ℕ} : d ∈ fiber G v ↔ d < 2 * G.edges.length ∧ G.incidenceVertices.getD d 0 = v

Fiber membership retains both the binary width and the exact endpoint.

theorem Cslib.Complexity.Graph.RotationRecognition.index_mem_fiber {G : Graph} (d : G.Dart) : d.index ∈ fiber G d.vertex

A dart's own binary index belongs to exactly its endpoint fiber.

theorem Cslib.Complexity.Graph.RotationRecognition.nodup_fiber (G : Graph) (v : ℕ) : (fiber G v).Nodup

Raw fibers contain no repeated dart indices, even on loops or parallel edges.

theorem Cslib.Complexity.Graph.RotationRecognition.length_fiber_le (G : Graph) (v : ℕ) : (fiber G v).length ≤ 2 * G.edges.length

Every raw fiber is bounded by the actual dart-list length.