Correctness of the DFA input guard

The scan takes one step per input bit. On acceptance, returning to the start takes another input-length plus two steps. Rejection halts with empty output.

theorem Complexity.MathlibTM0.BinaryMachine.run_add (M : BinaryMachine) (t u : ℕ) (c : M.Config) : M.run (t + u) c = (M.run t c).bind (M.run u)

Consecutive source runs compose by option bind.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.step_scan_bit (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (q : σ) (T : Turing.Tape M.Alphabet) (b : Bool) (h : M.readBit T.head = some b) : (M.guarded D).step { q := GuardState.scan q, Tape := T } = some { q := GuardState.scan (D.step q b), Tape := Turing.Tape.move Turing.Dir.right T }

Reading a bit advances the DFA and moves right.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.move_right (M : BinaryMachine) (L R : List M.Alphabet) (a : M.Alphabet) : Turing.Tape.move Turing.Dir.right (Turing.Tape.mk₂ L (a :: R)) = Turing.Tape.mk₂ (a :: L) R

Moving right consumes the next explicit tape cell.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.move_left (M : BinaryMachine) (L R : List M.Alphabet) (a : M.Alphabet) : Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ (a :: L) R) = Turing.Tape.mk₂ L (a :: R)

Moving left exposes the nearest cell on the left.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.scan (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (w : List Bool) (L : List M.Alphabet) (q : σ) : (M.guarded D).run w.length { q := GuardState.scan q, Tape := Turing.Tape.mk₂ L (List.map M.bit w) } = some { q := GuardState.scan (D.evalFrom q w), Tape := Turing.Tape.mk₂ ((List.map M.bit w).reverse ++ L) [] }

The guard scans an explicit binary suffix without changing the tape.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.rewind (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (w : List Bool) (R : List M.Alphabet) : (M.guarded D).run (w.length + 1) { q := GuardState.rewind, Tape := Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ (List.map M.bit w) R) } = some { q := GuardState.run default, Tape := Turing.Tape.mk₂ [] ((List.map M.bit w).reverse ++ R) }

Rewinding crosses the input once and returns from the preceding blank.

def Complexity.MathlibTM0.BinaryMachine.Guard.liftCfg (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (c : M.Config) : (M.guarded D).Config

Tag a source configuration with the execution phase.

Equations

• Complexity.MathlibTM0.BinaryMachine.Guard.liftCfg M D c = { q := Complexity.MathlibTM0.BinaryMachine.GuardState.run c.q, Tape := c.Tape }

theorem Complexity.MathlibTM0.BinaryMachine.Guard.step_lift (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (c : M.Config) : (M.guarded D).step (liftCfg M D c) = Option.map (liftCfg M D) (M.step c)

The execution phase preserves one source transition.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.run_lift (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) (t : ℕ) (c : M.Config) : (M.guarded D).run t (liftCfg M D c) = Option.map (liftCfg M D) (M.run t c)

The execution phase preserves any finite source run.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.prepare (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) {w : List Bool} (hw : w ∈ D.accepts) : (M.guarded D).run (2 * w.length + 2) { q := GuardState.scan D.start, Tape := Turing.Tape.mk₁ (List.map M.bit w) } = some (liftCfg M D (Turing.TM0.init (List.map M.bit w)))

An accepted input is restored at the source's initial state in linear time.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.accepted (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) {w output : List Bool} {time : ℕ} (hw : w ∈ D.accepts) (h : M.OutputsWithin w output time) : (M.guarded D).OutputsWithin w output (2 * w.length + time + 2)

A valid input incurs just the scan-and-rewind overhead.

theorem Complexity.MathlibTM0.BinaryMachine.Guard.rejected (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) {w : List Bool} (hw : w ∉ D.accepts) : (M.guarded D).OutputsWithin w [] w.length

A rejected input halts at the first blank with empty output.