Sketch of hierarchy theorem.

Cslib/Computability/Machines/RTM/HierarchyTheorems.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.RTM.TMSimulator
+public import Cslib.Computability.Machines.RTM.PB
+
+/-!
+# Hierarchy Theorems
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak2009], Chapter 4
+
+-/
+
+
+@[expose] public section
+
+namespace Turing
+
+namespace RoseTreeMachine
+
+
+variable {env : List Value} {α β : Type} [DataEncode α] [DataEncode β]
+
+/-- A TM normalized to use `Fin k` for its `State` and `Symbol` type. -/
+structure NormalizedTM where
+  states : ℕ
+  symbols : ℕ
+  toSingleTapeTM : SingleTapeTM (Fin (symbols + 2))
+  h_states : toSingleTapeTM.State = Fin (states + 1)
+
+def NormalizedTM.Cfg (tm : NormalizedTM) := tm.toSingleTapeTM.Cfg
+
+def NormalizedTM.step (tm : NormalizedTM) (cfg : tm.Cfg) : tm.Cfg :=
+  match tm.toSingleTapeTM.step cfg with
+  | none => cfg
+  | some cfg' => cfg'
+
+def binaryToFin {n : ℕ} (x : List Bool) : List (Fin (n + 2)) :=
+  List.map (fun b => if b then 1 else 0) x
+
+/-- If the TM `tm` is in the final state after at most `t` steps, returns the output.
+Note that this is a slightly different output notion since we do not require the tape to be in
+its canonical state. Also we just filter out any symbol that is not the encoding of a bool. -/
+def NormalizedTM.output? (tm : NormalizedTM) (input : List Bool) (t : ℕ) : Option (List Bool) :=
+  let cfg := tm.step^[t] (tm.toSingleTapeTM.initCfg (binaryToFin input))
+  if cfg.state = none then
+    (cfg.BiTape.head :: cfg.BiTape.right.toList).filterMap
+      (fun c => match c with | some 0 => some false | some 1 => some true | _ => none)
+  else
+    none
+
+def NormalizedTM.ComputesFunInTime (tm : NormalizedTM) (f : List Bool → List Bool) (t : ℕ → ℕ) :
+    Prop :=
+  ∀ input, ∃ t' < t input.length, tm.output? input t' = some (f input)
+
+def DSPACE (t : ℕ → ℕ) := { f : List Bool → Bool | ∃ tm : NormalizedTM, ∃ a,
+        tm.ComputesFunInTime (fun x => [f x]) fun n => a * t n + a }
+
+/-- An enumeration of Turing machines such that every TM appears infinitely often in the
+enumeration. -/
+def Enumerates (e : ℕ → NormalizedTM) : Prop := ∀ tm n, ∃ n' > n, e n' = tm
+
+-- /-- A universal machine for an enumeration can simulate any Turing machine from the enumeration
+-- with quadratic overhead.
+-- TODO: It is possible to have an overhead of `t log t`, but quadratic is fine for now. -/
+-- def UniversalMachineSemantics_old
+--     (allTMs : ℕ → NormalizedTM)
+--     (p : PB → PB) : Prop :=
+--   ∃ a, ∀ m input t, ∃ s, PB.ComputesEncInTimeAndSpace p
+--     (t, input, m)
+--     ((allTMs m).output? input t)
+--     ((a * (allTMs m).states * (allTMs m).symbols * t * t) + a)
+--     s
+
+def simulator (allTMs : ℕ → NormalizedTM) (m : ℕ) (input : List Bool) (t : ℕ) :
+    Option (List Bool) :=
+  (allTMs m).output? input t
+
+/-- A universal machine for an enumeration can simulate any Turing machine from the enumeration
+with quadratic overhead.
+TODO: It is possible to have an overhead of `t log t`, but quadratic is fine for now. -/
+def UniversalMachineSemantics
+    (allTMs : ℕ → NormalizedTM)
+    (p : PB → PB) : Prop :=
+  ∃ a, ∃ s, PB.ComputesFunEncInTimeAndSpace p
+    (fun (m, input, t) => simulator allTMs m input t)
+    (fun (m, _, t) =>
+      -- The runtime of the simulation has an overhead in the "size" of the TM, but does not
+      -- depend on the input.
+      (a * (allTMs m).states * (allTMs m).symbols * t * t) + a)
+    s
+
+def succ (x : PB) : PB := sorry
+
+def length (x : PB) : PB := sorry
+
+theorem length_computes {p : PB} {x : List α} (h_p : p.ComputesEnc env x) :
+  (length p).ComputesEnc env x.length := by
+  sorry
+
+/-- Computes `x * x` -/
+def mul (x y : PB) : PB := sorry
+
+theorem mul_computes {p q : PB} {x y : ℕ} (h_p : p.ComputesEnc env x) (h_q : q.ComputesEnc env y) :
+  (mul p q).ComputesEnc env (x * y) := by
+  sorry
+
+def cube (x : PB) : PB := mul (mul x x) x
+
+theorem cube_computes {p : PB} {x : ℕ} (h_p : p.ComputesEnc env x) :
+  (cube p).ComputesEnc env (x * x * x) := by
+  exact mul_computes (mul_computes h_p h_p) h_p
+
+/-- Run the universal machine on (x, x, |x|^3) and invert its output, if it halts. -/
+def diagonalizer (p : PB → PB) (x : PB) : PB :=
+  let output := p (PB.toPair x (PB.toPair x (cube (length x))))
+  PB.ifEq output (PB.constantEnc (Option.some [true]))
+      (PB.constantEnc [false])
+      (PB.constantEnc [true])
+
+/-- Semantic core of the diagonalizer (resources ignored): if the inner universal-machine call
+outputs `some [b]`, the diagonalizer outputs the inverted bit `[!b]`. This isolates the inversion
+logic from the resource bound and from the `log`/`mul`/`cube` stubs. -/
+theorem diagonalizer_inverts
+    {p_u : PB → PB}
+    {f_u : ℕ × List Bool × ℕ → List Bool}
+    {h_u : PB.ComputesFunEnc p_u f_u}
+    {p_in : PB}
+    {x : ℕ}
+    {h_in : p_in.ComputesEnc env x} :
+    (diagonalizer p_u p_in).ComputesEnc env [!(f_u (x, Nat.bits x, x * x * x) = [true])] :=
+  match f_u (x, Nat.bits x, x * x * x) with
+  | [true] => by
+    refine PB.ifeq_eq_computes ?_ PB.constantEnc_computesEnc PB.constantEnc_computesEnc
+    sorry
+  | _ => by
+    -- refine PB.ifeq_ne_computes ?_ PB.constantEnc_computesEnc ?_ ?_
+    sorry
+
+theorem hierarchy
+    (enum : ℕ → NormalizedTM)
+    (h_enum : Enumerates enum)
+    (h_exists_univ : ∃ p, UniversalMachineSemantics enum p) :
+    DSPACE id ≠ DSPACE (fun n => n^5) := by
+  obtain ⟨h, h_u⟩ := h_exists_univ
+  let diag := fun x : List Bool =>
+    let n := Nat.ofBits x.get
+    simulator enum n x (n * n * n) != some [true]
+  let m := diagonalizer h
+  -- TODO m computes diagm in a certain time, therfore it is in DSPACE (fun n => n^5)
+  have h_diag_in_quint : diag ∈ DSPACE (fun n => n^5) := by
+     sorry
+  have h_notin_linear : diag ∉ DSPACE id := by
+    intro h_linear
+    obtain ⟨tm, a, h_tm⟩ := h_linear
+
+    sorry
+  intro h_eq
+  simp_all
+
+end RoseTreeMachine
+
+end Turing

Cslib/Computability/Machines/RTM/PB.lean

@@ -78,6 +78,27 @@ def app (f a : PB) : PB := fun n => .app (f n) (a n)
 /-- Close a builder into a concrete `Prog`. -/
 def build (p : PB) : Prog := p 0
 
+/-- A proof that a `PB` that takes another `PB` as input computes a certain value.
+This is mainly used for final results. During composition, `computesFun₁` is more useful
+since it allows capturing the environment. -/
+def ComputesFunInTimeAndSpace (p : PB → PB) (input output : Data) (t s : ℕ) : Prop :=
+  ∀ env, ProgSem (env ++ [.data input]) (p (PB.var env.length) (env.length + 1))
+    (.data output) t s
+
+/-- The `PB → PB` analogue of `Prog.ComputesInTimeAndSpace`: viewing `p` as a transformation from
+an argument builder to a result builder, `p` computes `output` from `input` using `t` time and `s`
+space. The input is supplied as the last entry of the environment and read back through a variable,
+and the `∀ env` makes the statement hold under any outer environment (so it can be plugged into a
+larger program). -/
+def ComputesInTimeAndSpace (p : PB → PB) (input output : Data) (t s : ℕ) : Prop :=
+  ∀ env, ProgSem (env ++ [.data input]) (p (PB.var env.length) (env.length + 1))
+    (.data output) t s
+
+/-- Encoded form of `ComputesInTimeAndSpace`: `p` maps a value encoding `input : α` to one encoding
+`output : β`, using `t` time and `s` space. -/
+def ComputesEncInTimeAndSpace {α β : Type} [DataEncode α] [DataEncode β]
+    (p : PB → PB) (input : α) (output : β) (t s : ℕ) : Prop :=
+  ComputesInTimeAndSpace p (DataEncode.encode input) (DataEncode.encode output) t s
 
 variable {env : List Value}
 
@@ -114,6 +135,42 @@ This allows statements that `PB`s compute functions on lean datatypes. -/
 def ComputesEnc {α : Type} [DataEncode α] (env : List Value) (impl : PB) (x : α) :=
   Computes env impl (.data (DataEncode.encode x))
 
+/-- A `PB → PB` transformation `p` computes the (mathematical) function `φ`. Stated parametrically
+over the *argument builder* `a` together with a hypothesis that `a` computes the input: this is the
+shape of all the `_computes` lemmas (e.g. `tmMainLoop_computes`, `bitapeLeft_computes`), and it is
+what makes them composable. Resource-erased; for resource bounds see `ComputesInTimeAndSpace`. -/
+def ComputesFunEnc {α β : Type} [DataEncode α] [DataEncode β]
+    (p : PB → PB) (φ : α → β) : Prop :=
+  ∀ (env : List Value) (a : PB) (x : α), a.ComputesEnc env x → (p a).ComputesEnc env (φ x)
+
+/-- Composition of `PB → PB` transformations is function composition of the computed functions.
+This is the formal statement of the implicit composition used throughout `TMSimulator`. -/
+theorem ComputesFunEnc.comp {α β γ : Type} [DataEncode α] [DataEncode β] [DataEncode γ]
+    {p q : PB → PB} {φ : α → β} {ψ : β → γ}
+    (hp : ComputesFunEnc p φ) (hq : ComputesFunEnc q ψ) :
+    ComputesFunEnc (fun a => q (p a)) (ψ ∘ φ) :=
+  fun env a x h => hq env (p a) (φ x) (hp env a x h)
+
+/-- The identity transformation computes the identity function. -/
+theorem ComputesFunEnc.id {α : Type} [DataEncode α] :
+    ComputesFunEnc (α := α) (fun a => a) id :=
+  fun _ _ _ h => h
+
+/-- Resource-tracked analogue of `ComputesFunEnc`: `p` computes `φ`, charging its own time `t x`
+and space `s x` *on top of* the argument's cost. The costs are functions of the (decoded) input, so
+the bound can scale with the actual argument (e.g. with the simulated machine and step count). Given
+any argument builder `a` that computes `x` in time `ta` and space `sa`, the result builder `p a`
+computes `φ x` in time `t x + ta` and space `max (s x) sa`. Threading the argument cost this way is
+what makes the bounds additive under composition. -/
+def ComputesFunEncInTimeAndSpace {α β : Type} [DataEncode α] [DataEncode β]
+    (p : PB → PB) (φ : α → β) (t s : α → ℕ) : Prop :=
+  ∀ (env : List Value) (a : PB) (x : α) (ta sa : ℕ),
+    (∀ ext : List Value, ProgSem (env ++ ext) (a (env.length + ext.length))
+      (.data (DataEncode.encode x)) ta sa) →
+    (∀ ext : List Value, ProgSem (env ++ ext) (p a (env.length + ext.length))
+      (.data (DataEncode.encode (φ x))) (t x + ta) (max (s x) sa))
+
+
 /-- Var-lookup: `PB.var i` reads the `i`-th entry of the environment. -/
 @[simp]
 lemma var_computes {i : ℕ} (h : i < env.length) :

Cslib/Computability/Machines/RTM/Prog.lean

@@ -225,6 +225,10 @@ inductive InPlace : Prog → Prop
       accumulator. -/
   | while_ (hinit : InPlace init) (hbody : InPlace body) :
       InPlace (.while_ init (.fn body))
+  /-- `app` whose operator is a literal one-argument function `fn body` (a `let` binding):
+      the abstraction is created and immediately consumed, so no closure escapes. -/
+  | app (hbody : InPlace body) (harg : InPlace arg) :
+      InPlace (.app (.fn body) arg)
 
 
 end RoseTreeMachine

Cslib/Computability/Machines/RTM/Tools.lean

@@ -265,6 +265,7 @@ lemma listHeadOption_computes {p : PB} {l : List α} (h : p.ComputesEnc env l) :
     apply PB.elim_cons_computes h (PB.computesFun₂_branch2 (fun ext => ?_))
     refine PB.cons_computes (var_computes_fresh ext _) empty_computes
 
+
 -- Evaluate a function `f` at `arg` where the function is given as a graph (list of pairs).
 -- Returns `some y` for the first `x` in the graph such that `f x = y` and `none` otherwise.
 def evalFunGraph (graph : PB) (arg : PB) : PB :=
@@ -402,6 +403,37 @@ lemma evalFunGraph_Computes_of_fun
   apply PB.head_computes h
 
 
+def bitEq (x y : PB) : PB :=
+  ifEq x y (constantEnc true) (constantEnc false)
+
+def bitNot (x : PB) : PB :=
+  ifEq x (constantEnc true) (constantEnc false) (constantEnc true)
+
+def bitXor (x y : PB) : PB :=
+  ifEq x y (constantEnc false) (constantEnc true)
+
+def succ (x : PB) : PB :=
+  let loop_result := foldl
+    (fun st bit =>
+      let carry := st.fst
+      let acc := st.snd
+      let new_carry := PB.ifEq carry (constantEnc true)
+        (PB.ifEq bit (constantEnc true) (constantEnc true) (constantEnc false))
+        (constantEnc false)
+      let new_bit := PB.ifEq carry (constantEnc true)
+        (PB.ifEq bit (constantEnc true) (constantEnc false) (constantEnc true))
+        bit
+      toPair new_carry (cons new_bit acc))
+    (toPair (constantEnc true) empty)
+    x
+  let final_carry := loop_result.fst
+  let result_rev := loop_result.snd
+  -- If final carry, prepend 1; otherwise just reverse back
+  reverse (PB.ifEq final_carry (constantEnc true)
+    (cons (constantEnc true) result_rev)
+    result_rev)
+
+
 end PB
 
 end RoseTreeMachine

references.bib

@@ -30,6 +30,15 @@ @article{AngluinLaird1988
   doi          = {10.1007/BF00116829}
 }
 
+@book{AroraBarak2009,
+  title={Computational Complexity: A Modern Approach},
+  author={Arora, Sanjeev and Barak, Boaz},
+  year={2009},
+  publisher={Cambridge University Press},
+  address={New York, NY, USA},
+  isbn={978-0-521-42426-4}
+}
+
 @book{Baader1998,
 author = {Baader, Franz and Nipkow, Tobias},
 title = {Term rewriting and all that},