Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.Computability.BitTree.Elias.Execution
public import Geb.Prototypes.Computability.BitTree.Elias.ScannerCorrect
public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas

set_option doc.verso true

Resource bounds for the Elias-length recognizer

Work space counts all visited cells, including blank cells and marked origins. The input tape is read-only and excluded from CSLib's work-space measure.

Main statements

computableInTimeAndSpace_validBool proves simultaneous quadratic time and linear space.
spaceUsed_le_of_headBound converts the four head intervals to a work-space bound.

Implementation notes

The machine consumes each input bit once. Binary countdowns sweep their entire fixed-width words, including leading zeros, between input reads. Length fields are kept in binary, so malformed inputs advertising enormous payloads still halt within the same polynomial bound.

Tags

Elias delta code, Turing machine, running time, work space

              @[expose] public sectionnamespace Geb.BitTree.Elias.Machineopen Turing MultiTapeTM

Four heads confined to the same interval visit at most four times its number of cells.

theorem spaceUsed_le_of_headBound {input : List (Fin 3)}
    (cfg : Cfg 4 (Fin 3) Control input) (width t : ℕ)
    (h : ∀ u ≤ t, HeadBound width (machine.configs cfg u)) :
    machine.spaceUsed cfg t ≤ 4 * (width + 1) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)⊢ spaceUsed cfg t ≤ 4 * (width + 1)
  have hsub (i : Fin 4) : machine.visitedByTapeHead cfg t i ⊆
      (Finset.range (width + 1)).image (fun n : ℕ ↦ (n : ℤ)) := by
    intro z hzinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4z:ℤhz:z ∈ visitedByTapeHead cfg t i⊢ z ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    obtain ⟨u, hu, rfl⟩ := machine.mem_visitedByTapeHead.mp hzinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t i⊢ (configs cfg u).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    obtain ⟨hlo, hhi⟩ := h u (byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t i⊢ u ≤ t omegaAll goals completed! 🐙) iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ (configs cfg u).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    apply Finset.mem_image.mprinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ ∃ a ∈ Finset.range (width + 1), ↑a = (configs cfg u).workTapePos i
    refine ⟨_, Finset.mem_range.mpr ?_, Int.toNat_of_nonneg hlo⟩input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 4u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ ((configs cfg u).workTapePos i).toNat < width + 1
    omegainput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 4), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))⊢ spaceUsed cfg t ≤ 4 * (width + 1)
  have hi (i : Fin 4) : machine.spaceUsedByTape cfg t i ≤ width + 1 :=
    (Finset.card_le_card (hsub i)).trans (Finset.card_image_le.trans (byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 4), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))i:Fin 4⊢ (Finset.range (width + 1)).card ≤ width + 1 simpAll goals completed! 🐙))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 4), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))hi:∀ (i : Fin 4), spaceUsedByTape cfg t i ≤ width + 1⊢ spaceUsed cfg t ≤ 4 * (width + 1)
  calc
    machine.spaceUsed cfg t ≤ ∑ _i : Fin 4, (width + 1) :=
      Finset.sum_le_sum (fun i _ ↦ hi i)
    _ = 4 * (width + 1) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 4), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))hi:∀ (i : Fin 4), spaceUsedByTape cfg t i ≤ width + 1⊢ ∑ _i, (width + 1) = 4 * (width + 1) simpAll goals completed! 🐙

After all input bits, one final transition halts.

theorem halts_at (w : List Bool) :
    (machine.configs (machine.initCfg (w.map boolEmb)) (1 + runCost w + 1)).state = none := byw:List Bool⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1)).state = none
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 1 + runCost (List.take w.length w);
have a := account (List.take w.length w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1)).state = none
  simp only [List.take_length] at hw:List Boolh:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
    modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = [] ∧
    ∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1)).state = none
  obtain ⟨hc, _, _⟩ := hw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1)).state = none
  rw [configs_succ_eq_step',w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w))).state = none hcw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (MultiTapeTM.step
      (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)).state =
  none]w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (MultiTapeTM.step
      (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)).state =
  none
  rw [step_end _ (account w).1.1 rfl (inputSymbol_end _ (byw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ↑(modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).inputPos =
  (List.map (⇑boolEmb) w).length + 1
    simp only [modelCfg, scanCfg, List.length_map]All goals completed! 🐙))]All goals completed! 🐙

The only output is the decision of the Elias tree decoder.

theorem outputString_eq (w : List Bool) :
    machine.outputString (machine.initCfg (w.map boolEmb)) (1 + runCost w + 1) =
      [boolEmb (Elias.validBool w)] := byw:List Bool⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1) = [boolEmb (validBool w)]
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 1 + runCost (List.take w.length w);
have a := account (List.take w.length w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1) = [boolEmb (validBool w)]
  simp only [List.take_length] at hw:List Boolh:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
    modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = [] ∧
    ∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1) = [boolEmb (validBool w)]
  obtain ⟨hc, ho, _⟩ := hw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1) = [boolEmb (validBool w)]
  rw [outputString_succ,w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) ++
    (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w))).toList =
  [boolEmb (validBool w)] ho,w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [] ++ (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w))).toList = [boolEmb (validBool w)] hc,w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [] ++
    (outputSymbol
        (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)).toList =
  [boolEmb (validBool w)]
    outputSymbol_end _ (account w).1.1 rfl (inputSymbol_end _ (byw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ↑(modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).inputPos =
  (List.map (⇑boolEmb) w).length + 1
      simp only [modelCfg, scanCfg, List.length_map]All goals completed! 🐙)), account_projectw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [] ++ (some (boolEmb (decide ((Scanner.scan w).1 = Scanner.Mode.done)))).toList = [boolEmb (validBool w)]]w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [] ++ (some (boolEmb (decide ((Scanner.scan w).1 = Scanner.Mode.done)))).toList = [boolEmb (validBool w)]
  change [boolEmb (Scanner.validBool w)] = _w:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [boolEmb (Scanner.validBool w)] = [boolEmb (validBool w)]
  rw [Scanner.validBool_eqw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []right✝:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ [boolEmb (validBool w)] = [boolEmb (validBool w)]]All goals completed! 🐙

The final halting transition preserves the work-head interval.

theorem headBound_run (w : List Bool) :
    ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1)
      (machine.configs (machine.initCfg (w.map boolEmb)) u) := byw:List Bool⊢ ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 1 + runCost (List.take w.length w);
have a := account (List.take w.length w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  simp only [List.take_length] at hw:List Boolh:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
    modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = [] ∧
    ∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  obtain ⟨hc, _, hh⟩ := hw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  intro u huw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  by_cases he : u ≤ 1 + runCost wposw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1he:u ≤ 1 + runCost w⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1he:¬u ≤ 1 + runCost w⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  ·posw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1he:u ≤ 1 + runCost w⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) exact hh u heAll goals completed! 🐙
  ·negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1he:¬u ≤ 1 + runCost w⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) have hu' : u = 1 + runCost w + 1 := byw:List Bool⊢ ∀ u ≤ 1 + runCost w + 1, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) omeganegw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 1 + runCost w + 1he:¬u ≤ 1 + runCost whu':u = 1 + runCost w + 1⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    subst unegw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost w⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1))
    have hlast := hh (1 + runCost w) (Nat.le_refl _)negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w))⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1))
    rw [hcnegw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1))] at hlastnegw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w + 1))
    rw [configs_succ_eq_step',negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ HeadBound (w.length + 1) (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w))) hc,negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ HeadBound (w.length + 1)
  (MultiTapeTM.step (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2))
      step_end _ (account w).1.1 rfl (inputSymbol_end _ (byw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ ↑(modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).inputPos =
  (List.map (⇑boolEmb) w).length + 1
        simp only [modelCfg, scanCfg, List.length_map]All goals completed! 🐙))]negw:List Boolhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) =
  modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost w) = []hh:∀ u ≤ 1 + runCost w, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:1 + runCost w + 1 ≤ 1 + runCost w + 1he:¬1 + runCost w + 1 ≤ 1 + runCost whlast:HeadBound (w.length + 1)
  (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2)⊢ HeadBound (w.length + 1)
  { state := none,
    inputPos :=
      (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).inputPos,
    workTapes :=
      (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).workTapes,
    workTapePos :=
      (modelCfg (List.map (⇑boolEmb) w) ⟨w.length + 1, ⋯⟩ (account w).1 (account w).2.1 (account w).2.2).workTapePos }
    exact hlastAll goals completed! 🐙

The one-pass Elias recognizer has simultaneous quadratic-time and linear-space bounds.

theorem computableInTimeAndSpace_validBool :
    ComputableInTimeAndSpace (fun w : List Bool ↦ [Elias.validBool w])
      (fun n ↦ 5 * n ^ 2 + 16 * n + 2) (fun n ↦ 4 * (n + 2)) := by⊢ ComputableInTimeAndSpace (fun w ↦ [validBool w]) (fun n ↦ 5 * n ^ 2 + 16 * n + 2) fun n ↦ 4 * (n + 2)
  refine ⟨4, 3, 25, boolEmb, machine, fun w ↦ ?_⟩w:List Bool⊢ ∃ t' ≤ (fun n ↦ 5 * n ^ 2 + 16 * n + 2) w.length,
  ∃ s' ≤ (fun n ↦ 4 * (n + 2)) w.length,
    machine.ComputesInTimeAndSpace (List.map (⇑boolEmb) w) (List.map (⇑boolEmb) ((fun w ↦ [validBool w]) w)) t' s'
  refine ⟨1 + runCost w + 1, ?_,
    machine.spaceUsed (machine.initCfg (w.map boolEmb)) (1 + runCost w + 1),
    spaceUsed_le_of_headBound _ _ _ (headBound_run w),
    halts_at w, outputString_eq w, rfl⟩w:List Bool⊢ 1 + runCost w + 1 ≤ (fun n ↦ 5 * n ^ 2 + 16 * n + 2) w.length
  change 1 + runCost w + 1 ≤ 5 * w.length ^ 2 + 16 * w.length + 2w:List Bool⊢ 1 + runCost w + 1 ≤ 5 * w.length ^ 2 + 16 * w.length + 2
  have h := runCost_le ww:List Boolh:runCost w ≤ 5 * w.length ^ 2 + 16 * w.length⊢ 1 + runCost w + 1 ≤ 5 * w.length ^ 2 + 16 * w.length + 2
  omegaAll goals completed! 🐙

end Geb.BitTree.Elias.Machine