Finite frozen-edge parity queries

Each listed edge is replaced by three indexed segments through two fresh subdivision vertices. A completely prescribed original vertex freezes every incident first/last segment; the middle segments remain movable. The reference order lists each center followed by its selected leaves in reverse clockwise order, then the remaining subdivision points. Crossing bits use strict endpoint interleaving in that order. Independent unordered segment pairs contribute sparse XOR rows, with all frozen-edge move variables omitted.

This is a finite specialization of the equations in [Sch13], Sections 5.3–5.4, printed pp. 399–401. row_holds_iff and query_eq_true_iff prove their literal Boolean meaning using the existing native XOR solver. They assert no geometric or numerical feasibility criterion. The proposed full-rotation application of [FKP17], Theorem 1, p. 2, and the necessary drawing/parity bridges remain separate mathematical obligations.

Main definitions

• Cslib.Complexity.Graph.RotationRecognition.subdivide: twice subdivision with frozen flags.
• Cslib.Complexity.Graph.RotationRecognition.compile: sparse independent-edge equations.
• Cslib.Complexity.Graph.RotationRecognition.query: validate, compile and call XORSAT.solve.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Segment : Type

A segment retains its two endpoints and whether edge/vertex moves of this edge are frozen.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Segment.endpoints (segment : Segment) : ℕ × ℕ

The ordered endpoint pair of a subdivision segment.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Segment.source (segment : Segment) : ℕ

The source vertex of a subdivision segment.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Segment.target (segment : Segment) : ℕ

The target vertex of a subdivision segment.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Segment.frozen (segment : Segment) : Bool

Whether edge/vertex moves of this subdivision segment are frozen.

@[reducible, inline]

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

Two binary endpoints, framed together, then the frozen bit.

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

The total subdivided vertex count; only actual list lengths fund this unary count.

def Cslib.Complexity.Graph.RotationRecognition.subdivide (I : FixedRotationInput) : List Segment

Replace edge e=(u,v) by u--a_e--b_e--v, retaining all occurrence indices. A fixed endpoint freezes its entire first/last segment. Even loops and parallel edges get distinct fresh points.

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

Existing listed graph underlying the twice subdivision.

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

Center blocks with leaves in reverse prescribed clockwise order. A binary dart index d names precisely subdivision point n+d, including the two separate ends of an original loop.

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

Append subdivision points not already selected into a center block.

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

Finite algebraic frame. The count is unary; endpoint labels and reference ranks are binary.

• vertexCount : ℕ

  Declared number of vertices, used as the move-label stride.

• segments : List Segment

  Segment records, including the frozen flags.

• order : List ℕ

  Reference vertex order.

def Cslib.Complexity.Graph.RotationRecognition.instDecidableEqFrame.decEq (x✝ x✝¹ : Frame) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.Graph.RotationRecognition.instDecidableEqFrame : DecidableEq Frame

@[instance_reducible]

instance Cslib.Complexity.Graph.RotationRecognition.instReprFrame : Repr Frame

def Cslib.Complexity.Graph.RotationRecognition.instReprFrame.repr : Frame → ℕ → Std.Format

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_order_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFrame S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).order) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → List ((ℕ × ℕ) × Bool)} {x2 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encUnary) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList encSegment)) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { vertexCount := x0 x, segments := x1 x, order := x2 x }) encIn encFrame

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → List ((ℕ × ℕ) × Bool)} {x2 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encUnary budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList encSegment) budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { vertexCount := x0 x, segments := x1 x, order := x2 x }) encIn encFrame budget

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_segments_deg : Turing.MultiTapeTM.ComputableInDegree Frame.segments encFrame (Turing.MultiTapeTM.encList encSegment) 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_order_inO : Turing.MultiTapeTM.ComputableInO Frame.order encFrame (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : Frame) => (encFrame a).length) fun (a : Frame) => (encFrame a).length

@[reducible, inline]

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

The tuple of the fields of encFrame.

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_vertexCount_deg : Turing.MultiTapeTM.ComputableInDegree Frame.vertexCount encFrame Turing.MultiTapeTM.encUnary 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_vertexCount_inO : Turing.MultiTapeTM.ComputableInO Frame.vertexCount encFrame Turing.MultiTapeTM.encUnary (fun (a : Frame) => (encFrame a).length) fun (a : Frame) => (encFrame a).length

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_vertexCount_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFrame S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).vertexCount) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_order_deg : Turing.MultiTapeTM.ComputableInDegree Frame.order encFrame (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_segments_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFrame → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).segments) encIn✝ (Turing.MultiTapeTM.encList encSegment)

def Cslib.Complexity.Graph.RotationRecognition.encFrame : Frame ↪ List Bool

Unary stride, then framed binary segments and framed binary reference order.

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Frame) => (a.vertexCount, a.segments, a.order)) encFrame encFrameFields 1 1

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_apply (a : Frame) : encFrame a = encFrameFields (a.vertexCount, a.segments, a.order)

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_order_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFrame → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).order) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_segments_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFrame S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).segments) encIn✝ (Turing.MultiTapeTM.encList encSegment) S✝

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_segments_inO : Turing.MultiTapeTM.ComputableInO Frame.segments encFrame (Turing.MultiTapeTM.encList encSegment) (fun (a : Frame) => (encFrame a).length) fun (a : Frame) => (encFrame a).length

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_vertexCount_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFrame → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).vertexCount) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × List ((ℕ × ℕ) × Bool) × List ℕ) => { vertexCount := p.1, segments := p.2.1, order := p.2.2 }) encFrameFields encFrame 1 1

theorem Cslib.Complexity.Graph.RotationRecognition.encFrame_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → List ((ℕ × ℕ) × Bool)} {T1 S1 : γ → ℕ} {x2 : γ → List ℕ} {T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encUnary T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList encSegment) T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { vertexCount := x0 x, segments := x1 x, order := x2 x }) encIn encFrame (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

def Cslib.Complexity.Graph.RotationRecognition.frame (I : FixedRotationInput) : Frame

Concrete frame compiled from the raw existing graph and fixed orders.

def Cslib.Complexity.Graph.RotationRecognition.independent (e f : ℕ × ℕ) : Bool

Independent endpoints; no equation is emitted for a pair sharing a vertex.

def Cslib.Complexity.Graph.RotationRecognition.between (order : List ℕ) (e : ℕ × ℕ) (v : ℕ) : Bool

Strict interval membership of the reference rank of a vertex.

def Cslib.Complexity.Graph.RotationRecognition.crossing (order : List ℕ) (e f : ℕ × ℕ) : Bool

Reference crossing parity, computed without coordinates.

def Cslib.Complexity.Graph.RotationRecognition.moveLabel (n e v : ℕ) : ℕ

Binary label of the move of indexed segment e past vertex v.

def Cslib.Complexity.Graph.RotationRecognition.moveLabels (n i : ℕ) (e : Segment) (f : ℕ × ℕ) : List ℕ

The two endpoint move labels of an unfrozen segment, or no labels for a frozen segment.

def Cslib.Complexity.Graph.RotationRecognition.row (F : Frame) (e f : Segment × ℕ) : Logic.PL.AffineEquation ℕ

Literal sparse row for two indexed segment records. No label deduplication is performed.

def Cslib.Complexity.Graph.RotationRecognition.compileFrame (F : Frame) : XORSAT.System

Every unordered independent pair appears once, in increasing first segment index and then increasing second index. All scans traverse actual segment lists, never move-label intervals.

def Cslib.Complexity.Graph.RotationRecognition.compile (I : FixedRotationInput) : XORSAT.System

The concrete sparse system on the twice-subdivided existing graph.

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

Ordinary native XOR solving, after raw input validation. This is an algebraic query; no result identifying it with Feasible is assumed or asserted.

def Cslib.Complexity.Graph.RotationRecognition.moveValue (F : Frame) (assignment : ℕ → Bool) (e : Segment × ℕ) (v : ℕ) : Bool

A frozen segment contributes zero regardless of the assignment; an unfrozen segment reads its actual binary move label.

theorem Cslib.Complexity.Graph.RotationRecognition.row_holds_iff (F : Frame) (assignment : ℕ → Bool) (e f : Segment × ℕ) : (row F e f).Holds assignment ↔ moveValue F assignment e f.1.source + moveValue F assignment e f.1.target + (moveValue F assignment f e.1.source + moveValue F assignment f e.1.target) = crossing F.order e.1.endpoints f.1.endpoints

A sparse row states exactly the four endpoint moves with the frozen zeros retained.

theorem Cslib.Complexity.Graph.RotationRecognition.holds_compileFrame_iff (F : Frame) (assignment : ℕ → Bool) : Logic.PL.AffineSystem.Holds (compileFrame F) assignment ↔ ∀ e ∈ F.segments.zipIdx, ∀ f ∈ F.segments.zipIdx, f.2 < e.2 → independent e.1.endpoints f.1.endpoints = true → (row F e f).Holds assignment

Exact row enumeration, including the strict unordered-pair scan and independence guard.

theorem Cslib.Complexity.Graph.RotationRecognition.query_eq_true_iff (I : FixedRotationInput) : query I = true ↔ Valid I ∧ ∃ (assignment : ℕ → Bool), Logic.PL.AffineSystem.Holds (compile I) assignment

The actual native query accepts exactly valid inputs whose concrete frozen parity rows have a Boolean assignment. This uses the implemented XOR solver without a hypothesis.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_subdivide (I : FixedRotationInput) : (subdivide I).length = 3 * I.graph.edges.length

There are exactly three listed segments per original edge occurrence.

@[simp]

theorem Cslib.Complexity.Graph.RotationRecognition.length_subdivisionGraph_vertices (I : FixedRotationInput) : (subdivisionGraph I).vertices.length = I.graph.vertices.length + 2 * I.graph.edges.length

Twice subdivision has the advertised dense vertex count, including isolates.

theorem Cslib.Complexity.Graph.RotationRecognition.length_row_le (F : Frame) (e f : Segment × ℕ) : (row F e f).1.length ≤ 4

Each independent-edge row contains at most four binary move labels.

theorem Cslib.Complexity.Graph.RotationRecognition.length_compileFrame_le (F : Frame) : List.length (compileFrame F) ≤ F.segments.length ^ 2

The number of rows is at most the square of the actual segment-list length.

theorem Cslib.Complexity.Graph.RotationRecognition.moveLabel_lt {n m e v : ℕ} (he : e < m) (hv : v < n) : moveLabel n e v < m * n

A bounded endpoint produces a move label below the full rectangular move budget.