diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean
index 7bd2abd6..b725c85d 100644
--- a/Complexitylib/Models.lean
+++ b/Complexitylib/Models.lean
@@ -56,6 +56,10 @@ import Complexitylib.Models.TuringMachine.UTM.ClockedUtm
 import Complexitylib.Models.TuringMachine.UTM.HierarchySupport
 import Complexitylib.Models.TuringMachine.UTM.Diagonal
 import Complexitylib.Models.RandomAccessMachine
+import Complexitylib.Models.RoseTreeMachine.Data
+import Complexitylib.Models.RoseTreeMachine.DataEncode
+import Complexitylib.Models.RoseTreeMachine.Prog
+import Complexitylib.Models.RoseTreeMachine.Compile
 
 /-!
 # Computation models
diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean
new file mode 100644
index 00000000..b361ae1c
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+import Complexitylib.Models.RoseTreeMachine.Compile.Defs
+import Complexitylib.Models.RoseTreeMachine.Compile.Internal
+
+/-!
+# Compiling in-place rose tree machine programs to Turing machines
+
+This is the **surface** of the RTM → TM compiler: it states the single public
+theorem `inPlace_compilesToTM`. The human-auditable contract it establishes
+(`SubroutineLayout` / `Prog.RunsAsSubroutine`) lives in
+`Complexitylib.Models.RoseTreeMachine.Compile.Defs`, and all proof machinery
+lives in `Complexitylib.Models.RoseTreeMachine.Compile.Internal`.
+
+## Main result
+
+- `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem**:
+  every `InPlace` program of arity `m` compiles to a reusable tape-indexed
+  subroutine (`Prog.RunsAsSubroutine m`). The caller runs it at tape indices of
+  their choosing (a `SubroutineLayout`); inputs live on the chosen argument work
+  tapes (not the dedicated input tape) as their `Data.toBits` serialization; the
+  machine halts with `HasOutput result.toBits` on the result tape, leaves every
+  other tape exactly as it started, and matches the RTM time/space bounds up to
+  a constant. Because the encoding is `Data.toBits`, `Data.toBits_length` makes
+  the space charge coincide exactly with the RTM `Data.size` measure.
+
+## Scope
+
+This is the first verified slice of the `InPlace`-RTM → TM compiler. The
+compiler recursion `Compile.Internal.compilesUnder_of_inPlace` is fully
+decomposed into per-constructor parts and `inPlace_compilesToTM` is wired to it;
+of those parts, `compiled_empty` is proven and each remaining part is stated but
+still `sorry` (it needs concrete `Data`-manipulation subroutines over the tape
+serialization, tracked in `ROADMAP.md`, track N0). The final theorem below
+therefore transitively depends on `sorry`, so `lake build --wfail` and the axiom
+guard will report it until the parts are proved.
+-/
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+/-- **The full in-place RTM → Turing-machine compiler theorem.** Every
+first-order (`InPlace`) rose tree machine program compiles, at any argument
+arity `m`, to a reusable tape-indexed Turing-machine subroutine
+(`Prog.RunsAsSubroutine`): the caller runs it at tape indices of their choosing,
+inputs are serialized via `Data.toBits`, and time/space match the RTM `ProgSem`
+bounds up to a constant. See `Prog.RunsAsSubroutine` for the precise contract.
+
+The base case `empty` is discharged by `Compile.Internal.compiled_empty`; the
+remaining constructors are tracked in `ROADMAP.md`, track N0. The statement is
+provided now so the subroutine interface is fixed; the proof is deferred. -/
+theorem inPlace_compilesToTM {m : ℕ} (p : Prog) (hp : InPlace p) :
+    p.RunsAsSubroutine m :=
+  compilesUnder_of_inPlace p hp
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean
new file mode 100644
index 00000000..fa7d39fe
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+import Complexitylib.Models.RoseTreeMachine.Prog
+import Complexitylib.Models.TuringMachine.Hoare.Space.Defs
+import Complexitylib.Models.TuringMachine.Registers
+
+/-!
+# Compiling in-place rose tree machine programs to Turing machines — contract
+
+This module holds the **human-auditable contract** the RTM → TM compiler
+establishes: the caller-chosen tape layout and the public subroutine
+specification. The proof machinery that discharges the contract lives in
+`Complexitylib.Models.RoseTreeMachine.Compile.Internal`, and the final theorem
+`inPlace_compilesToTM` lives in `Complexitylib.Models.RoseTreeMachine.Compile`.
+
+## What "match" means here
+
+The RTM cost model is faithful to Turing machines only *up to a constant
+factor* — the standard notion for cross-model simulation. A compiled machine
+computes the *same* binary function as the source program and its time (resp.
+space) bound is *dominated by* the program's RTM time (resp. space) bound.
+
+Two structural facts make this achievable for the `InPlace` fragment:
+
+- **Result materialization is already paid for.** `ProgSem.size_le` shows every
+  derivation charges at least the size of the value it produces, in both time
+  and space, so the O(size) traversal/assembly/copy work a Turing machine must
+  perform to build a `Data` result is always absorbed (up to a constant).
+- **Space is charged generously.** Most `ProgSem` rules *add* the space of
+  sequential sub-computations (`s₁ + s₂ + …`) where a Turing machine reuses
+  space and pays only their `max`, so the RTM figure is a valid upper bound.
+
+## Main definitions
+
+- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout: a single
+  injective `place` map assigning each slot (an argument, the result, or a
+  scratch tape) a distinct physical tape in the caller's bank. Role accessors
+  `argIdx`/`resIdx`/`scratchIdx` and their pairwise-distinctness follow from
+  injectivity of `place`.
+- `RoseTreeMachine.Prog.RunsAsSubroutine` — the **public subroutine contract**:
+  the compiled machine, run from a `SubroutineLayout.Loaded` start, halts with
+  the result on the result tape, frames every other tape (arguments preserved,
+  scratch restored blank), and matches the RTM time/space bounds up to a
+  constant. This is what `inPlace_compilesToTM` establishes.
+-/
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+open Complexity.TM
+
+/-- The tapes a subroutine occupies, indexed uniformly by role: `m` argument
+slots, one result slot, and `sc` scratch slots. A `SubroutineLayout` maps this
+slot space injectively into the caller's tape bank. -/
+abbrev SubroutineSlot (m sc : ℕ) := Fin m ⊕ Unit ⊕ Fin sc
+
+/-- **A caller-chosen tape layout** for running an `m`-argument in-place RTM
+program as a subroutine on a `Fin k` tape bank using `sc` scratch tapes. As with
+the binary-arithmetic subroutines, the caller picks the tapes; a single
+injective `place` assigns each slot (argument, result, or scratch) a distinct
+physical tape, so the machine can treat them as independent registers. -/
+structure SubroutineLayout (m sc k : ℕ) where
+  /-- The physical tape each slot occupies. -/
+  place : SubroutineSlot m sc → Fin k
+  /-- Distinct slots occupy distinct tapes. -/
+  place_inj : Function.Injective place
+
+namespace SubroutineLayout
+
+variable {m sc k : ℕ} (L : SubroutineLayout m sc k)
+
+/-- The tape variable `j` is read from. -/
+def argIdx (j : Fin m) : Fin k := L.place (.inl j)
+
+/-- The tape the result is written to. -/
+def resIdx : Fin k := L.place (.inr (.inl ()))
+
+/-- The `l`-th auxiliary tape the machine may use. -/
+def scratchIdx (l : Fin sc) : Fin k := L.place (.inr (.inr l))
+
+/-- Distinct variables use distinct tapes. -/
+theorem argIdx_inj : Function.Injective L.argIdx := fun _ _ h =>
+  Sum.inl_injective (L.place_inj h)
+
+/-- Distinct scratch slots use distinct tapes. -/
+theorem scratchIdx_inj : Function.Injective L.scratchIdx := fun _ _ h =>
+  Sum.inr_injective (Sum.inr_injective (L.place_inj h))
+
+/-- No argument tape coincides with the result tape. -/
+theorem arg_ne_res (j : Fin m) : L.argIdx j ≠ L.resIdx := fun h => by
+  simpa using L.place_inj h
+
+/-- No scratch tape coincides with the result tape. -/
+theorem scratch_ne_res (l : Fin sc) : L.scratchIdx l ≠ L.resIdx := fun h => by
+  simpa using L.place_inj h
+
+/-- Argument tapes and scratch tapes are disjoint. -/
+theorem arg_ne_scratch (j : Fin m) (l : Fin sc) : L.argIdx j ≠ L.scratchIdx l :=
+  fun h => by simpa using L.place_inj h
+
+/-- The starting tape assignment expected by a `SubroutineLayout`: environment
+entry `j` sits on its argument tape as the balanced-parenthesis serialization
+`Data.toBits`, and the result and scratch tapes start blank. Every layout tape
+is **parked** (head at cell 1, just past the `▷` marker): a parked head is
+fixed by `idleDir`, so tapes the machine does not touch stay literally
+unchanged, and the convention matches the binary-arithmetic subroutines
+(e.g. `clearWorkTM`). Tapes outside the layout carry no prescribed contents, but
+they too must be **parked at head 1** (`Parked ∧ head ≤ 1`): parkedness makes the
+machine leave them literally unchanged (a head resting past a stray `▷` could be
+mutated across an idle step), and the head-1 bound keeps them inside the `b·s+b`
+auxiliary-space budget from the very first configuration. Every layout tape
+already sits at head 1, so this constrains only the caller's spare tapes. This
+makes the "every non-result tape is preserved" frame in `RunsAsSubroutine` hold
+for the whole bank, not just the layout tapes. -/
+def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop :=
+  (∀ j, work (L.argIdx j) =
+      (Tape.init ((env j).toBits.map Γ.ofBool)).move Dir3.right) ∧
+  work L.resIdx = (Tape.init []).move Dir3.right ∧
+  (∀ l, work (L.scratchIdx l) = (Tape.init []).move Dir3.right) ∧
+  (∀ i, Parked (work i) ∧ (work i).head ≤ 1)
+
+end SubroutineLayout
+
+/-- **The public subroutine contract.** `p.RunsAsSubroutine m` says the
+`m`-argument in-place program `p` compiles to a reusable Turing-machine
+subroutine: there is a scratch-tape count `sc` and constants `a`, `b`
+(depending only on `p`), so that for *any* caller layout `L : SubroutineLayout
+m sc k` there is a machine `M : TM k` that, whenever `p` maps `env` to `result`
+in RTM time `t` and space `s`, run from a `Loaded` start
+
+* halts within `a·t + a` steps with `result.toBits` on the result tape
+  (`HasOutput`),
+* leaves **every other tape exactly as it started** (`∀ i ≠ resIdx`): arguments
+  preserved read-only, scratch restored blank, untouched tapes untouched, and
+* keeps all work heads within `b·s + b` auxiliary space.
+
+The dedicated input and output tapes are not used by the compiler: the caller
+supplies them **parked** (`Parked inp₀`, `Parked out₀`) so the machine leaves
+them literally unchanged (`inp = inp₀ ∧ out = out₀`), and the input head starts
+at cell 1 (`inp₀.head ≤ 1`) so it fits the `0 + space + 1` input allowance.
+
+Inputs live on the chosen argument work tapes, *not* the dedicated input tape,
+so the space charge is over `Data.toBits`; by `Data.toBits_length` it matches
+the RTM `Data.size` measure up to `b`. Exposing `sc` tells the caller how many
+auxiliary tapes to reserve, and the "only the result tape changes" frame makes
+`M` freely composable. -/
+def Prog.RunsAsSubroutine (p : Prog) (m : ℕ) : Prop :=
+  ∃ sc a b : ℕ, ∀ {k : ℕ} (L : SubroutineLayout m sc k),
+    ∃ M : TM k, ∀ (env : Fin m → Data) (result : Data) (t s : ℕ)
+      (work₀ : Fin k → Tape) (inp₀ out₀ : Tape),
+      ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s →
+      L.Loaded env work₀ →
+      Parked inp₀ → inp₀.head ≤ 1 → Parked out₀ →
+      M.HoareTimeSpace
+        (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
+        (fun inp work out => inp = inp₀ ∧ out = out₀ ∧
+          (work L.resIdx).HasOutput result.toBits ∧
+          (∀ i, i ≠ L.resIdx → work i = work₀ i))
+        (a * t + a) 0 (b * s + b)
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean
new file mode 100644
index 00000000..6eb42750
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean
@@ -0,0 +1,315 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+import Complexitylib.Models.RoseTreeMachine.Compile.Defs
+import Complexitylib.Models.RoseTreeMachine.Compile.Internal.EmptyTM
+import Complexitylib.Models.TuringMachine.Subroutines.CopyWorkOutput
+
+/-!
+# Compiling in-place rose tree machine programs to Turing machines — internals
+
+This module holds the **proof machinery** for the RTM → TM compiler: the
+per-constructor compiler parts and the structural recursion
+`compilesUnder_of_inPlace` that assembles them into the public subroutine
+contract `Prog.RunsAsSubroutine`. Correctness is established by the type checker;
+the human-auditable contract it discharges lives in
+`Complexitylib.Models.RoseTreeMachine.Compile.Defs`, and the final theorem
+`inPlace_compilesToTM` in `Complexitylib.Models.RoseTreeMachine.Compile`.
+
+## Contents
+
+- `RoseTreeMachine.Compiled` — a thin alias for `Prog.RunsAsSubroutine`, the
+  shared codomain of the compiler recursion and the per-constructor parts.
+- `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`,
+  `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the
+  **individual compiler parts**, one per `InPlace` constructor. `compiled_empty`
+  and `compiled_var` are proven: `compiled_empty` reuses `TM.emptyTM` (the
+  parked-tape layout subroutine that materializes the empty node's serialization
+  `[false, true]`), and `compiled_var` copies argument tape `i` to the result
+  tape via `TM.copyWorkToWorkTM` then restores it with `TM.rewindWorkTM` (falling
+  back to `TM.emptyTM` when `i ≥ m`). Each remaining part is stated but still
+  `sorry`: it needs concrete `Data`-manipulation subroutines over the tape
+  serialization, tracked as future work in `ROADMAP.md` (track N0).
+- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every
+  `InPlace` program compiles, for any argument arity, to a subroutine satisfying
+  `Prog.RunsAsSubroutine`. The assembly is complete (no `sorry`); it dispatches
+  each program constructor to its individual part.
+
+> Note: the `compiled_*` parts other than `compiled_empty` and `compiled_var`
+> use `sorry` (and `compilesUnder_of_inPlace` depends on them), so
+> `lake build --wfail` and the axiom guard will report them until the parts are
+> proved.
+-/
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+open Complexity.TM
+
+/-- `Compiled m p`: the first-order program `p` compiles, for argument arity
+`m`, to a reusable tape-indexed Turing-machine subroutine. This is a thin alias
+for the public contract `Prog.RunsAsSubroutine`; it names the shared codomain of
+the compiler recursion `compilesUnder_of_inPlace` and the per-constructor
+building blocks below. -/
+def Compiled (m : ℕ) (p : Prog) : Prop := p.RunsAsSubroutine m
+
+/-- **Compiler part — `empty`.** The empty constructor compiles to `TM.emptyTM`,
+the parked-tape layout subroutine that clears the result tape and writes the
+empty node's serialization `[false, true] = (Data.l []).toBits` onto it, leaving
+every other tape literally unchanged. `ProgSem.empty` fixes the RTM cost at
+`t = s = 2`, so the machine's constant time and additive space fit the
+`a·t + a` / `b·s + b` budget with `a = clearWorkTimeBound 0 + 3` and `b = a + 1`. -/
+theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by
+  refine ⟨0, clearWorkTimeBound 0 + 1 + 2, 1 + (clearWorkTimeBound 0 + 1 + 2), ?_⟩
+  intro k L
+  refine ⟨emptyTM L.resIdx, ?_⟩
+  intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP
+  obtain ⟨_, hres, _, hpark⟩ := hloaded
+  cases hsem
+  have htarget :
+      work₀ L.resIdx = (Tape.init (([] : List Bool).map Γ.ofBool)).move Dir3.right := by
+    simpa using hres
+  have hinitial :
+      ({ state := (emptyTM L.resIdx).qstart
+         input := inp₀
+         work := work₀
+         output := out₀ } :
+        Cfg k (emptyTM L.resIdx).Q).WithinAuxSpace 0 1 :=
+    ⟨fun i => (hpark i).2, by show inp₀.head ≤ 0 + 1 + 1; omega⟩
+  have key := emptyTM_hoareTimeSpace L.resIdx [] 0 1 inp₀ work₀ out₀ htarget
+    hinpP (fun i _ => (hpark i).1) houtP hinitial
+  simp only [List.length_nil] at key
+  refine key.consequence (fun _ _ _ h => h) ?_ (by omega) (le_refl _) (by omega)
+  rintro inp work out ⟨hi, hframe, hacc, ho⟩
+  exact ⟨hi, ho, by simpa using hacc, hframe⟩
+
+/-- **Compiler part — `var i`.** Reading environment variable `i` copies the
+value on argument tape `i` (for `i < m`) to the result tape via
+`TM.copyWorkToWorkTM`, then restores the argument tape with `TM.rewindWorkTM`;
+for `i ≥ m` (where the read falls off the environment) it materializes the empty
+node with `TM.emptyTM`. Matches `ProgSem.var`. The copy/rewind pair adds only
+linear time and no extra space beyond the copied value, fitting the `a·t + a` /
+`b·s + b` budget with `a = clearWorkTimeBound 0 + 5` and `b = a + 1`. -/
+theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by
+  refine ⟨0, clearWorkTimeBound 0 + 5, clearWorkTimeBound 0 + 6, ?_⟩
+  intro k L
+  by_cases hi : i < m
+  · -- copy argument tape i to the result tape, then rewind the argument tape
+    set src := L.argIdx ⟨i, hi⟩ with hsrc
+    set dst := L.resIdx with hdst
+    have hne : src ≠ dst := L.arg_ne_res ⟨i, hi⟩
+    refine ⟨seqTM (copyWorkToWorkTM src dst) (rewindWorkTM src), ?_⟩
+    intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP
+    obtain ⟨hargs, hres, hscratch, hpark⟩ := hloaded
+    -- identify the result value with argument `i`
+    have hval : Value.data result
+        = (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty :=
+      hsem.value_det _ _ _ ProgSem.var
+    simp only [List.getElem?_ofFn, hi, dif_pos, Option.getD_some] at hval
+    have hresult : result = env ⟨i, hi⟩ := by
+      simpa using hval
+    subst hresult
+    set x := (env ⟨i, hi⟩).toBits with hx
+    set source := (Tape.init (x.map Γ.ofBool)).move Dir3.right with hsource
+    have hsrc_source : work₀ src = source := by rw [hsrc, hargs, hsource, hx]
+    have hsource_head : source.head = 1 := by rw [hsource]; simp [Tape.move]
+    have hsource_out : source.HasOutput x := by
+      have := Tape.init_move_right_hasBinaryString x
+      exact ⟨this.2.1, this.2.2 x.length le_rfl⟩
+    have hsource_cells0 : source.cells 0 = Γ.start := by
+      rw [hsource]; simp [Tape.move, Tape.init]
+    have hsource_nostart : ∀ j, j ≥ 1 → source.cells j ≠ Γ.start := by
+      intro j hj
+      obtain ⟨p, rfl⟩ : ∃ p, j = p + 1 := ⟨j - 1, by omega⟩
+      have hbs := Tape.init_move_right_hasBinaryString x
+      rw [hsource]
+      by_cases hp : p < x.length
+      · rw [hbs.2.1 p hp]; cases (x[p]'hp) <;> simp [Γ.ofBool]
+      · rw [hbs.2.2 p (by omega)]; simp
+    -- copy-phase frame predicate
+    set Pc : Tape → (Fin k → Tape) → Tape → Prop :=
+      fun inp work out => inp = inp₀ ∧ out = out₀ ∧
+        (∀ j, j ≠ src → j ≠ dst → work j = work₀ j) with hPc
+    have hcopy := copyWorkToWorkTM_hoareTime_frame_of_hasOutput src dst hne x source
+      (P := Pc)
+      (by
+        rintro inp work out inp' work' out' ⟨hi1, hi2, hi3⟩ _ _ _ _ _ hii hoo hframe
+        exact ⟨by rw [hii, hi1], by rw [hoo, hi2],
+          fun j hj1 hj2 => by rw [hframe j hj1 hj2]; exact hi3 j hj1 hj2⟩)
+    -- rewind-phase frame predicate
+    set Pr : Tape → (Fin k → Tape) → Tape → Prop :=
+      fun inp work out => inp = inp₀ ∧ out = out₀ ∧
+        (work dst).HasOutput x ∧ (work src).cells = source.cells ∧
+        (∀ j, j ≠ src → j ≠ dst → work j = work₀ j) with hPr
+    have hrewind := rewindWorkTM_hoareTime_frame src (x.length + 1)
+      (P := Pr)
+      (by
+        rintro inp work out inp' work' out' ⟨hi1, hi2, hi3, hi4, hi5⟩
+          hcells hhead hframe hii houtc houth
+        refine ⟨by rw [hii, hi1], ?_, ?_, ?_, ?_⟩
+        · rw [hi2] at houtc houth; exact Tape.ext houth houtc
+        · rw [hframe dst hne.symm]; exact hi3
+        · rw [hcells]; exact hi4
+        · intro j hj1 hj2; rw [hframe j hj1]; exact hi5 j hj1 hj2)
+    -- compose
+    have hcomp := seqTM_hoareTime (copyWorkToWorkTM src dst) (rewindWorkTM src)
+      hcopy ?_ hrewind
+    · -- convert to time-space and fit the budget
+      have hsize := hsem.size_le
+      rw [Value.size_data] at hsize
+      obtain ⟨hst, hss⟩ := hsize
+      have hxlen : x.length = (env ⟨i, hi⟩).size := by rw [hx]; exact (env ⟨i, hi⟩).toBits_length
+      have hHT : (seqTM (copyWorkToWorkTM src dst) (rewindWorkTM src)).HoareTime
+          (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
+          (fun inp work out => inp = inp₀ ∧ out = out₀ ∧
+            (work L.resIdx).HasOutput (env ⟨i, hi⟩).toBits ∧
+            (∀ j, j ≠ L.resIdx → work j = work₀ j))
+          (x.length + 1 + 1 + (x.length + 1 + 2)) := by
+        refine hcomp.consequence ?_ ?_ le_rfl
+        · rintro inp work out ⟨rfl, rfl, rfl⟩
+          exact ⟨hsrc_source, hsource_head, hsource_out,
+            by rw [hdst]; exact hres, hinpP.read_ne_start, houtP.read_ne_start,
+            houtP.1, fun j _ _ => ⟨(hpark j).1.read_ne_start, (hpark j).1.1⟩,
+            rfl, rfl, fun _ _ _ => rfl⟩
+        · rintro inp work out ⟨hhead1, hpr1, hpr2, hpr3, hpr4, hpr5⟩
+          refine ⟨hpr1, hpr2, by rw [← hdst]; exact hpr3, ?_⟩
+          intro j hj
+          by_cases hjs : j = src
+          · subst hjs
+            rw [hsrc_source]
+            exact Tape.ext (hhead1.trans hsource_head.symm) hpr4
+          · exact hpr5 j hjs (by rw [hdst]; exact hj)
+      have hHTS := hHT.toHoareTimeSpace (inputLength := 0) (initialSpace := 1)
+        (by rintro inp work out ⟨rfl, rfl, rfl⟩
+            exact ⟨fun j => (hpark j).2, by show inp.head ≤ 0 + 1 + 1; omega⟩)
+      refine hHTS.consequence (fun _ _ _ h => h) (fun _ _ _ h => h) ?_ (le_refl _) ?_
+      · have hPt : 2 * t ≤ (clearWorkTimeBound 0 + 5) * t := by gcongr; omega
+        omega
+      · have hPs : 2 * s ≤ (clearWorkTimeBound 0 + 6) * s := by gcongr; omega
+        omega
+    · -- boundary transition: all reads ≠ start, so the transition is the identity
+      rintro inp work out ⟨hc1, hc2, hc3, hc4, hc5, hpc1, hpc2, hpc3⟩
+      have hwork_ns : ∀ j, (work j).read ≠ Γ.start := by
+        intro j
+        by_cases hjs : j = src
+        · subst hjs; rw [Tape.read, hc2, hc3.2]; decide
+        · by_cases hjd : j = dst
+          · subst hjd; rw [hc4.read_blank]; decide
+          · rw [hpc3 j hjs hjd]; exact (hpark j).1.read_ne_start
+      have hinp_ns : inp.read ≠ Γ.start := by rw [hpc1]; exact hinpP.read_ne_start
+      have hout_ns : out.read ≠ Γ.start := by rw [hpc2]; exact houtP.read_ne_start
+      obtain ⟨hti, htw, hto⟩ :=
+        phaseTransition_eq_self_of_reads_ne_start hinp_ns hwork_ns hout_ns
+      rw [hti, htw, hto]
+      refine ⟨by rw [hc1]; exact hsource_cells0,
+        fun j hj => by rw [hc1]; exact hsource_nostart j hj, hc2.le, hinp_ns, hout_ns,
+        by rw [hpc2]; exact houtP.1, ?_, hpc1, hpc2, hc4.hasOutput, hc1, hpc3⟩
+      intro j hjs
+      by_cases hjd : j = dst
+      · subst hjd; exact ⟨by rw [hc4.read_blank]; decide, by rw [hc4.1]; omega⟩
+      · rw [hpc3 j hjs hjd]; exact ⟨(hpark j).1.read_ne_start, (hpark j).1.1⟩
+  · -- i ≥ m : the read falls off the environment; materialize the empty node
+    refine ⟨emptyTM L.resIdx, ?_⟩
+    intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP
+    obtain ⟨_, hres, _, hpark⟩ := hloaded
+    have hval : Value.data result
+        = (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty :=
+      hsem.value_det _ _ _ ProgSem.var
+    rw [List.getElem?_ofFn, dif_neg hi, Option.getD_none] at hval
+    injection hval with hresult
+    subst hresult
+    have htarget :
+        work₀ L.resIdx = (Tape.init (([] : List Bool).map Γ.ofBool)).move Dir3.right := by
+      simpa using hres
+    have hinitial :
+        ({ state := (emptyTM L.resIdx).qstart
+           input := inp₀
+           work := work₀
+           output := out₀ } :
+          Cfg k (emptyTM L.resIdx).Q).WithinAuxSpace 0 1 :=
+      ⟨fun i => (hpark i).2, by show inp₀.head ≤ 0 + 1 + 1; omega⟩
+    have key := emptyTM_hoareTimeSpace L.resIdx [] 0 1 inp₀ work₀ out₀ htarget
+      hinpP (fun i _ => (hpark i).1) houtP hinitial
+    simp only [List.length_nil] at key
+    refine key.consequence (fun _ _ _ h => h) ?_ (by omega) (le_refl _) (by omega)
+    rintro inp work out ⟨hi', hframe, hacc, ho⟩
+    exact ⟨hi', ho, by simpa using hacc, hframe⟩
+
+/-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines
+for `h` and `t`, `cons` runs them on a shared tape bank and prepends the head
+value to the tail list on the result tape. Matches `ProgSem.cons`
+(time/space add). -/
+theorem compiled_cons {m : ℕ} {h t : Prog}
+    (ih_h : Compiled m h) (ih_t : Compiled m t) : Compiled m (Prog.cons h t) := by
+  sorry
+
+/-- **Compiler part — `elim v emp (fn (fn body))`** (statement only). Given
+compiled sub-machines for the scrutinee `v` and the empty branch `emp` at arity
+`m`, and for the cons branch `body` at arity `m + 2` (the two fresh tapes hold
+the destructured head and tail), `elim` branches on whether `v` is the empty
+node. Matches `ProgSem.elim_nil` / `ProgSem.elim_cons`. -/
+theorem compiled_elim {m : ℕ} {v emp body : Prog}
+    (ih_v : Compiled m v) (ih_emp : Compiled m emp) (ih_body : Compiled (m + 2) body) :
+    Compiled m (Prog.elim v emp (.fn (.fn body))) := by
+  sorry
+
+/-- **Compiler part — `ifEq x y then_ else_`** (statement only). Given compiled
+sub-machines for all four arguments at arity `m`, `ifEq` compares the values of
+`x` and `y` and runs the matching branch. Matches `ProgSem.ifEq_then` /
+`ProgSem.ifEq_else`. -/
+theorem compiled_ifEq {m : ℕ} {x y then_ else_ : Prog}
+    (ih_x : Compiled m x) (ih_y : Compiled m y)
+    (ih_then : Compiled m then_) (ih_else : Compiled m else_) :
+    Compiled m (Prog.ifEq x y then_ else_) := by
+  sorry
+
+/-- **Compiler part — `while_ init (fn body)`** (statement only). Given a
+compiled sub-machine for `init` at arity `m` and for the loop `body` at arity
+`m + 1` (the fresh tape holds the accumulator), `while_` iterates the body on the
+accumulator tape until its head is empty. Matches `ProgSem.while_` /
+`WhileSem` (which already uses `max` for space, exactly the loop's reuse). -/
+theorem compiled_while {m : ℕ} {init body : Prog}
+    (ih_init : Compiled m init) (ih_body : Compiled (m + 1) body) :
+    Compiled m (Prog.while_ init (.fn body)) := by
+  sorry
+
+/-- **Compiler part — `app (fn body) arg`** (the in-place `let`; statement only).
+Given a compiled sub-machine for `arg` at arity `m` and for `body` at arity
+`m + 1`, `app` evaluates `arg` onto a fresh environment tape and then runs
+`body`. Matches `ProgSem.app` composed with `AppSem.mk` (running `body` in
+`σ ++ [v]`). Nested uses give multi-argument `let`-chains, hence arbitrary
+arities. -/
+theorem compiled_app {m : ℕ} {body arg : Prog}
+    (ih_body : Compiled (m + 1) body) (ih_arg : Compiled m arg) :
+    Compiled m (Prog.app (.fn body) arg) := by
+  sorry
+
+/-- **The internal compiler recursion.** For every argument arity `m`, every
+first-order (`InPlace`) program compiles to a reusable tape-indexed Turing
+machine subroutine satisfying `Prog.RunsAsSubroutine`.
+
+The recursion structure is fully assembled here: induction on the `InPlace`
+derivation dispatches each program constructor to its compiler part
+(`compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`,
+`compiled_ifEq`, `compiled_while`, `compiled_app`), threading the argument arity
+so that `elim`/`while_`/`app` compile their body at the extended arity (`m + 2`,
+`m + 1`, `m + 1`) that the `σ`-extension of the operational semantics uses. Only
+the individual parts carry `sorry`; the assembly below is complete. -/
+theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) :
+    Compiled m p := by
+  induction hp generalizing m with
+  | var => exact compiled_var m _
+  | empty => exact compiled_empty m
+  | cons _ _ ih_h ih_t => exact compiled_cons ih_h ih_t
+  | elim _ _ _ ih_v ih_emp ih_body => exact compiled_elim ih_v ih_emp ih_body
+  | ifEq _ _ _ _ ih_x ih_y ih_then ih_else =>
+      exact compiled_ifEq ih_x ih_y ih_then ih_else
+  | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body
+  | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal/EmptyTM.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal/EmptyTM.lean
new file mode 100644
index 00000000..263d283e
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal/EmptyTM.lean
@@ -0,0 +1,278 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+import Complexitylib.Models.TuringMachine.Registers.Emit
+import Complexitylib.Models.TuringMachine.Subroutines.ClearWork
+import Complexitylib.Models.TuringMachine.Hoare
+import Complexitylib.Models.TuringMachine.Hoare.Space
+
+/-!
+# The `empty` constructor as a tape-indexed Turing-machine subroutine
+
+The rose tree machine `empty` constructor produces the empty node, whose
+balanced-parenthesis serialization is the two-bit word `[false, true]`
+(an open followed by a close parenthesis). This module builds the Turing
+machine that materializes that word on a **caller-chosen work tape**, so it can
+serve as the machine the compiler maps `Prog.empty` to.
+
+The construction is deliberately parameterized only by the target tape index:
+
+- `TM.emitBitsWorkTM idx w` — a reusable subroutine that appends a *fixed* word
+  `w` to work tape `idx` (the work-tape analogue of the output-tape
+  `TM.emitBitsTM`), one cell per step.
+- `TM.emptyTM idx` — clears work tape `idx` first (reusing `TM.clearWorkTM`, so
+  the machine works regardless of the tape's prior contents), then writes
+  `[false, true]`. Running the clear first costs only linear extra time and
+  does not increase the space footprint.
+
+## Main results
+
+- `TM.emitBitsWorkTM_hoareTime` — `emitBitsWorkTM idx w` writes `w` onto work
+  tape `idx` in `|w|` steps, framing every other tape.
+- `TM.emitBitsWorkTM_isTransducer` — the writer never moves the output head left.
+- `TM.emptyTM_hoareTime` — from any canonical Boolean target tape, `emptyTM idx`
+  leaves `[false, true]` on tape `idx` (`OutAcc`/`HasOutput`), framing the rest,
+  in time linear in the tape's prior length.
+- `TM.emptyTM_hoareTimeSpace` — the corresponding additive space contract.
+- `TM.emptyTM_isTransducer` — `emptyTM` never moves the output head left.
+-/
+
+namespace Complexity
+
+namespace TM
+
+variable {n : ℕ}
+
+-- ════════════════════════════════════════════════════════════════════════
+-- emitBitsWorkTM: append a fixed word to a work tape
+-- ════════════════════════════════════════════════════════════════════════
+
+/-- **Append the fixed word `w` to work tape `idx`** and halt. State `k` = the
+number of bits already written; each step writes bit `k` on tape `idx`, moves
+that head right, and leaves the input, output, and every other work tape parked
+and untouched. This is the work-tape analogue of `emitBitsTM`. -/
+def emitBitsWorkTM (idx : Fin n) (w : List Bool) : TM n where
+  Q := Fin (w.length + 1)
+  qstart := ⟨0, by omega⟩
+  qhalt := ⟨w.length, by omega⟩
+  δ := fun k iHead wHeads oHead =>
+    if h : k.val < w.length then
+      (⟨k.val + 1, by omega⟩,
+       fun i => if i = idx then Γw.ofBool w[k.val] else readBackWrite (wHeads i),
+       readBackWrite oHead,
+       idleDir iHead,
+       fun i => if i = idx then Dir3.right else idleDir (wHeads i),
+       idleDir oHead)
+    else
+      allIdle k iHead wHeads oHead
+  δ_right_of_start := by
+    intro k iHead wHeads oHead
+    by_cases h : k.val < w.length
+    · simp only [h, ↓reduceDIte]
+      refine ⟨idleDir_right_of_start, ?_, idleDir_right_of_start⟩
+      intro i hi
+      split
+      · rfl
+      · exact idleDir_right_of_start hi
+    · simp only [h, ↓reduceDIte]
+      exact rightOfStart_allIdle iHead wHeads oHead
+
+/-- One write step: from state `k < |w|`, the machine writes bit `k` on tape
+`idx`, advances the accumulator, and leaves the parked input, output, and other
+work tapes unchanged. -/
+private theorem emitBitsWorkTM_step (idx : Fin n) (w : List Bool)
+    (c : Cfg n (emitBitsWorkTM (n := n) idx w).Q) (k : ℕ) (hk : k < w.length)
+    (hst : c.state = ⟨k, by omega⟩)
+    (hinp : Parked c.input) (hout : Parked c.output)
+    (hother : ∀ i, i ≠ idx → Parked (c.work i)) :
+    (emitBitsWorkTM (n := n) idx w).step c = some
+      { state := ⟨k + 1, by omega⟩, input := c.input,
+        work := Function.update c.work idx
+          ((c.work idx).writeAndMove (Γ.ofBool w[k]) .right),
+        output := c.output } := by
+  have hne : ¬ c.state = (emitBitsWorkTM (n := n) idx w).qhalt := by
+    rw [hst]
+    simp only [emitBitsWorkTM, Fin.mk.injEq]
+    omega
+  rw [TM.step, if_neg hne]
+  simp only [emitBitsWorkTM, hst, hk, ↓reduceDIte]
+  refine congrArg some ((Cfg.mk.injEq ..).mpr ⟨rfl, ?_, ?_, ?_⟩)
+  · exact hinp.move_idle
+  · funext i
+    by_cases hi : i = idx
+    · subst hi
+      simp only [if_true, Function.update_self, Γw.ofBool_toΓ]
+    · simp only [if_neg hi, Function.update_of_ne hi]
+      exact (hother i hi).writeAndMove_readBack_idle
+  · exact hout.writeAndMove_readBack_idle
+
+/-- The write loop: from state `k` with `|w| = k + m`, the machine reaches the
+halt state in exactly `m` steps, appending `w.drop k` to tape `idx` and
+preserving the input, output, and other work tapes. -/
+private theorem emitBitsWorkTM_run (idx : Fin n) (w : List Bool) (m : ℕ) :
+    ∀ (k : ℕ) (hk : w.length = k + m),
+      ∀ (c : Cfg n (emitBitsWorkTM (n := n) idx w).Q) (ys : List Bool),
+      c.state = ⟨k, by omega⟩ → Parked c.input → Parked c.output →
+      (∀ i, i ≠ idx → Parked (c.work i)) → OutAcc ys (c.work idx) →
+      ∃ c', (emitBitsWorkTM (n := n) idx w).reachesIn m c c' ∧
+        c'.state = ⟨w.length, by omega⟩ ∧ c'.input = c.input ∧
+        c'.output = c.output ∧ (∀ i, i ≠ idx → c'.work i = c.work i) ∧
+        OutAcc (ys ++ w.drop k) (c'.work idx) := by
+  induction m with
+  | zero =>
+    intro k hk c ys hst _ _ _ hacc
+    refine ⟨c, .zero, ?_, rfl, rfl, fun _ _ => rfl, ?_⟩
+    · rw [hst]; congr 1; omega
+    · rw [List.drop_of_length_le (by omega), List.append_nil]
+      exact hacc
+  | succ m ih =>
+    intro k hk c ys hst hinp hout hother hacc
+    have hklt : k < w.length := by omega
+    have hstep := emitBitsWorkTM_step idx w c k hklt hst hinp hout hother
+    set c₁ : Cfg n (emitBitsWorkTM (n := n) idx w).Q :=
+      { state := ⟨k + 1, by omega⟩, input := c.input,
+        work := Function.update c.work idx
+          ((c.work idx).writeAndMove (Γ.ofBool w[k]) .right),
+        output := c.output } with hc₁
+    have hother₁ : ∀ i, i ≠ idx → Parked (c₁.work i) := by
+      intro i hi
+      show Parked (Function.update c.work idx _ i)
+      rw [Function.update_of_ne hi]
+      exact hother i hi
+    have hacc₁ : OutAcc (ys ++ [w[k]]) (c₁.work idx) := by
+      show OutAcc _ (Function.update c.work idx _ idx)
+      rw [Function.update_self]
+      exact outAcc_append_bit hacc w[k]
+    obtain ⟨c', hreach, hst', hinp', hout', hwork', hacc'⟩ :=
+      ih (k + 1) (by omega) c₁ (ys ++ [w[k]]) rfl hinp hout hother₁ hacc₁
+    refine ⟨c', .step hstep hreach, hst', hinp', hout', ?_, ?_⟩
+    · intro i hi
+      rw [hwork' i hi]
+      show Function.update c.work idx _ i = c.work i
+      rw [Function.update_of_ne hi]
+    · rwa [List.append_assoc, List.singleton_append,
+        List.getElem_cons_drop] at hacc'
+
+/-- **`emitBitsWorkTM` Hoare specification.** Writes the word `w` onto work tape
+`idx` in `|w|` steps, leaving the input, output, and every other (parked) work
+tape literally unchanged. Ghost-parametrized by the initial tapes so it composes
+through `seqTM_hoareTime`. The starting tape `idx` is the empty accumulator (a
+blank tape rewound to cell 1). -/
+theorem emitBitsWorkTM_hoareTime (idx : Fin n) (w : List Bool)
+    (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape)
+    (hinp₀ : Parked inp₀) (hout₀ : Parked out₀)
+    (hother₀ : ∀ i, i ≠ idx → Parked (work₀ i))
+    (hidx₀ : OutAcc [] (work₀ idx)) :
+    (emitBitsWorkTM (n := n) idx w).HoareTime
+      (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
+      (fun inp work out =>
+        inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧
+        OutAcc w (work idx) ∧ out = out₀)
+      w.length := by
+  rintro inp work out ⟨rfl, rfl, rfl⟩
+  obtain ⟨c', hreach, hst', hinp', hout', hwork', hacc'⟩ :=
+    emitBitsWorkTM_run idx w w.length 0 (by omega)
+      { state := ⟨0, by omega⟩, input := inp, work := work, output := out }
+      [] rfl hinp₀ hout₀ hother₀ (by simpa using hidx₀)
+  refine ⟨c', w.length, le_refl _, hreach, hst', hinp', hwork', ?_, hout'⟩
+  rwa [List.nil_append, List.drop_zero] at hacc'
+
+/-- Fixed-word work-tape emission never moves the output head left. -/
+theorem emitBitsWorkTM_isTransducer (idx : Fin n) (w : List Bool) :
+    (emitBitsWorkTM (n := n) idx w).IsTransducer := by
+  intro k iHead wHeads oHead
+  by_cases h : k.val < w.length
+  · simp [emitBitsWorkTM, h, idleDir]
+    split <;> decide
+  · simp [emitBitsWorkTM, h, allIdle, idleDir]
+    split <;> decide
+
+-- ════════════════════════════════════════════════════════════════════════
+-- emptyTM: clear then materialize the empty node's serialization
+-- ════════════════════════════════════════════════════════════════════════
+
+/-- **The Turing machine for the rose tree `empty` constructor.** Clears work
+tape `idx` (so it works from any prior canonical Boolean content), then writes
+the two-bit serialization `[false, true]` of the empty node onto it. -/
+def emptyTM (idx : Fin n) : TM n :=
+  seqTM (clearWorkTM idx) (emitBitsWorkTM idx [false, true])
+
+/-- The empty accumulator is exactly a rewound blank work tape. -/
+private theorem outAcc_nil_move_right :
+    OutAcc [] ((Tape.init []).move Dir3.right) :=
+  outAcc_nil_init
+
+/-- **`emptyTM` Hoare specification.** Starting from any canonical Boolean
+target tape `idx`, `emptyTM idx` produces the empty node's serialization
+`[false, true]` on tape `idx`, leaves the input, output, and every other work
+tape unchanged, and runs in `clearWorkTimeBound bits.length + 3` steps —
+linear in the tape's prior length. -/
+theorem emptyTM_hoareTime (idx : Fin n) (bits : List Bool)
+    (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape)
+    (htarget : work₀ idx = (Tape.init (bits.map Γ.ofBool)).move Dir3.right)
+    (hinp : Parked inp₀) (hother : ∀ i, i ≠ idx → Parked (work₀ i))
+    (hout : Parked out₀) :
+    (emptyTM idx).HoareTime
+      (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
+      (fun inp work out =>
+        inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧
+        (work idx).HasOutput [false, true] ∧ out = out₀)
+      (clearWorkTimeBound bits.length + 1 + 2) := by
+  set wc := Function.update work₀ idx ((Tape.init []).move Dir3.right) with hwc_def
+  have hidx0 : OutAcc [] (wc idx) := by
+    rw [hwc_def, Function.update_self]; exact outAcc_nil_move_right
+  have hwcParked : ∀ i, Parked (wc i) := by
+    intro i
+    by_cases hi : i = idx
+    · subst hi; exact hidx0.parked
+    · rw [hwc_def, Function.update_of_ne hi]; exact hother i hi
+  refine (seqTM_hoareTime (clearWorkTM idx) (emitBitsWorkTM idx [false, true])
+    (clearWorkTM_hoareTime_frame idx bits inp₀ work₀ out₀ htarget hinp hother hout)
+    ?htrans
+    (emitBitsWorkTM_hoareTime idx [false, true] inp₀ wc out₀ hinp hout
+      (fun i _ => hwcParked i) hidx0)).strengthen_post ?hpost
+  · rintro inp work out ⟨rfl, rfl, rfl⟩
+    exact ⟨hinp.transitionInput_eq_self,
+      funext fun i => (hwcParked i).transitionTape_eq_self,
+      hout.transitionTape_eq_self⟩
+  · rintro inp work out ⟨hi, hframe, hacc, ho⟩
+    refine ⟨hi, fun i hi' => ?_, hacc.hasOutput, ho⟩
+    rw [hframe i hi', hwc_def, Function.update_of_ne hi']
+
+/-- `emptyTM` never moves the output head left. -/
+theorem emptyTM_isTransducer (idx : Fin n) :
+    (emptyTM idx).IsTransducer :=
+  (clearWorkTM_isTransducer idx).seqTM (emitBitsWorkTM_isTransducer idx [false, true])
+
+/-- **Time-and-space form of `emptyTM_hoareTime`.** Starting within an
+`initialSpace` budget, materializing the empty node stays within
+`initialSpace + (clearWorkTimeBound bits.length + 3)` — the standard additive
+over-approximation (one cell per step). Since the running time is linear in the
+target tape's prior length, so is the extra space charged here. -/
+theorem emptyTM_hoareTimeSpace (idx : Fin n) (bits : List Bool)
+    (inputLength initialSpace : ℕ)
+    (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape)
+    (htarget : work₀ idx = (Tape.init (bits.map Γ.ofBool)).move Dir3.right)
+    (hinp : Parked inp₀) (hother : ∀ i, i ≠ idx → Parked (work₀ i))
+    (hout : Parked out₀)
+    (hinitial :
+      ({ state := (emptyTM idx).qstart
+         input := inp₀
+         work := work₀
+         output := out₀ } :
+        Cfg n (emptyTM idx).Q).WithinAuxSpace inputLength initialSpace) :
+    (emptyTM idx).HoareTimeSpace
+      (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
+      (fun inp work out =>
+        inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧
+        (work idx).HasOutput [false, true] ∧ out = out₀)
+      (clearWorkTimeBound bits.length + 1 + 2) inputLength
+      (initialSpace + (clearWorkTimeBound bits.length + 1 + 2)) :=
+  (emptyTM_hoareTime idx bits inp₀ work₀ out₀ htarget hinp hother hout).toHoareTimeSpace
+    (by rintro inp work out ⟨rfl, rfl, rfl⟩; exact hinitial)
+
+end TM
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Models/RoseTreeMachine/Data.lean
new file mode 100644
index 00000000..6aeadcf2
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Data.lean
@@ -0,0 +1,157 @@
+/-
+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 Mathlib.Data.Part
+
+/-!
+# Main internal data type for the rose tree machine (RTM)
+
+This file contains the main internal data structure for the RTM, `Data`, a rose tree.
+
+## Main definitions and notations
+
+- `Data` - the main data structure
+- `Data.size` - the size of a `Data` object when encoded using parentheses, complexity results
+  use this size as the main measure.
+- `Data.recL` - the main recursion principle for `Data`
+- `Data.inductionL` - the main induction principle for `Data`
+
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+/-- Rose-tree data structure, it allows us to encode most of Lean's data structures in a
+"natural" manner -/
+inductive Data where
+  | l : List Data → Data
+deriving Repr
+
+mutual
+  /-- Decidable equality for `Data`, defined jointly with `Data.listDecEq`. -/
+  def Data.decEq : ∀ (a b : Data), Decidable (a = b)
+    | .l xs, .l ys =>
+      match Data.listDecEq xs ys with
+      | isTrue h => isTrue (congrArg Data.l h)
+      | isFalse h => isFalse fun heq => h (Data.l.inj heq)
+  /-- Decidable equality for `List Data`, defined jointly with `Data.decEq`. -/
+  def Data.listDecEq : ∀ (xs ys : List Data), Decidable (xs = ys)
+    | [], [] => isTrue rfl
+    | [], _ :: _ => isFalse (by simp)
+    | _ :: _, [] => isFalse (by simp)
+    | x :: xs, y :: ys =>
+      match Data.decEq x y, Data.listDecEq xs ys with
+      | isTrue hxy, isTrue hxys => isTrue (congrArg₂ List.cons hxy hxys)
+      | isFalse hxy, _ => isFalse fun h => hxy (List.cons.inj h).1
+      | _, isFalse hxys => isFalse fun h => hxys (List.cons.inj h).2
+end
+
+instance : DecidableEq Data := Data.decEq
+instance : BEq Data := inferInstance
+instance : LawfulBEq Data := inferInstance
+
+/-- The empty `Data` node, `Data.l []`. -/
+abbrev Data.empty := Data.l []
+
+
+/-- The list of children of a `Data` node. -/
+@[scoped grind =]
+def Data.asList
+  | Data.l xs => xs
+
+@[scoped grind =]
+lemma Data.asList_empty : Data.empty.asList = [] := by rfl
+
+@[simp, scoped grind =]
+lemma Data.asList_l (d : Data) : Data.l d.asList = d := by simp [Data.asList]; grind
+
+@[simp, scoped grind =]
+lemma Data.l_asList (xs : List Data) : (Data.l xs).asList = xs := by simp [Data.asList]
+
+/-- The encoding length of `d`, relevant for complexity.
+This is the encoded size assuming an encoding into parenthesized expressions. -/
+def Data.size : Data → ℕ
+  | Data.l xs => 2 + (xs.map Data.size |>.sum)
+
+@[simp]
+lemma Data.size_le {d : Data} : 0 < d.size := by
+  obtain ⟨xs⟩ := d
+  grind [Data.size]
+
+@[simp, scoped grind =]
+lemma Data.size_empty : Data.empty.size = 2 := by simp [Data.empty, Data.size]
+
+@[simp, scoped grind =]
+lemma Data.cons_size {h : Data} {t : List Data} :
+    (Data.l (h :: t)).size = h.size + (Data.l t).size := by
+  simp [Data.size]
+  grind
+
+/-- Recursion principle for `Data`. -/
+@[elab_as_elim]
+def Data.recL {motive : Data → Sort*}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) :
+    ∀ d, motive d
+  | .l [] => nil
+  | .l (x :: xs) =>
+      cons x xs (Data.recL nil cons x) (Data.recL nil cons (.l xs))
+
+/-- Induction principle for `Data`, the `Prop`-valued companion to `Data.recL`. -/
+@[elab_as_elim]
+theorem Data.inductionL {motive : Data → Prop}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs)))
+    (d : Data) : motive d :=
+  Data.recL nil cons d
+
+mutual
+/-- Serialize a `Data` value to a balanced-parenthesis bit string: a node
+`Data.l xs` becomes `false` (open bracket), the concatenated serializations of
+its children, then `true` (close bracket). This is the physical layout used to
+store a `Data` value on a Turing-machine tape; its length equals `Data.size`
+(see `Data.toBits_length`), so the tape uses exactly `d.size` cells. -/
+def Data.toBits : Data → List Bool
+  | .l xs => false :: Data.toBitsList xs ++ [true]
+/-- Concatenated serializations of a list of `Data` nodes; the recursive helper
+of `Data.toBits`. -/
+def Data.toBitsList : List Data → List Bool
+  | [] => []
+  | x :: xs => Data.toBits x ++ Data.toBitsList xs
+end
+
+@[simp] lemma Data.toBits_l (xs : List Data) :
+    (Data.l xs).toBits = false :: Data.toBitsList xs ++ [true] := rfl
+
+@[simp] lemma Data.toBitsList_nil : Data.toBitsList [] = [] := rfl
+
+@[simp] lemma Data.toBitsList_cons (x : Data) (xs : List Data) :
+    Data.toBitsList (x :: xs) = x.toBits ++ Data.toBitsList xs := rfl
+
+/-- The serialization length equals `Data.size`: a tape holding `d.toBits` uses
+exactly `d.size` cells. This is the bridge between RTM space (`Data.size`) and
+the Turing-machine tape space that stores the value. -/
+@[simp] lemma Data.toBits_length (d : Data) : d.toBits.length = d.size := by
+  induction d using Data.inductionL with
+  | nil => simp
+  | cons x xs ihx ihxs =>
+    simp only [Data.toBits_l, Data.toBitsList_cons, Data.cons_size,
+      List.length_append, List.length_cons, List.length_nil] at *
+    omega
+
+/-- Index of a tape cell used by the rose tree machine's execution model. -/
+abbrev TapeIndex := ℕ
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean b/Complexitylib/Models/RoseTreeMachine/DataEncode.lean
new file mode 100644
index 00000000..3d06b0f9
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/DataEncode.lean
@@ -0,0 +1,107 @@
+/-
+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 Complexitylib.Models.RoseTreeMachine.Data
+public import Mathlib.Data.Nat.Bits
+public import Mathlib.Data.List.Basic
+
+/-!
+# Encodings into `Data`
+
+This file defines the class that is used to encode arbitrary data structures into `Data`,
+so that RTMs (rose tree machines) can operate on them.
+
+Instances are provided for convenience for `Data` itself, `Bool`, `List α`, `Option α`, `α × β`,
+and `ℕ` (binary encoding via `List Bool`)
+
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+/-- Encoding of types into `Data`. -/
+class DataEncode (α : Type) where
+  /-- Encode a value of `α` as `Data`. -/
+  encode : α → Data
+  /-- The encoding is injective, so distinct values never collide. -/
+  h_inj : encode.Injective
+
+instance : DataEncode Data where
+  encode b := b
+  h_inj := by intros a b h_eq; grind
+
+@[simp, scoped grind =]
+lemma DataEncode_encode_data (d : Data) : DataEncode.encode d = d := rfl
+
+instance : DataEncode Bool where
+  encode b := if b then Data.l [ Data.l [] ] else Data.l []
+  h_inj := by intros a b h_eq; grind
+
+instance (α : Type) [DataEncode α] : DataEncode (List α) where
+  encode xs := Data.l (xs.map DataEncode.encode)
+  h_inj := by
+    intro a b h
+    exact List.map_injective_iff.mpr DataEncode.h_inj (Data.l.inj h)
+
+@[simp, scoped grind =]
+lemma DataEncode_list_nil {α : Type} [DataEncode α] :
+  DataEncode.encode ([] : List α) = Data.l [] := by
+  simp [DataEncode.encode]
+
+@[simp, scoped grind =]
+lemma DataEncode_list_eq_nil_iff_nil {α : Type} [DataEncode α] (xs : List α) :
+  DataEncode.encode xs = Data.empty ↔ xs = [] := by
+  simp [DataEncode.encode]
+
+@[simp, scoped grind =]
+lemma DataEncode_list_tail {α : Type} [DataEncode α] (xs : List α) :
+  (DataEncode.encode xs).asList.tail = (DataEncode.encode xs.tail).asList := by
+  simp [DataEncode.encode]
+
+instance (α : Type) [DataEncode α] : DataEncode (Option α) where
+  encode := fun
+    | none => Data.l []
+    | some x => Data.l [DataEncode.encode x]
+  h_inj := by
+    intro a b h
+    grind [DataEncode.h_inj]
+
+@[simp]
+lemma DataEncode_Option_empty {α : Type} [DataEncode α] (x : Option α) :
+  (DataEncode.encode x == Data.empty) = x.isNone := by
+  cases x <;> simp [DataEncode.encode, Data.empty]
+
+instance (α β : Type) [DataEncode α] [DataEncode β] : DataEncode (α × β) where
+  encode := fun (a, b) => Data.l [DataEncode.encode a, DataEncode.encode b]
+  h_inj := by
+    intro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
+    grind [DataEncode.h_inj]
+
+lemma DataEncode_pair {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) :
+  DataEncode.encode (a, b) = Data.l [DataEncode.encode a, DataEncode.encode b] := by
+  simp [DataEncode.encode]
+
+instance : DataEncode ℕ where
+  encode x := DataEncode.encode (Nat.bits x)
+  h_inj := by
+    intro a b h
+    have hb : a.bits = b.bits := DataEncode.h_inj h
+    have hrec : ∀ n : ℕ, n.bits.foldr (fun b acc => Nat.bit b acc) 0 = n := by
+      intro n
+      induction n using Nat.binaryRec' with
+      | zero => simp
+      | bit b n hn ih => rw [Nat.bits_append_bit n b hn]; simp [ih]
+    have := congrArg (List.foldr (fun b acc => Nat.bit b acc) 0) hb
+    simpa [hrec] using this
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Prog.lean b/Complexitylib/Models/RoseTreeMachine/Prog.lean
new file mode 100644
index 00000000..f6494672
--- /dev/null
+++ b/Complexitylib/Models/RoseTreeMachine/Prog.lean
@@ -0,0 +1,396 @@
+/-
+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 Complexitylib.Models.RoseTreeMachine.Data
+public import Complexitylib.Models.RoseTreeMachine.DataEncode
+
+
+/-!
+# Programs in a rose tree machine (RTM)
+
+This file contains the main definition of the rose tree machine, its programs including
+semantics and time and space resource consumption.
+
+## Main definitions and notations
+
+- `Prog` - the program
+- `ProgSem` - semantics and resource consumption
+- `InPlace` - a fragment of the language that can be easily simulated using multi-tape Turing
+    machines.
+- `Prog.ComputesInTimeAndSpace` - this defines the complexity notion for the RTM computation model,
+    based on `Data` values.
+- `Prog.ComputesBoolFunInTimeAndSpace` - the complexity notion transferred to functions on binary
+    strings, this making it compatible to all other computation models.
+- `ComputableInOTime` - generic time-complexity in the RTM model
+- `ComputableInOSpace` - generic space-complexity in the RTM model
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace RoseTreeMachine
+
+/--
+Prog is the syntax representation of a functional language that has a resource consumption
+model which is compatible to that of a Turing machine.
+The data structure it operates on is a rose tree (`Data`). The advantage of this data structure
+is that the majority of lean data types have a direct encoding.
+-/
+inductive Prog where
+  /-- Variable reference at de Bruijn level `id`. -/
+  | var (id : ℕ)
+  /-- The empty constructor of `Data`. -/
+  | empty
+  /-- The `cons` constructor of `Data`: prepend the value of `h` to the list value of `t`. -/
+  | cons (h t : Prog)
+  /-- Destructor of `Data`: evaluate `v`; if it is `empty`, run `emp`; otherwise destructure into
+      `head` and `tail` and apply the function `cs` to `head` and then to `tail`. -/
+  | elim (v emp cs : Prog)
+  /-- Equality comparison: If `x` evaluates to the same data as `y`, run `then_`, else
+  run `else_`.
+  This can be simulated using `while_` below, but it is useful to have. -/
+  | ifEq (x y then_ else_ : Prog)
+  /-- While loop: evaluate `init` to the starting accumulator; `body` must evaluate
+      to a one-argument function which is applied to the current accumulator on each
+      iteration. Return the accumulator if its head is empty. -/
+  | while_ (init body : Prog)
+  /-- Abstraction / closure in one variable. -/
+  | fn (body : Prog)
+  /-- Function application. -/
+  | app (fn arg : Prog)
+deriving Repr
+
+/-- Runtime values for the semantics predicate `ProgSem`. -/
+inductive Value where
+  | data (d : Data)
+  | closure (body : Prog) (env : List Value)
+deriving Repr
+
+/-- The empty `Value`, wrapping the empty `Data` node. -/
+abbrev Value.empty : Value := .data (Data.l [])
+
+/-- Whether the program `Prog` refers to the variable at de Bruijn index `i`. -/
+def Prog.hasVar (i : ℕ) : Prog → Bool
+  | .var j => i = j
+  | .empty => false
+  | .cons h t => h.hasVar i || t.hasVar i
+  | .elim v emp cs => v.hasVar i || emp.hasVar i || cs.hasVar i
+  | .ifEq x y then_ else_ =>
+      x.hasVar i || y.hasVar i || then_.hasVar i || else_.hasVar i
+  | .while_ init body => init.hasVar i || body.hasVar i
+  | .fn body => body.hasVar i
+  | .app f arg => f.hasVar i || arg.hasVar i
+
+
+mutual
+  /-- The size of a closure's environment, restricted to variables that `body` actually
+  references. -/
+  def closureSize (body : Prog) (env : List Value) : ℕ :=
+    let rec go (depth : ℕ) (env : List Value) : ℕ :=
+      match env with
+      | [] => 0
+      | hd :: tl => go (depth + 1) tl + if body.hasVar depth then hd.size else 0
+    go 0 env
+
+  /-- The size of a `Value`. The size of data is the length of its encoding and the size
+  of a closure is the sum of the sizes of the referenced variables. -/
+  @[simp]
+  def Value.size : Value → ℕ
+    | .data d => d.size
+    | .closure p env => closureSize p env
+end
+
+-- `closureSize.go` is an internal helper generated from the `let rec` inside `closureSize`;
+-- doc comments cannot be placed directly on `let rec` definitions (doing so breaks
+-- elaboration), so the docBlame lint is suppressed here instead.
+attribute [nolint docBlame] closureSize.go
+
+@[simp, scoped grind =]
+lemma closureSize_of_noVar {body : Prog} {env : List Value} (h : ∀ i, ¬body.hasVar i) :
+    closureSize body env = 0 := by
+  have (depth : ℕ) : closureSize.go body depth env = 0 := by
+    induction env generalizing depth with
+    | nil => simp [closureSize.go]
+    | cons hd tl ih => simp [closureSize.go, h depth, ih]
+  simp [closureSize, this]
+
+@[simp, scoped grind =]
+lemma closureSize_of_var {env : List Value} :
+    closureSize (.var i) env = (env[i]?.map fun v => v.size).getD 0 := by
+  unfold closureSize
+  have (d : ℕ) : closureSize.go (.var i) d env =
+      if h : d ≤ i ∧ i - d < env.length then (env[i - d]'(by grind)).size else 0 := by
+    induction env generalizing d with
+    | nil => simp [closureSize.go]
+    | cons hd tl ih =>
+      grind [closureSize.go, List.length_cons, Prog.hasVar]
+  grind
+
+
+@[scoped grind =]
+lemma Value.size_data {d : Data} : (Value.data d).size = d.size := by simp [Value.size]
+
+/-- Splitting the environment of a closure size computation across an append. -/
+lemma closureSize.go_append (body : Prog) (depth : ℕ) (l1 l2 : List Value) :
+    closureSize.go body depth (l1 ++ l2)
+      = closureSize.go body depth l1 + closureSize.go body (depth + l1.length) l2 := by
+  induction l1 generalizing depth with
+  | nil => simp [closureSize.go]
+  | cons hd tl ih =>
+      have he : depth + 1 + tl.length = depth + (tl.length + 1) := by omega
+      simp only [List.cons_append, closureSize.go, List.length_cons, ih (depth + 1), he]
+      omega
+
+/-- The closure size over an appended environment splits into the size over the prefix plus the
+contribution of the suffix (counted starting at depth `l1.length`). -/
+lemma closureSize_append (body : Prog) (l1 l2 : List Value) :
+    closureSize body (l1 ++ l2)
+      = closureSize body l1 + closureSize.go body l1.length l2 := by
+  simp only [closureSize, closureSize.go_append, Nat.zero_add]
+
+/-- `closureSize.go` is monotone in the set of accessed variables. -/
+lemma closureSize.go_mono {body1 body2 : Prog} (env : List Value)
+    (h : ∀ i, body1.hasVar i → body2.hasVar i) (depth : ℕ) :
+    closureSize.go body1 depth env ≤ closureSize.go body2 depth env := by
+  induction env generalizing depth with
+  | nil => simp [closureSize.go]
+  | cons hd tl ih =>
+      simp only [closureSize.go]
+      have hb : (if body1.hasVar depth then hd.size else 0)
+          ≤ (if body2.hasVar depth then hd.size else 0) := by
+        by_cases hv : body1.hasVar depth
+        · simp [hv, h depth hv]
+        · simp [hv]
+      have := ih (depth + 1)
+      omega
+
+/-- If every variable accessed by `body1` is also accessed by `body2`, then `body1` has a smaller
+closure size over any environment. -/
+lemma closureSize_mono {body1 body2 : Prog} (env : List Value)
+    (h : ∀ i, body1.hasVar i → body2.hasVar i) :
+    closureSize body1 env ≤ closureSize body2 env := by
+  have := closureSize.go_mono env h 0
+  simpa only [closureSize] using this
+
+/-- The closure size is bounded by the total size of the environment. -/
+lemma closureSize.go_le_sum (body : Prog) (depth : ℕ) (env : List Value) :
+    closureSize.go body depth env ≤ (env.map Value.size).sum := by
+  induction env generalizing depth with
+  | nil => simp [closureSize.go]
+  | cons hd tl ih =>
+      simp only [closureSize.go, List.map_cons, List.sum_cons]
+      have h1 := ih (depth + 1)
+      have h2 : (if body.hasVar depth then hd.size else 0) ≤ hd.size := by
+        by_cases hv : body.hasVar depth <;> simp [hv]
+      omega
+
+mutual
+/-- Semantics of `Prog` including time and space resource bounds.
+`ProgSem σ p x t s` means that on environment `σ`, the program `p` evaluates to the value
+`x` and uses `t` time and `s` space. -/
+inductive ProgSem : (List Value) → Prog → Value → ℕ → ℕ → Prop
+  | var :
+      ProgSem σ (.var i) (σ[i]?.getD Value.empty)
+        (σ[i]?.getD Value.empty).size (σ[i]?.getD Value.empty).size
+  | empty : ProgSem σ .empty Value.empty 2 2
+  | cons (h₁ : ProgSem σ head (.data hd) hd_t hd_s) (h₂ : ProgSem σ tail (.data tl) tl_t tl_s) :
+      ProgSem σ (.cons head tail) (.data (Data.l (hd :: tl.asList))) (hd_t + tl_t) (hd_s + tl_s)
+  /-- `elim`, empty branch: `v` is the empty list, so run `emp` in the current environment. -/
+  | elim_nil
+      (h₁ : ProgSem σ val (.data (Data.l [])) t_v s_v)
+      (h₂ : ProgSem σ emp r t_emp s_emp) :
+      ProgSem σ (.elim val emp cs) r (t_v + t_emp) (s_v + s_emp)
+  /-- `elim`, cons branch: `v` destructures to `hd :: tl`; evaluate the function `cs` to a
+      closure and apply it first to `hd` and then to `tl` (so `cs` is a curried
+      two-argument function). -/
+  | elim_cons
+      (h_v : ProgSem σ val (.data (Data.l (hd :: tl))) t_v s_v)
+      (h_cs : ProgSem σ cs cv t_cs s_cs)
+      (h_app₁ : AppSem cv (.data hd) cv' t₁ s₁)
+      (h_app₂ : AppSem cv' (.data (Data.l tl)) r t₂ s₂) :
+      ProgSem σ (.elim val emp cs) r (t_v + t_cs + t₁ + t₂) (s_v + s_cs + s₁ + s₂)
+  | ifEq_then
+      (h_x : ProgSem σ x (.data vx) t_x s_x)
+      (h_y : ProgSem σ y (.data vx) t_y s_y)
+      (h_then : ProgSem σ then_ r t_then s_then) :
+      ProgSem σ (.ifEq x y then_ else_) r (t_x + t_y + t_then) (s_x + s_y + s_then)
+  | ifEq_else
+      (h_x : ProgSem σ x (.data vx) t_x s_x)
+      (h_y : ProgSem σ y (.data vy) t_y s_y)
+      (h_neq : vx ≠ vy)
+      (h_else : ProgSem σ else_ r t_else s_else) :
+      ProgSem σ (.ifEq x y then_ else_) r (t_x + t_y + t_else) (s_x + s_y + s_else)
+  /-- `while_ init body`: evaluate `init` to the starting accumulator and `body` to a
+      one-argument closure, then iterate the closure via `WhileSem` until it halts. -/
+  | while_
+      (h_init : ProgSem σ init (.data acc) t_init s_init)
+      (h_body : ProgSem σ body bodyVal t_body s_body)
+      (h_while : WhileSem bodyVal acc r t_w s_w) :
+      ProgSem σ (.while_ init body) (.data r) (t_init + t_body + t_w) (s_init + s_body + s_w)
+  /-- `fn body`: evaluate to a closure capturing the current environment `σ`. The cost is the
+      size of the resulting closure (mirroring `var`, which charges the size of the value it
+      produces). -/
+  | fn : ProgSem σ (.fn body) (.closure body σ)
+        (Value.closure body σ).size (Value.closure body σ).size
+  /-- `app fn arg`: evaluate `fn` to a closure, evaluate `arg` to a value, then run the
+      closure's body in the *captured* environment extended with the argument (static
+      scoping). -/
+  | app
+      (h_fn : ProgSem σ fn fv t_f s_f)
+      (h_arg : ProgSem σ arg v t_a s_a)
+      (h_app : AppSem fv v r t_b s_b) :
+      ProgSem σ (.app fn arg) r (t_f + t_a + t_b) (s_f + s_a + s_b)
+
+/-- Application of a value to an argument value. `AppSem f v r t s` means that applying the
+closure `f` to the argument `v` yields `r` using `t` time and `s` space. Only closures can be
+applied; applying a first-order value has no derivation (the program is stuck). -/
+inductive AppSem : Value → Value → Value → ℕ → ℕ → Prop
+  | mk (h_body : ProgSem (σ ++ [v]) body r t s) :
+      AppSem (.closure body σ) v r t s
+
+/-- Iterates the closure `bodyVal` of a `while_` loop, threading the accumulator.
+`WhileSem bodyVal acc r t s` means that, starting from accumulator `acc`, repeatedly applying
+`bodyVal` to the current accumulator eventually yields result `r` using `t` time and `s` space.
+Before each iteration the halting condition is checked on the current accumulator: iteration
+terminates (with the accumulator as result) when `acc` is empty or its head is empty.
+Otherwise `bodyVal` is applied and its result becomes the new accumulator. Non-terminating
+loops simply have no derivation. -/
+inductive WhileSem : Value → Data → Data → ℕ → ℕ → Prop
+  | halt
+      (h_stop : acc.asList.head?.getD (Data.l []) = Data.l []) :
+      WhileSem bodyVal acc acc acc.size acc.size
+  | step
+      (h_cont : acc.asList.head?.getD (Data.l []) ≠ Data.l [])
+      (h_app : AppSem bodyVal (.data acc) (.data v) t_b s_b)
+      (h_rest : WhileSem bodyVal v r t_r s_r) :
+      WhileSem bodyVal acc r (t_b + t_r) (max s_b s_r)
+end
+
+/-- Producing a value costs at least its size, in both time and space. This holds because every
+`ProgSem` derivation either reads/builds the value directly (charging its size) or returns a
+value produced by a sub-derivation whose cost it includes. Provable by mutual induction over
+`ProgSem`/`AppSem`/`WhileSem`. -/
+lemma ProgSem.size_le {σ : List Value} {p : Prog} {v : Value} {t s : ℕ}
+    (h : ProgSem σ p v t s) : v.size ≤ t ∧ v.size ≤ s := by
+  induction h using ProgSem.rec
+    (motive_2 := fun _ _ r t s _ => r.size ≤ t ∧ r.size ≤ s)
+    (motive_3 := fun _ _ r t s _ => (Value.data r).size ≤ t ∧ (Value.data r).size ≤ s) with
+  | empty => exact ⟨by simp, by simp⟩
+  | var | cons | elim_nil | elim_cons | ifEq_then | ifEq_else
+  | while_ | fn | app  | mk | halt | step
+    => grind [Value.size_data, Data.cons_size, Data.asList_l]
+
+/-- Value-determinism of the relational semantics: a program evaluates to at most one value in a
+given environment. The mutually-defined `AppSem`/`WhileSem` relations are value-deterministic too.
+The potential branch overlaps (`elim_nil`/`elim_cons`, `ifEq_then`/`ifEq_else`) are ruled out by
+value-determinism of the scrutinee / compared values, supplied by the induction hypotheses. -/
+theorem ProgSem.value_det {σ : List Value} {p : Prog} {v₁ : Value} {t₁ s₁ : ℕ}
+    (h₁ : ProgSem σ p v₁ t₁ s₁) :
+    ∀ (v₂ : Value) (t₂ s₂ : ℕ), ProgSem σ p v₂ t₂ s₂ → v₁ = v₂ := by
+  induction h₁ using ProgSem.rec
+    (motive_2 := fun f a r₁ _ _ _ =>
+      ∀ (r₂ : Value) (t₂ s₂ : ℕ), AppSem f a r₂ t₂ s₂ → r₁ = r₂)
+    (motive_3 := fun b acc r₁ _ _ _ =>
+      ∀ (r₂ : Data) (t₂ s₂ : ℕ), WhileSem b acc r₂ t₂ s₂ → r₁ = r₂) with
+  | var | empty | fn => rintro _ _ _ h₂; cases h₂; rfl
+  | cons _ _ ih₁ ih₂ =>
+    rintro _ _ _ h₂; cases h₂ with
+    | cons h₁' h₂' => have := ih₁ _ _ _ h₁'; have := ih₂ _ _ _ h₂'; grind
+  | elim_nil _ _ ih_v _ =>
+    rintro _ _ _ h₂; cases h₂ with
+    | elim_nil h_v' _ => grind
+    | elim_cons h_v' _ _ _ => have := ih_v _ _ _ h_v'; grind
+  | elim_cons _ _ _ _ ih_v ih_cs ih₁ ih₂ =>
+    rintro _ _ _ h₂; cases h₂ with
+    | elim_nil h_v' _ => have := ih_v _ _ _ h_v'; grind
+    | elim_cons h_v' h_cs' h_a₁' h_a₂' =>
+      have := ih_v _ _ _ h_v'; have := ih_cs _ _ _ h_cs'
+      grind
+  | ifEq_then _ _ _ ih_x ih_y ih_then =>
+    rintro _ _ _ h₂; cases h₂ with
+    | ifEq_then h_x' _ h_then' => have := ih_then _ _ _ h_then'; grind
+    | ifEq_else h_x' h_y' h_neq _ =>
+      have := ih_x _ _ _ h_x'; have := ih_y _ _ _ h_y'; grind
+  | ifEq_else _ _ _ _ ih_x ih_y ih_else =>
+    rintro _ _ _ h₂; cases h₂ with
+    | ifEq_then h_x' h_y' _ => have := ih_x _ _ _ h_x'; have := ih_y _ _ _ h_y'; grind
+    | ifEq_else _ _ _ h_else' => have := ih_else _ _ _ h_else'; grind
+  | while_ _ _ _ ih_init ih_body ih_while =>
+    rintro _ _ _ h₂; cases h₂ with
+    | while_ h_init' h_body' h_while' =>
+      have := ih_init _ _ _ h_init'; have := ih_body _ _ _ h_body'; grind
+  | app _ _ _ ih_fn ih_arg ih_app =>
+    rintro _ _ _ h₂; cases h₂ with
+    | app h_fn' h_arg' h_app' =>
+      have := ih_fn _ _ _ h_fn'; have := ih_arg _ _ _ h_arg'; grind
+  | mk _ ih_body =>
+    rename_i h₂; cases h₂ with
+    | mk h_body' => exact ih_body _ _ _ h_body'
+  | halt _
+  | step _ _ _ ih_app ih_rest =>
+    rename_i h₂; cases h₂ with
+    | halt h_stop => grind
+    | step _ h_app' h_rest' => grind
+
+/-- The program `p` computes the value `y` from the value `x` in time `t` and space `s`. -/
+def Prog.ComputesInTimeAndSpace (p : Prog) (x y : Data) (t : ℕ) (s : ℕ) : Prop :=
+  ProgSem [.data x] p (.data y) t s
+
+
+/-- The program `p` computes the function `f` (on binary strings) in time `t` and space `s`.
+This is the main definition that defines complexity for this computation model. -/
+def Prog.ComputesBoolFunInTimeAndSpace
+  (p : Prog) (f : List Bool → List Bool) (t : ℕ → ℕ) (s : ℕ → ℕ) : Prop :=
+  ∀ x, ∃ t' ≤ t x.length, ∃ s' ≤ s x.length,
+  Prog.ComputesInTimeAndSpace p (DataEncode.encode x) (DataEncode.encode (f x)) t' s'
+
+/-- The function `f` is computable in time `t` in the RTM model, up to constant factors -/
+def ComputableInOTime (f : List Bool → List Bool) (t : ℕ → ℕ) : Prop :=
+  ∃ p a s, Prog.ComputesBoolFunInTimeAndSpace p f (fun n => a * (t n) + a) s
+
+/-- The function `f` is computable in space `s` in the RTM model, up to constant factors -/
+def ComputableInOSpace (f : List Bool → List Bool) (s : ℕ → ℕ) : Prop :=
+  ∃ p a t, Prog.ComputesBoolFunInTimeAndSpace p f t (fun n => a * (s n) + a)
+
+/-- The *in-place* (first-order) fragment of the functional language.
+
+`InPlace p` holds when every `fn` in `p` occurs in an immediately-consumed position — as the
+operator of an `app`, or as the (curried) branch of an `elim`/`while_`. Consequently no
+closure ever escapes: every abstraction is created and used on the spot, so all values that
+flow through the environment are first-order `Data`. This is exactly the fragment a
+defunctionalising compiler targets, and it is closed under the operational semantics.
+
+A Turing machine can directly implement this fragment without the need for closures:
+One tape is used for each "node" in the syntax tree.
+-/
+inductive InPlace : Prog → Prop
+  | var : InPlace (.var i)
+  | empty : InPlace .empty
+  | cons (hh : InPlace h) (ht : InPlace t) : InPlace (.cons h t)
+  /-- `elim` over an in-place value, empty branch, and a curried two-argument function
+      branch `fn (fn body)` binding `head` and `tail`. -/
+  | elim (hv : InPlace v) (hemp : InPlace emp) (hbody : InPlace body) :
+      InPlace (.elim v emp (.fn (.fn body)))
+  | ifEq (hx : InPlace x) (hy : InPlace y) (hthen : InPlace then_) (helse : InPlace else_) :
+      InPlace (.ifEq x y then_ else_)
+  /-- `while_` whose body is a literal one-argument function `fn body` binding the
+      accumulator. -/
+  | while_ (hinit : InPlace init) (hbody : InPlace body) :
+      InPlace (.while_ init (.fn body))
+  /-- `app` whose operator is a literal one-argument function `fn body`: this is a `let`,
+      binding the value of `arg` and running `body` on the spot. The abstraction is consumed
+      immediately, so no closure escapes. Nested applications of this form give multi-argument
+      `let`-chains; arbitrary arities follow by repeated use of this constructor. -/
+  | app (hbody : InPlace body) (harg : InPlace arg) :
+      InPlace (.app (.fn body) arg)
+
+
+end RoseTreeMachine
+
+end Complexity
diff --git a/ROADMAP.md b/ROADMAP.md
index 214fa757..8189a7e5 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -153,6 +153,26 @@ another controller-local proof.
     deferred and optional, not implemented. It is not a dependency of the
     named-tape/effect work; revisit only when a real construction needs recursive
     Data-valued syntax and the bounded slice can meet all promotion gates.
+  - [ ] Compile the `InPlace` (first-order) RTM fragment to Turing machines with
+    resource consumption matching the `ProgSem` cost model up to a constant
+    factor. `Complexitylib.Models.RoseTreeMachine.Compile` lands the first
+    verified slice: the public `inPlace_compilesToTM` theorem statement (single
+    input/output, subroutine-ready), the internal layout-relative contract
+    `CompilesUnder` / `LoadedStart` (one work tape per program argument via
+    `slot : Fin m → Fin k`) with its recursion `compilesUnder_of_inPlace`, the
+    `Data.toBits` balanced-parenthesis tape serialization (length `= Data.size`),
+    the `InPlaceRealizedByTM` correspondence predicate, the linear
+    `Data`-encoding-size bridge (`dataSize_encode_listBool`), and two proven base
+    cases — `empty` (matching time *and* space via `emptyOutputTM`) and
+    `var 0`/identity (matching time via `copyInputToOutputTM`). The two headline
+    statements are `sorry` for now. The inductive constructors (`cons`, `elim`,
+    `ifEq`, `while_`, and the immediately consumed `app`/`fn` let-binding) need
+    concrete `Data`-manipulation subroutines and remain to be composed through
+    the `CompilesUnder` interface. The compiler recursion is fully decomposed:
+    `compilesUnder_of_inPlace` assembles the per-constructor parts
+    (`compiled_var`/`compiled_empty`/`compiled_cons`/`compiled_elim`/
+    `compiled_ifEq`/`compiled_while`/`compiled_app`) by induction with no
+    `sorry`; the parts themselves are the remaining obligations.
 - [x] Audit proof-engineering mechanics across representative machine and circuit
   constructions: inventory repeated state/tape/wire bookkeeping, run or trace
   stitching, semantic transport, and resource accounting, then prototype the
diff --git a/RTM_to_TM.lean b/RTM_to_TM.lean
new file mode 100644
index 00000000..cee4d48c
--- /dev/null
+++ b/RTM_to_TM.lean
@@ -0,0 +1,123 @@
+/--
+
+Sketch of how to simulate an RTM with a TM.
+
+First we describe how to simulate the RTM with a multi-tape TM.
+
+From each Prog, we can determine a number of tapes required:
+
+def tape_count (p : Prog) : ℕ :=
+  match p with
+  | .var _ => 1
+  | .letin val rest => 1 + tape_count val + tape_count rest
+  | .empty => 1
+  | .cons h t => 1 + tape_count h + tape_count t
+  | .elim v em cs => 5 + tape_count v + tape_count em + tape_count cs
+  | .eq a b => 1 + tape_count a + tape_count b
+  | .fold body init list => 5 + tape_count body + tape_count init + tape_count list
+  | .while_ init body => 5 + tape_count init + tape_count body
+
+From these tape counts, we can allocate distinct tapes for each Prog. Each prog has a designated
+output tape and potentially some helper tapes. We also maintain a mapping from
+variable indices to tapes.
+
+This is how we simulate. Whenever we write to a tape, we first clear it, because it might
+still contain data from previous loop iterations.
+
+var : copy from the tape of the variable to the output tape of the Prog. This should take linear time in the size of the copied data and also linear space in that.
+
+letin : simulate 'val'. add a new variable to the environment and let it point at the output
+  tape of 'val'. Then simulate 'rest'. Copy its output to the output tape.
+
+empty: write '(', ')' to the output tape.
+
+cons: simulate h and t. write '(' to the output tape, then copy the contents of the output tape
+of h, then copy the contents of the output tape of t (but ignore the first symbol).
+
+elim: simulate v. check if the output take is exactly "()". If yes, simulate em and copy its
+output to the output tape of elim. Otherwise, use three auxiliary tapes: We nede to copy
+the head and the tail of the output tape of v to two separate tapes. For that, we need to
+analyze the parentheses-nesting structure. Prepare an auxiliary tape to count the current nesting
+level in unary (you can put single '(' that do not match a closing one). skip the first '(' on
+the output tape of v. Then do the following in a loop: copy the current symbol to the head auxiliary tape
+and update the nesting level (add a '(' for '(', remove a '(' for ')'). If the nesting level reaches 0 (the tape head on the nesting level tape reads "empty"), we are at the end of the head, so we switch to copying to the tail auxiliary tape: put a `(` on hte tail auxiliary tape and copy over the rest of the 'v' autput tape. After this, we have the head and tail on separate tapes, so we can simulate cs with these tapes added to the variable mapping. After rest terminates, copy its output tape to the outpuut tape of elim.
+
+eq : simulate a and b. We compare the tape contents by moving over them in parallel. If we find a mismatch, write (()), otherwise write () to the output tape.
+
+fold: simulate init and list. We maintain an auxiliary tape for the accumulator, which we initialize with the output of init. We also maintain an auxiliary tape for the current element of the list. TODO
+
+Then we can simulate each Prog on the TM by using the tapes to store the environment and intermediate results. The TM will have a fixed number of tapes equal to the maximum number of tapes needed for any Prog we want to simulate.
+
+Finally, we can use the fact that multi-tape TMs can be simulated by single-tape TMs with only a polynomial slowdown, to conclude that we can simulate the RTM with a single-tape TM.
+
+-/
+inductive Prog where
+  | var (id : Var)
+  /-- `letin val rest`: evaluate `val`, append the result to `env`, then evaluate `rest`. -/
+  | letin (val : Prog) (rest : Prog)
+  | empty
+  | cons (h t : Prog)
+  /-- `elim v em cs`: if `v` evaluates to `empty`, run `em`; otherwise destructure into
+      `head` and `tail` (both appended to `env`, in that order) and run `cs`. -/
+  | elim (v : Prog) (em : Prog) (cs : Prog)
+  | eq (a b : Prog)
+  /-- `fold body init list`: `init` and `list` produce starting accumulator and the input
+      list; `body` runs once per element with `env` extended by `[acc, x]`. -/
+  | fold (body : Prog) (init list : Prog)
+  /-- `while_ init body`: `init` produces the starting accumulator; `body` runs with
+      `env` extended by the current accumulator. -/
+  | while_ (init body : Prog)
+deriving Repr
+
+/-- Evaluates `p` on `env` and returns the result, the time and the space consumption. -/
+def Prog.meteredEval (env : List Data) (p : Prog) : Part (Data × ℕ × ℕ) :=
+  match p with
+    -- TODO charge for copy?
+  | .var id => .some (env[(show ℕ from id)]?.getD (Data.l []), 1, 1)
+  | .letin val rest => do
+    let (v, t, s) ← val.meteredEval env
+    let (r, t', s') ← rest.meteredEval (env ++ [v])
+    -- TODO charge for copy?
+    return (r, 1 + t + t', max s s')
+  | .empty => .some (Data.empty, 1, 1)
+  | .cons h t => do
+    let (head, h_t, h_s) ← h.meteredEval env
+    let (tail, t_t, t_s) ← t.meteredEval env
+    return (Data.l (head :: tail.asList), 1 + h_t + t_t, max h_s t_s)
+  | .elim v em cs => do
+    let (v', t, s) ← v.meteredEval env
+    match v' with
+    | Data.l [] =>
+      let (r, t', s') ← em.meteredEval env
+      return (r, 1 + t + t', max s s')
+    | Data.l (head :: tail) =>
+      let (r, t', s') ← cs.meteredEval (env ++ [head, Data.l tail])
+      return (r, 1 + t + t', max s s')
+  | .eq a b => do
+    let (a, a_t, a_s) ← a.meteredEval env
+    let (b, b_t, b_s) ← b.meteredEval env
+    (if a == b then Data.l [ Data.l [] ] else Data.l [], 1 + a_t + b_t, 1 + max a_s b_s)
+  | .fold body init list => do
+    let (i, i_t, i_s) ← init.meteredEval env
+    let (l, l_t, l_s) ← list.meteredEval env
+    l.asList.foldlM
+      (fun (acc, t, s) el => do
+        let (acc', b_t, b_s) ← body.meteredEval (env ++ [acc, el])
+        return (acc', 1 + t + b_t, max s b_s))
+      (i, 1 + i_t + l_t, max i_s l_s)
+  | .while_ init body => do
+    let (i, i_t, i_s) ← init.meteredEval env
+    -- Real while loop: check the halt condition on the current accumulator first.
+    -- If `acc.asList.headD = []` (empty head), halt and return `acc`.
+    -- Otherwise run `body` on the accumulator and loop with its result.
+    let F : ((Data × ℕ × ℕ) → Part (Data × ℕ × ℕ)) →
+            (Data × ℕ × ℕ) → Part (Data × ℕ × ℕ) :=
+      fun rec d_ts =>
+        let (acc, t, s) := d_ts
+        if acc.asList.headD (Data.l []) = Data.l [] then
+          .some (acc, t, s)
+        else
+          (body.meteredEval (env ++ [acc])).bind fun (r, b_t, b_s) =>
+            rec (r, t + 1 + b_t, max s b_s)
+    Part.fix F (i, 1 + i_t, max 1 i_s)
+  termination_by (sizeOf p, 0)