Finite move assignments for frozen sparse equations

Assignments have one bit per segment/vertex pair in the finite frame. Frozen segments contribute zero, including when the unused assignment bit is true. The sparse solver's arbitrary binary label assignment and this finite move semantics are equivalent; neither direction assumes any recognizer or topological theorem.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationRecognition.Moves (F : Frame) : Type

The finite rectangle of potential segment/vertex moves.

def Cslib.Complexity.Graph.RotationRecognition.readMove (F : Frame) (moves : Moves F) (e v : ℕ) : Bool

Total lookup of a finite move table, returning zero outside the rectangle.

def Cslib.Complexity.Graph.RotationRecognition.finiteMoveValue (F : Frame) (moves : Moves F) (e : Segment × ℕ) (v : ℕ) : Bool

Frozen edges contribute zero; all other entries are read from the finite move rectangle.

def Cslib.Complexity.Graph.RotationRecognition.MoveEquations (F : Frame) (moves : Moves F) : Prop

The literal independent-pair switch equations, with all frozen contributions zero.

def Cslib.Complexity.Graph.RotationRecognition.assignmentOfMoves (F : Frame) (moves : Moves F) (label : ℕ) : Bool

Decode a binary move label by quotient and remainder, with a total zero fallback.

theorem Cslib.Complexity.Graph.RotationRecognition.assignmentOfMoves_label (F : Frame) (moves : Moves F) {e v : ℕ} (hv : v < F.vertexCount) : assignmentOfMoves F moves (moveLabel F.vertexCount e v) = readMove F moves e v

Binary label decoding is exact throughout the finite move rectangle.

theorem Cslib.Complexity.Graph.RotationRecognition.holds_assignmentOfMoves_iff {F : Frame} (hF : BoundedEndpoints F) (moves : Moves F) : Logic.PL.AffineSystem.Holds (compileFrame F) (assignmentOfMoves F moves) ↔ MoveEquations F moves

Every finite move table evaluates the sparse rows exactly as the frozen switch equations.

theorem Cslib.Complexity.Graph.RotationRecognition.satisfiable_iff_exists_moves {F : Frame} (hF : BoundedEndpoints F) : XORSAT.Satisfiable (compileFrame F) ↔ ∃ (moves : Moves F), MoveEquations F moves

Sparse satisfiability is precisely existence of finitely many move bits with frozen zeros. Unused and out-of-range labels in the solver's assignment have no effect.

def Cslib.Complexity.Graph.RotationRecognition.FrozenMoves (F : Frame) (moves : Moves F) : Prop

Every stored bit at a frozen segment is literally zero.

def Cslib.Complexity.Graph.RotationRecognition.freezeMoves (F : Frame) (moves : Moves F) : Moves F

Explicitly set every frozen-edge entry of the finite rectangle to zero.

theorem Cslib.Complexity.Graph.RotationRecognition.satisfiable_iff_exists_frozen_moves {F : Frame} (hF : BoundedEndpoints F) : XORSAT.Satisfiable (compileFrame F) ↔ ∃ (moves : Moves F), FrozenMoves F moves ∧ MoveEquations F moves

Frozen coordinates can actually be zero in the finite witness, not merely omitted from its sparse variable list. No value of an unused solver label is treated as a permitted move.

theorem Cslib.Complexity.Graph.RotationRecognition.query_eq_true_iff_exists_moves (I : FixedRotationInput) : query I = true ↔ Valid I ∧ ∃ (moves : Moves (frame I)), MoveEquations (frame I) moves

The actual validated native query decides exactly existence of finite frozen move bits.

theorem Cslib.Complexity.Graph.RotationRecognition.query_eq_true_iff_exists_frozen_moves (I : FixedRotationInput) : query I = true ↔ Valid I ∧ ∃ (moves : Moves (frame I)), FrozenMoves (frame I) moves ∧ MoveEquations (frame I) moves

Finite query semantics with literal zeros on every coordinate of every fixed segment.