Correctness and state cost of the binary liveness scanner

Descending column order lets a countdown retain the selected target vertex. The codeword transition relation is exactly the relation being encoded. The arbitrary-word-encoding lower bound then applies with no state loss.

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_seek_bits (n : ℕ) (i : Fin (n + 1)) (bits : List Bool) : (machine n).evalFrom {State.seek i} (List.map Letter.bit bits) = {State.seek i}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_carry_bits (n : ℕ) (i : Fin (n + 1)) (bits : List Bool) : (machine n).evalFrom {State.carry i} (List.map Letter.bit bits) = {State.carry i}

theorem Complexity.FiniteAutomaton.BinaryLiveness.columnWord_succ (bits : ℕ → Bool) (k : ℕ) : columnWord bits (k + 1) = Letter.bit (bits k) :: columnWord bits k

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_empty (n : ℕ) (w : List Letter) : (machine n).evalFrom ∅ w = ∅

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_scan_columns (n k : ℕ) (hk : k ≤ n) (bits : ℕ → Bool) : (machine n).evalFrom {State.scan ⟨k, ⋯⟩} (columnWord bits (k + 1)) = {q : State n | ∃ (j : Fin (n + 1)), q = State.carry j ∧ ↑j ≤ k ∧ bits ↑j = true}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_seek_row (n : ℕ) (i : Fin (n + 1)) (bits : ℕ → Bool) : (machine n).evalFrom {State.seek i} (rowWord n bits) = if _hi : ↑i = 0 then {q : State n | ∃ (j : Fin (n + 1)), q = State.carry j ∧ bits ↑j = true} else {State.seek ⟨↑i - 1, ⋯⟩}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_carry_row (n : ℕ) (i : Fin (n + 1)) (bits : ℕ → Bool) : (machine n).evalFrom {State.carry i} (rowWord n bits) = {State.carry i}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_carry_rows_stop (n : ℕ) (i : Fin (n + 1)) (rows : List (ℕ → Bool)) : (machine n).evalFrom {State.carry i} (List.flatMap (rowWord n) rows ++ [Letter.stop]) = {State.seek i}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_row_selection (n : ℕ) (bits : ℕ → Bool) (rows : List (ℕ → Bool)) : (machine n).evalFrom {q : State n | ∃ (j : Fin (n + 1)), q = State.carry j ∧ bits ↑j = true} (List.flatMap (rowWord n) rows ++ [Letter.stop]) = {q : State n | ∃ (j : Fin (n + 1)), q = State.seek j ∧ bits ↑j = true}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_seek_rows_stop (n : ℕ) (i : Fin (n + 1)) (rows : List (ℕ → Bool)) : (machine n).evalFrom {State.seek i} (List.flatMap (rowWord n) rows ++ [Letter.stop]) = {q : State n | ∃ (j : Fin (n + 1)), q = State.seek j ∧ rowAt rows ↑i ↑j = true}

theorem Complexity.FiniteAutomaton.BinaryLiveness.rowAt_relationRows {n : ℕ} (R : BRel (Fin (n + 1))) (i j : Fin (n + 1)) : rowAt (relationRows R) ↑i ↑j = true ↔ R.holds i j

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_seek_code {n : ℕ} (R : BRel (Fin (n + 1))) (i : Fin (n + 1)) : (machine n).evalFrom {State.seek i} (code R) = {q : State n | ∃ (j : Fin (n + 1)), q = State.seek j ∧ R.holds i j}

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_image_code {n : ℕ} (R : BRel (Fin (n + 1))) (S : Set (Fin (n + 1))) : (machine n).evalFrom (State.seek '' S) (code R) = State.seek '' (livenessNFA (n + 1)).stepSet S R

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_encode {n : ℕ} (w : List (BRel (Fin (n + 1)))) (S : Set (Fin (n + 1))) : (machine n).evalFrom (State.seek '' S) (List.flatMap code w) = State.seek '' (livenessNFA (n + 1)).evalFrom S w

theorem Complexity.FiniteAutomaton.BinaryLiveness.machine_accepts_code {n : ℕ} (w : List (BRel (Fin (n + 1)))) : List.flatMap code w ∈ (machine n).accepts ↔ w ∈ oneWayLiveness (n + 1)

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_binary_letter {Q : Type} (M : NFA Letter Q) (q : Q) (a : Letter) : (binaryMachine M).evalFrom {(q, none)} (letterBits a) = boundary (M.step q a)

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_binary_boundary_letter {Q : Type} (M : NFA Letter Q) (S : Set Q) (a : Letter) : (binaryMachine M).evalFrom (boundary S) (letterBits a) = boundary (M.stepSet S a)

theorem Complexity.FiniteAutomaton.BinaryLiveness.evalFrom_binary_encode {Q : Type} (M : NFA Letter Q) (S : Set Q) (w : List Letter) : (binaryMachine M).evalFrom (boundary S) (List.flatMap letterBits w) = boundary (M.evalFrom S w)

theorem Complexity.FiniteAutomaton.BinaryLiveness.binaryMachine_accepts_encode {Q : Type} (M : NFA Letter Q) (w : List Letter) : List.flatMap letterBits w ∈ (binaryMachine M).accepts ↔ w ∈ M.accepts

theorem Complexity.FiniteAutomaton.BinaryLiveness.binary_liveness_accepts_code {n : ℕ} (w : List (BRel (Fin (n + 1)))) : List.flatMap binaryCode w ∈ (binaryMachine (machine n)).accepts ↔ w ∈ oneWayLiveness (n + 1)

theorem Complexity.FiniteAutomaton.BinaryLiveness.card_binary_state (n : ℕ) : Fintype.card (State n × Option Bool) = 9 * (n + 1)

theorem Complexity.FiniteAutomaton.BinaryLiveness.binary_state_lower_bound (n : ℕ) (positive : Bool) (s : ℕ) (D : DMachine Bool s) (hD : D.Recognizes positive (binaryMachine (machine (n + 1))).accepts) : 2 ^ (n / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2