From 5bc455a4a645fa6e9dee6a89a28bab4b59adc003 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 3 Aug 2026 12:09:35 +0200
Subject: [PATCH 1/6] Prove an exponential upper bound in the number of
 configurations reachable in bounded space.

---
 Cslib.lean                                    |   1 +
 .../Turing/MultiTape/ConfigBound.lean         | 329 ++++++++++++++++++
 2 files changed, 330 insertions(+)
 create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean

diff --git a/Cslib.lean b/Cslib.lean
index e188de56d..41c0e3245 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -40,6 +40,7 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
new file mode 100644
index 000000000..0379492fe
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -0,0 +1,329 @@
+/-
+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.Turing.MultiTape.TapeLemmas
+public import Mathlib.Data.Fintype.BigOperators
+public import Mathlib.Data.Fintype.Pi
+public import Mathlib.Data.Fintype.Prod
+public import Mathlib.Data.Fintype.Option
+public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
+
+/-!
+# Bounds on the number of reachable configurations in bounded space
+
+For a deterministic multi-tape Turing machine that uses at most `s` cells of work-tape space, the
+number of distinct configurations it can be in is at most exponential in `s`.
+
+The configuration type `Cfg` is split into the input head position and the *storage* part
+(`Storage`), i.e. the state, the work tape contents and head positions. This split can be used
+to show the collapse of small space-bounded classes.
+
+
+## Important Definitions
+
+The key lemmas in this file are:
+
+* `MultiTapeTM.card_storages_le` bounds the number of *storage configurations* only, disregarding
+  the input head position. The function used for the bound is `storageBound Symbol State k s`.
+* `MultiTapeTM.card_configs_le` additionally tracks the input head position, giving the bound
+  `(n + 2) * storageBound Symbol State k s` on the number of full configurations of an input of
+  length `n`.
+* `MultiTapeTM.card_configs_le_pow` restates the previous bound as `(n + 2) * a * 2 ^ (c * s)`
+  for constants `a` and `c` depending only on the machine, so it can be used to time-bound
+  space-bounded machines.
+
+## Design
+
+Starting from the all-blank tapes with every head at `0` and moving by at most one cell per step,
+a computation in which tape `i` has visited at most `sᵢ` cells keeps that tape's head position and
+every non-blank cell within the per-tape window `[-sᵢ, sᵢ]`.
+
+Hence a storage configuration is determined by finite data over these windows, and counting it
+gives the per-tape product `∏ᵢ (2 sᵢ + 1) · (|Symbol| + 1)^(2 sᵢ + 1)`. Since the tapes share the
+total space budget (`∑ᵢ sᵢ ≤ s`), this collapses to an expression with the *total* space
+(`2s + k`) as the alphabet exponent. The full-configuration bound needed for time-bounding
+space-bounded machines then follows by pairing the storage count with the `(n + 2)` possible
+input-head positions.
+
+We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used
+area, but this is absorbed by the `O(s)` exponent in the final bound. The `+ 2` in `(n + 2)` is
+needed because the input head is allowed to move one step off the input in either direction by
+the model.
+-/
+
+@[expose] public section
+
+open Cslib
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ}
+variable {State Symbol : Type*}
+variable {input : List Symbol}
+variable {tm : MultiTapeTM k Symbol State}
+
+/-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed
+by an arbitrary type `ι i`. If you add the input tape position and use `ι i = ℤ`, this is equivalent
+to `Cfg` (cf. `Cfg.storage`).
+The index set is useful for cardinality arguments if we have a bound on the tape cells that
+are actually used.
+The input head position is not included because this is useful for arguments below logarithmic
+space. -/
+@[ext]
+structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where
+  /-- the state of the TM (cf. `Cfg.state`) -/
+  state : Option State
+  /-- the contents of work tape `i` (cf. `Cfg.workTapes`) -/
+  workTapes (i : Fin k) : ι i → Option Symbol
+  /-- the position of the head on work tape `i` (cf. `Cfg.workTapePos`) -/
+  workTapePos (i : Fin k) : ι i
+
+/-- A `Storage` is just a product of its fields; this equivalence is used for counting. -/
+def Storage.equivProd (Symbol State : Type*) (ι : Fin k → Type*) :
+    Storage Symbol State ι ≃
+      Option State × ((i : Fin k) → ι i → Option Symbol) × ((i : Fin k) → ι i) where
+  toFun x := (x.state, x.workTapes, x.workTapePos)
+  invFun := fun ⟨state, workTapes, workTapePos⟩ => ⟨state, workTapes, workTapePos⟩
+
+instance (Symbol State : Type*) [Fintype Symbol] [Fintype State]
+    (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] :
+    Fintype (Storage Symbol State ι) :=
+  Fintype.ofEquiv _ (Storage.equivProd Symbol State ι).symm
+
+/-- A `Storage` over the unrestricted index type `ℤ` for every tape, as extracted from a full
+configuration by `Cfg.storage`. -/
+abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) :=
+  Storage Symbol State (fun _ : Fin k => ℤ)
+
+/-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/
+def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k :=
+  ⟨c.state, c.workTapes, c.workTapePos⟩
+
+/-- For a fixed input, a configuration is fully determined by its input-head position together with
+its `storage`. Hence counting distinct configurations reduces to counting `(inputPos, storage)`
+pairs. -/
+lemma inputPos_storage_injective (input : List Symbol) :
+    Function.Injective (fun c : Cfg k Symbol State input => (c.inputPos.val, c.storage)) := by
+  intro c₁ c₂ h
+  simp only [Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
+  obtain ⟨hip, hstate, hwt, hwp⟩ := h
+  exact Cfg.ext hstate (Fin.ext hip) hwt hwp
+
+/-- The window `[-s, s]` of tape positions allotted to a tape that uses `s` cells. -/
+def Storage.window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
+
+@[scoped grind =]
+lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ Storage.window s ↔ z.natAbs ≤ s := by
+  grind [Storage.window]
+
+@[simp]
+lemma Storage.card_window (s : ℕ) : (Storage.window s).card = 2 * s + 1 := by
+  grind [Storage.window, Int.card_Icc]
+
+/-- A bounded storage configuration: a `Storage` whose tape `i` is restricted to the finite window
+`[-(w i), w i]`. Storage configurations of a computation that visits at most the window of each
+tape embed injectively into this finite type (`Storage.toBounded`), so its cardinality bounds the
+number of reachable storage configurations. -/
+abbrev BoundedStorage (Symbol State : Type*) {k : ℕ} (w : Fin k → ℕ) :=
+  Storage Symbol State (fun i => Storage.window (w i))
+
+/-- A storage fits in the per-tape windows `w`: on each tape `j`, the head position and every
+non-blank cell have absolute value `≤ w j`. -/
+structure Storage.FitsIn (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) : Prop where
+  /-- the head position on every tape lies within its window -/
+  pos_le : ∀ j, (x.workTapePos j).natAbs ≤ w j
+  /-- every non-blank cell on every tape lies within its window -/
+  cell_le : ∀ j z, x.workTapes j z ≠ none → z.natAbs ≤ w j
+
+/-- If an `UnboundedStorage` fits in a smaller window, it also fits in the larger window. -/
+lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.FitsIn := by
+  intro w₁ w₂ h_le h_fits
+  refine ⟨?_, ?_⟩
+  · intro j
+    grind [h_fits.pos_le j, h_le j]
+  · intro j z h_ne
+    grind [h_fits.cell_le j z h_ne, h_le j]
+
+/-- Restriction of a storage over `ℤ` to the finite windows `w` (with heads outside their window
+clamped to `0`). -/
+def Storage.toBounded (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) :
+    BoundedStorage Symbol State w where
+  state := x.state
+  workTapes j z := x.workTapes j z.1
+  workTapePos j :=
+    if h : x.workTapePos j ∈ Storage.window (w j) then ⟨x.workTapePos j, h⟩
+    else ⟨0, Storage.mem_window.mpr (Nat.zero_le _)⟩
+
+/-- The restriction is injective on storages that fit in the windows. -/
+lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
+    Set.InjOn (Storage.toBounded (Symbol := Symbol) (State := State) · w) {x | x.FitsIn w} := by
+  rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
+  simp only [Storage.toBounded, Storage.mk.injEq] at hxy
+  obtain ⟨hstate, htapes, hpos⟩ := hxy
+  refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
+  · by_cases hz : z ∈ Storage.window (w j)
+    · exact congrFun (congrFun htapes j) ⟨z, hz⟩
+    · grind
+  · have := congrFun hpos j
+    grind [Subtype.ext_iff]
+
+/-- The number of storages over finite position types is the per-tape product of
+"cell contents × head position" counts. -/
+lemma card_storage [Fintype Symbol] [Fintype State]
+    (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] :
+    Fintype.card (Storage Symbol State ι)
+      = (Fintype.card State + 1)
+        * ∏ i, Fintype.card (ι i) * (Fintype.card Symbol + 1) ^ Fintype.card (ι i) := by
+  rw [Fintype.card_congr (Storage.equivProd Symbol State ι)]
+  simp only [Fintype.card_prod, Fintype.card_option, Fintype.card_pi, Finset.prod_const,
+    Finset.card_univ, Finset.prod_mul_distrib]
+  ring
+
+/-- An upper bound on the number of storage configurations a `k`-tape machine can be in while using
+at most `s` cells of total work-tape space, over the given alphabet and state set. The `(2s + 1)^k`
+factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(2s + k)` uses the
+*total* space `s` in the exponent (the `k` tapes share the space budget), matching the textbook
+`|State| · |Symbol|^{O(s)} · poly(s)` count. -/
+def storageBound (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ :=
+  (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k))
+
+/-- `storageBound` grows at most exponentially in the space `s`: there exist constants `a` and `c`
+(depending on the machine's alphabet, state set and tape count) with
+`storageBound Symbol State k s ≤ a * 2 ^ (c * s)` for all `s`. -/
+lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
+    ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) := by
+  set syms := Fintype.card Symbol + 1 with hB
+  set states := Fintype.card State + 1 with hQ
+  -- The strategy is to bound each factor of `storageBound` by a power of `2`, using `B ≤ 2 ^ B`
+  -- and `2 * s + 1 ≤ 2 ^ (s + 1)`. Collecting the exponents then yields
+  -- `(s + 1) * k + B * (2 * s + k)`, which splits into the constant part `B * k + k`
+  -- (absorbed into `a`) and the part `(2 * B + k) * s` linear in `s` (which is `c * s`).
+  refine ⟨states * 2 ^ (syms * k + k), 2 * syms + k, fun s => ?_⟩
+  have hB2 : syms ≤ 2 ^ syms := Nat.lt_two_pow_self.le
+  have h2s1 : 2 * s + 1 ≤ 2 ^ (s + 1) := by grind [pow_succ, Nat.lt_two_pow_self]
+  calc storageBound Symbol State k s
+      = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl
+    _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by
+        gcongr <;> exact Nat.zero_le _
+    _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by rw [← pow_mul, ← pow_mul, ← pow_add]
+    _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf
+    _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by rw [pow_add, mul_assoc]
+
+/-- The per-tape product is bounded by `storageBound`: each tape uses at most the total space `s`,
+and the tapes together use at most `s`, which collapses the alphabet exponent to `2s + k`. -/
+lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
+    (w : Fin k → ℕ) (s : ℕ) (hsum : ∑ i, w i ≤ s) :
+    Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s := by
+  have hle : ∀ i, w i ≤ s := fun i =>
+    (Finset.single_le_sum (fun i _ => Nat.zero_le (w i)) (Finset.mem_univ i)).trans hsum
+  simp only [card_storage, storageBound, Fintype.card_coe, Storage.card_window]
+  rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum]
+  have hsc : ∑ i : Fin k, (2 * w i + 1) = 2 * (∑ i, w i) + k := by
+    simp [two_mul, Finset.sum_add_distrib]
+  gcongr
+  · simpa using Finset.prod_le_pow_card Finset.univ (fun i => 2 * w i + 1) (2 * s + 1)
+      fun i _ => by have := hle i; omega
+  · omega
+  · omega
+
+/-- The storage of any configuration reached within `T` steps fits in the windows given by the
+per-tape space usage up to step `T`. -/
+lemma storage_fitsIn
+    (T : ℕ)
+    {t : ℕ}
+    (ht : t ≤ T) :
+    (tm.configs (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) T) := by
+  -- The bounds at step `t` extend to the window at step `T ≥ t` by monotonicity of space usage.
+  apply Storage.FitsIn_mono (fun j => tm.spaceUsedByTape_mono _ j ht)
+  refine ⟨?_, ?_⟩
+  · intro j
+    simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
+      (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)
+  · intro j
+    exact content_natAbs_le_spaceUsedByTape t
+
+
+open scoped Classical in
+/-- For any multi-tape Turing machine that uses at most space `s` up to step `t`, the number
+of storage configurations (configurations disregarding the input head positions) up to step `t`
+is at most `storageBound Symbol State k s` (independent of `t`). -/
+theorem card_storages_le
+    [Fintype Symbol] [Fintype State]
+    (t s : ℕ)
+    (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) :
+    ((Finset.range (t + 1)).image (fun t' => (tm.configs (tm.initCfg input) t').storage)).card
+    ≤ storageBound Symbol State k s := by
+  set space := tm.spaceUsedByTape (tm.initCfg input) t
+  calc ((Finset.range (t + 1)).image
+          (fun t' => (tm.configs (tm.initCfg input) t').storage)).card
+      ≤ Fintype.card (BoundedStorage Symbol State space) := by
+        rw [← Finset.card_univ]
+        refine Finset.card_le_card_of_injOn (Storage.toBounded · space) (by simp) ?_
+        refine Set.InjOn.mono ?_ (Storage.toBounded_injOn space)
+        intro x hx
+        simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Finset.mem_range] at hx
+        obtain ⟨t', ht, rfl⟩ := hx
+        exact storage_fitsIn t (by omega)
+    _ ≤ storageBound Symbol State k s := card_boundedStorage_le space s hs
+
+
+open scoped Classical in
+/-- The number of distinct configurations a multi-tape Turing machine with space bound `s`
+can reach is at most `(n + 2) * storageBound Symbol State k s`, where `n` is the input length.
+The `(n + 2)` factor accounts for the input-head position; the `storageBound` factor accounts for
+everything else (`storage`). -/
+theorem card_configs_le
+    [Fintype Symbol] [Fintype State]
+    (t s : ℕ)
+    (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) :
+    ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
+      ≤ (input.length + 2) * storageBound Symbol State k s := by
+  -- Counting configurations reduces to counting `(inputPos, storage)` pairs, since the map to such
+  -- pairs is injective for a fixed input.
+  rw [← Finset.card_image_of_injective _ (inputPos_storage_injective input), Finset.image_image]
+  -- The pair image lies in the product of the input-head range with the storage image, so its
+  -- cardinality is bounded by `(n + 2)` times the storage count from `card_storages_le`.
+  calc ((Finset.range (t + 1)).image (fun t' =>
+          ((tm.configs (tm.initCfg input) t').inputPos.val,
+           (tm.configs (tm.initCfg input) t').storage))).card
+      ≤ (Finset.range (input.length + 2) ×ˢ (Finset.range (t + 1)).image
+          (fun t' => (tm.configs (tm.initCfg input) t').storage)).card := by
+        apply Finset.card_le_card
+        intro x hx
+        simp only [Finset.mem_image, Finset.mem_range] at hx
+        obtain ⟨t, ht, rfl⟩ := hx
+        simp only [Finset.mem_product, Finset.mem_range, Finset.mem_image]
+        exact ⟨(tm.configs (tm.initCfg input) t).inputPos.isLt, t, ht, rfl⟩
+    _ = (input.length + 2) * ((Finset.range (t + 1)).image
+          (fun t => (tm.configs (tm.initCfg input) t).storage)).card := by
+        rw [Finset.card_product, Finset.card_range]
+    _ ≤ (input.length + 2) * storageBound Symbol State k s :=
+        Nat.mul_le_mul_left _ (card_storages_le t s hs)
+
+open scoped Classical in
+/-- The number of distinct configurations reachable in space `s` is at most `2 ^ (O(s))`, up to the
+`(n + 2)` factor for the input-head position: there are constants `a` and `c` (depending only on
+the machine's alphabet, state set and tape count) that bound the configuration count for *every*
+input and step count. This is the form used to time-bound space-bounded machines. -/
+theorem card_configs_le_pow
+    [Finite Symbol] [Finite State] :
+    ∃ a c : ℕ, ∀ (input : List Symbol) (t s : ℕ),
+      tm.spaceUsed (tm.initCfg input) t ≤ s →
+      ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
+        ≤ (input.length + 2) * a * 2 ^ (c * s) := by
+  have : Fintype Symbol := Fintype.ofFinite Symbol
+  have : Fintype State := Fintype.ofFinite State
+  obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State)
+  refine ⟨a, c, fun input t s hs => ?_⟩
+  calc ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
+      ≤ (input.length + 2) * storageBound Symbol State k s :=
+        tm.card_configs_le t s hs
+    _ ≤ (input.length + 2) * (a * 2 ^ (c * s)) := Nat.mul_le_mul_left _ (hpow s)
+    _ = (input.length + 2) * a * 2 ^ (c * s) := by ring
+
+end Turing.MultiTapeTM

From 69b097bba3f55b61b642e42b3453cd173a325e53 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 12:27:08 +0200
Subject: [PATCH 2/6] Changes required by including the output tape in Cfg.

---
 .../Turing/MultiTape/ConfigBound.lean         | 365 ++++++++++--------
 .../Machines/Turing/MultiTape/TapeLemmas.lean |  26 ++
 2 files changed, 236 insertions(+), 155 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index 0379492fe..465a49da5 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -11,49 +11,60 @@ public import Mathlib.Data.Fintype.BigOperators
 public import Mathlib.Data.Fintype.Pi
 public import Mathlib.Data.Fintype.Prod
 public import Mathlib.Data.Fintype.Option
+public import Mathlib.Data.Set.Card
+public import Mathlib.Order.Lattice.Nat
 public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
+public import Mathlib.Tactic.Ring
 
 /-!
 # Bounds on the number of reachable configurations in bounded space
 
-For a deterministic multi-tape Turing machine that uses at most `s` cells of work-tape space, the
-number of distinct configurations it can be in is at most exponential in `s`.
-
-The configuration type `Cfg` is split into the input head position and the *storage* part
-(`Storage`), i.e. the state, the work tape contents and head positions. This split can be used
-to show the collapse of small space-bounded classes.
-
+A deterministic multi-tape Turing machine that uses at most `s` cells of work-tape space can only
+be in exponentially many (in `s`) different *storages*, i.e. states, work tape contents and work
+tape head positions. Together with the `n + 2` possible positions of the input head this bounds
+the number of configurations the machine can be in, disregarding the write-only output tape.
 
 ## Important Definitions
 
-The key lemmas in this file are:
-
-* `MultiTapeTM.card_storages_le` bounds the number of *storage configurations* only, disregarding
-  the input head position. The function used for the bound is `storageBound Symbol State k s`.
-* `MultiTapeTM.card_configs_le` additionally tracks the input head position, giving the bound
-  `(n + 2) * storageBound Symbol State k s` on the number of full configurations of an input of
-  length `n`.
-* `MultiTapeTM.card_configs_le_pow` restates the previous bound as `(n + 2) * a * 2 ^ (c * s)`
-  for constants `a` and `c` depending only on the machine, so it can be used to time-bound
-  space-bounded machines.
+The results are layered, from the purely combinatorial to the machine-specific:
+
+* `MultiTapeTM.encard_fitsIn_le` is a counting statement about the type `Storage` alone and does
+  not mention Turing machines: a memory whose non-blank cells and heads stay within per-tape
+  windows of total size `s` can hold at most `storageBound Symbol State k s` different values.
+* `MultiTapeTM.storage_fitsIn` is the geometric input: the storage reached after `t` steps stays
+  within the windows given by the space used up to step `t`.
+* `MultiTapeTM.encard_storages_le` combines the two: a machine bounded by space `s` passes through
+  at most `storageBound Symbol State k s` storages *during its whole run*, no matter how long it
+  runs and how long its input is. This is the form needed for arguments below logarithmic space,
+  where the number of storages is much smaller than the number of input head positions.
+* `MultiTapeTM.encard_cores_le` adds the input head position, giving the bound
+  `(n + 2) * storageBound Symbol State k s` on the number of reachable *cores* (`Cfg.core`,
+  a configuration without its output tape) for an input of length `n`.
+* `MultiTapeTM.storageBound_le_base_mul_pow` restates `storageBound Symbol State k s` as
+  `storageBoundBase Symbol State k * 2 ^ (storageBoundExp Symbol k * s)`, so that the bounds can
+  be used to time-bound space-bounded machines.
 
 ## Design
 
+The write-only output tape is never read by `step`, so it can be dropped: what a machine can still
+react to is its `Cfg.core`, the pair of the input head position and the `Storage`. The input head
+position, in contrast, *is* read, so it cannot be dropped and has to be counted, which is where
+the factor `n + 2` comes from (the input head may move one step off the input in either direction).
+
 Starting from the all-blank tapes with every head at `0` and moving by at most one cell per step,
 a computation in which tape `i` has visited at most `sᵢ` cells keeps that tape's head position and
 every non-blank cell within the per-tape window `[-sᵢ, sᵢ]`.
 
-Hence a storage configuration is determined by finite data over these windows, and counting it
-gives the per-tape product `∏ᵢ (2 sᵢ + 1) · (|Symbol| + 1)^(2 sᵢ + 1)`. Since the tapes share the
-total space budget (`∑ᵢ sᵢ ≤ s`), this collapses to an expression with the *total* space
-(`2s + k`) as the alphabet exponent. The full-configuration bound needed for time-bounding
-space-bounded machines then follows by pairing the storage count with the `(n + 2)` possible
-input-head positions.
+Hence a storage is determined by finite data over these windows, and counting it gives the
+per-tape product `∏ᵢ (2 sᵢ + 1) · (|Symbol| + 1)^(2 sᵢ + 1)`. Since the tapes share the total space
+budget (`∑ᵢ sᵢ ≤ s`), this collapses to an expression with the *total* space (`2s + k`) as the
+alphabet exponent.
 
 We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used
-area, but this is absorbed by the `O(s)` exponent in the final bound. The `+ 2` in `(n + 2)` is
-needed because the input head is allowed to move one step off the input in either direction by
-the model.
+area, but this is absorbed by the `O(s)` exponent in the final bound.
+
+The windows for a whole run are available because a machine that is space-bounded at every point in
+time attains its per-tape space usage at a single step (`MultiTapeTM.exists_spaceUsedByTape_max`).
 -/
 
 @[expose] public section
@@ -67,13 +78,15 @@ variable {State Symbol : Type*}
 variable {input : List Symbol}
 variable {tm : MultiTapeTM k Symbol State}
 
+/-! ## Storages -/
+
 /-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed
-by an arbitrary type `ι i`. If you add the input tape position and use `ι i = ℤ`, this is equivalent
-to `Cfg` (cf. `Cfg.storage`).
+by an arbitrary type `ι i`. Adding the input head position and using `ι i = ℤ` gives `Cfg.core`,
+a configuration without its write-only output tape (cf. `Cfg.storage`).
 The index set is useful for cardinality arguments if we have a bound on the tape cells that
 are actually used.
-The input head position is not included because this is useful for arguments below logarithmic
-space. -/
+The input head position is not included because leaving it out is useful for arguments below
+logarithmic space, where there are fewer storages than input head positions. -/
 @[ext]
 structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where
   /-- the state of the TM (cf. `Cfg.state`) -/
@@ -100,20 +113,6 @@ configuration by `Cfg.storage`. -/
 abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) :=
   Storage Symbol State (fun _ : Fin k => ℤ)
 
-/-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/
-def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k :=
-  ⟨c.state, c.workTapes, c.workTapePos⟩
-
-/-- For a fixed input, a configuration is fully determined by its input-head position together with
-its `storage`. Hence counting distinct configurations reduces to counting `(inputPos, storage)`
-pairs. -/
-lemma inputPos_storage_injective (input : List Symbol) :
-    Function.Injective (fun c : Cfg k Symbol State input => (c.inputPos.val, c.storage)) := by
-  intro c₁ c₂ h
-  simp only [Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
-  obtain ⟨hip, hstate, hwt, hwp⟩ := h
-  exact Cfg.ext hstate (Fin.ext hip) hwt hwp
-
 /-- The window `[-s, s]` of tape positions allotted to a tape that uses `s` cells. -/
 def Storage.window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
 
@@ -125,10 +124,10 @@ lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ Storage.window s ↔ z.natA
 lemma Storage.card_window (s : ℕ) : (Storage.window s).card = 2 * s + 1 := by
   grind [Storage.window, Int.card_Icc]
 
-/-- A bounded storage configuration: a `Storage` whose tape `i` is restricted to the finite window
-`[-(w i), w i]`. Storage configurations of a computation that visits at most the window of each
-tape embed injectively into this finite type (`Storage.toBounded`), so its cardinality bounds the
-number of reachable storage configurations. -/
+/-- A bounded storage: a `Storage` whose tape `i` is restricted to the finite window
+`[-(w i), w i]`. The storages of a computation that visits at most the window of each tape embed
+injectively into this finite type (`Storage.toBounded`), so its cardinality bounds the number of
+reachable storages. -/
 abbrev BoundedStorage (Symbol State : Type*) {k : ℕ} (w : Fin k → ℕ) :=
   Storage Symbol State (fun i => Storage.window (w i))
 
@@ -172,6 +171,12 @@ lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
   · have := congrFun hpos j
     grind [Subtype.ext_iff]
 
+/-! ## Counting storages
+
+This section is purely combinatorial: it counts how many values a `Storage` restricted to given
+windows can take, without reference to a machine or a run.
+-/
+
 /-- The number of storages over finite position types is the per-tape product of
 "cell contents × head position" counts. -/
 lemma card_storage [Fintype Symbol] [Fintype State]
@@ -184,7 +189,7 @@ lemma card_storage [Fintype Symbol] [Fintype State]
     Finset.card_univ, Finset.prod_mul_distrib]
   ring
 
-/-- An upper bound on the number of storage configurations a `k`-tape machine can be in while using
+/-- An upper bound on the number of storages a `k`-tape machine can be in while using
 at most `s` cells of total work-tape space, over the given alphabet and state set. The `(2s + 1)^k`
 factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(2s + k)` uses the
 *total* space `s` in the exponent (the `k` tapes share the space budget), matching the textbook
@@ -192,32 +197,10 @@ factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(
 def storageBound (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ :=
   (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k))
 
-/-- `storageBound` grows at most exponentially in the space `s`: there exist constants `a` and `c`
-(depending on the machine's alphabet, state set and tape count) with
-`storageBound Symbol State k s ≤ a * 2 ^ (c * s)` for all `s`. -/
-lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
-    ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) := by
-  set syms := Fintype.card Symbol + 1 with hB
-  set states := Fintype.card State + 1 with hQ
-  -- The strategy is to bound each factor of `storageBound` by a power of `2`, using `B ≤ 2 ^ B`
-  -- and `2 * s + 1 ≤ 2 ^ (s + 1)`. Collecting the exponents then yields
-  -- `(s + 1) * k + B * (2 * s + k)`, which splits into the constant part `B * k + k`
-  -- (absorbed into `a`) and the part `(2 * B + k) * s` linear in `s` (which is `c * s`).
-  refine ⟨states * 2 ^ (syms * k + k), 2 * syms + k, fun s => ?_⟩
-  have hB2 : syms ≤ 2 ^ syms := Nat.lt_two_pow_self.le
-  have h2s1 : 2 * s + 1 ≤ 2 ^ (s + 1) := by grind [pow_succ, Nat.lt_two_pow_self]
-  calc storageBound Symbol State k s
-      = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl
-    _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by
-        gcongr <;> exact Nat.zero_le _
-    _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by rw [← pow_mul, ← pow_mul, ← pow_add]
-    _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf
-    _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by rw [pow_add, mul_assoc]
-
 /-- The per-tape product is bounded by `storageBound`: each tape uses at most the total space `s`,
 and the tapes together use at most `s`, which collapses the alphabet exponent to `2s + k`. -/
 lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
-    (w : Fin k → ℕ) (s : ℕ) (hsum : ∑ i, w i ≤ s) :
+    {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i, w i ≤ s) :
     Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s := by
   have hle : ∀ i, w i ≤ s := fun i =>
     (Finset.single_le_sum (fun i _ => Nat.zero_le (w i)) (Finset.mem_univ i)).trans hsum
@@ -231,15 +214,100 @@ lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
   · omega
   · omega
 
-/-- The storage of any configuration reached within `T` steps fits in the windows given by the
-per-tape space usage up to step `T`. -/
-lemma storage_fitsIn
-    (T : ℕ)
-    {t : ℕ}
-    (ht : t ≤ T) :
-    (tm.configs (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) T) := by
-  -- The bounds at step `t` extend to the window at step `T ≥ t` by monotonicity of space usage.
-  apply Storage.FitsIn_mono (fun j => tm.spaceUsedByTape_mono _ j ht)
+/-- The counting result at the heart of this file: a `Storage` whose non-blank cells and head
+positions stay within per-tape windows of total size at most `s` can take at most
+`storageBound Symbol State k s` different values. This does not refer to a machine, a run, or an
+input; it only counts how much a memory of that shape can hold. -/
+theorem encard_fitsIn_le [Fintype Symbol] [Fintype State]
+    {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i, w i ≤ s) :
+    {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
+      ≤ storageBound Symbol State k s := by
+  calc {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
+      = ((Storage.toBounded · w) '' {x | x.FitsIn w}).encard :=
+        ((Storage.toBounded_injOn w).encard_image).symm
+    _ ≤ (Set.univ : Set (BoundedStorage Symbol State w)).encard :=
+        Set.encard_le_encard (Set.subset_univ _)
+    _ = Fintype.card (BoundedStorage Symbol State w) := by
+        simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]
+    _ ≤ storageBound Symbol State k s := by
+        exact_mod_cast card_boundedStorage_le hsum
+
+/-! ### The exponential form of `storageBound` -/
+
+/-- The constant factor in the exponential form of `storageBound`, see
+`storageBound_le_base_mul_pow`. It only depends on the alphabet, the state set and the number of
+work tapes, but not on the space. -/
+def storageBoundBase (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k : ℕ) : ℕ :=
+  (Fintype.card State + 1) * 2 ^ ((Fintype.card Symbol + 1) * k + k)
+
+/-- The factor in the exponent of the exponential form of `storageBound`, see
+`storageBound_le_base_mul_pow`. It only depends on the alphabet and the number of work tapes,
+but not on the space. -/
+def storageBoundExp (Symbol : Type*) [Fintype Symbol] (k : ℕ) : ℕ :=
+  2 * (Fintype.card Symbol + 1) + k
+
+/-- `storageBound` grows at most exponentially in the space `s`, with a constant factor and a
+factor in the exponent that only depend on the machine's alphabet, state set and tape count. -/
+lemma storageBound_le_base_mul_pow [Fintype Symbol] [Fintype State] (s : ℕ) :
+    storageBound Symbol State k s
+      ≤ storageBoundBase Symbol State k * 2 ^ (storageBoundExp Symbol k * s) := by
+  set syms := Fintype.card Symbol + 1 with hB
+  set states := Fintype.card State + 1 with hQ
+  -- The strategy is to bound each factor of `storageBound` by a power of `2`, using
+  -- `syms ≤ 2 ^ syms` and `2 * s + 1 ≤ 2 ^ (s + 1)`. Collecting the exponents then yields
+  -- `(s + 1) * k + syms * (2 * s + k)`, which splits into the constant part `syms * k + k`
+  -- (which is in `storageBoundBase`) and the part `(2 * syms + k) * s` linear in `s`.
+  have hB2 : syms ≤ 2 ^ syms := Nat.lt_two_pow_self.le
+  have h2s1 : 2 * s + 1 ≤ 2 ^ (s + 1) := by grind [pow_succ, Nat.lt_two_pow_self]
+  calc storageBound Symbol State k s
+      = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl
+    _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by
+        gcongr <;> exact Nat.zero_le _
+    _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by rw [← pow_mul, ← pow_mul, ← pow_add]
+    _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf
+    _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by rw [pow_add, mul_assoc]
+
+/-- `storageBound` grows at most exponentially in the space `s`: there exist constants `a` and `c`
+(depending on the machine's alphabet, state set and tape count) with
+`storageBound Symbol State k s ≤ a * 2 ^ (c * s)` for all `s`. -/
+lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
+    ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) :=
+  ⟨_, _, storageBound_le_base_mul_pow⟩
+
+/-! ## The storage and the core of a configuration -/
+
+/-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/
+def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k :=
+  ⟨c.state, c.workTapes, c.workTapePos⟩
+
+/-- The part of a configuration that the machine can still read: the input head position together
+with the `Storage`. This is the configuration without its write-only output tape, which `step`
+never looks at, so the core of the next configuration only depends on the core of the current
+one. -/
+def Cfg.core (c : Cfg k Symbol State input) :
+    Fin (input.length + 2) × UnboundedStorage Symbol State k :=
+  (c.inputPos, c.storage)
+
+/-- `step` never reads the output tape, so the core of the next configuration is determined by the
+core of the current one. This is what makes the bounds below usable to bound the running time of a
+machine: two configurations with the same core behave the same from then on. -/
+lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) :
+    (tm.step c₁).core = (tm.step c₂).core := by
+  simp only [Cfg.core, Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
+  obtain ⟨hpos, hstate, hwt, hwp⟩ := h
+  have hsym : c₁.inputSymbol = c₂.inputSymbol := by simp [Cfg.inputSymbol, hpos]
+  have hws : c₁.workTapeSymbols = c₂.workTapeSymbols := by
+    funext i
+    simp [Cfg.workTapeSymbols, hwt, hwp]
+  simp only [Cfg.core, Cfg.storage, step, hstate, hsym, hws]
+  cases c₂.state <;> simp [hpos, hstate, hwt, hwp]
+
+/-! ## The storages and cores of a space-bounded run -/
+
+/-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up
+to step `t`. -/
+lemma storage_fitsIn (t : ℕ) :
+    (tm.runFrom (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) t) := by
   refine ⟨?_, ?_⟩
   · intro j
     simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
@@ -247,83 +315,70 @@ lemma storage_fitsIn
   · intro j
     exact content_natAbs_le_spaceUsedByTape t
 
-
-open scoped Classical in
-/-- For any multi-tape Turing machine that uses at most space `s` up to step `t`, the number
-of storage configurations (configurations disregarding the input head positions) up to step `t`
-is at most `storageBound Symbol State k s` (independent of `t`). -/
-theorem card_storages_le
-    [Fintype Symbol] [Fintype State]
-    (t s : ℕ)
-    (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) :
-    ((Finset.range (t + 1)).image (fun t' => (tm.configs (tm.initCfg input) t').storage)).card
-    ≤ storageBound Symbol State k s := by
-  set space := tm.spaceUsedByTape (tm.initCfg input) t
-  calc ((Finset.range (t + 1)).image
-          (fun t' => (tm.configs (tm.initCfg input) t').storage)).card
-      ≤ Fintype.card (BoundedStorage Symbol State space) := by
-        rw [← Finset.card_univ]
-        refine Finset.card_le_card_of_injOn (Storage.toBounded · space) (by simp) ?_
-        refine Set.InjOn.mono ?_ (Storage.toBounded_injOn space)
-        intro x hx
-        simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Finset.mem_range] at hx
-        obtain ⟨t', ht, rfl⟩ := hx
-        exact storage_fitsIn t (by omega)
-    _ ≤ storageBound Symbol State k s := card_boundedStorage_le space s hs
-
-
-open scoped Classical in
-/-- The number of distinct configurations a multi-tape Turing machine with space bound `s`
-can reach is at most `(n + 2) * storageBound Symbol State k s`, where `n` is the input length.
-The `(n + 2)` factor accounts for the input-head position; the `storageBound` factor accounts for
-everything else (`storage`). -/
-theorem card_configs_le
-    [Fintype Symbol] [Fintype State]
-    (t s : ℕ)
-    (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) :
-    ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
+/-- **The storage bound.** A machine that uses at most `s` cells of work-tape space at every point
+in time passes through at most `storageBound Symbol State k s` different storages during its whole
+run — independently of the length of the input and of how long (or whether) it runs.
+
+Note that the input head position is deliberately not counted here: below logarithmic space this
+bound is much smaller than the number of input head positions, which is what makes arguments such
+as crossing sequences possible. Use `encard_cores_le` for the bound that includes the input head
+position. -/
+theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ}
+    (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) :
+    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard
+      ≤ storageBound Symbol State k s := by
+  obtain ⟨T, hT⟩ := tm.exists_spaceUsedByTape_max (tm.initCfg input) hs
+  refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs T))
+  rintro _ ⟨t, rfl⟩
+  exact Storage.FitsIn_mono (fun i => hT t i) (tm.storage_fitsIn t)
+
+/-- The number of cores (`Cfg.core`, i.e. configurations without their write-only output tape) that
+a machine bounded by space `s` can reach is at most `(n + 2) * storageBound Symbol State k s`,
+where `n` is the length of the input. The factor `n + 2` counts the positions of the input head,
+which — unlike the output tape — the machine can read and therefore cannot be dropped. -/
+theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
+    (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) :
+    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
       ≤ (input.length + 2) * storageBound Symbol State k s := by
-  -- Counting configurations reduces to counting `(inputPos, storage)` pairs, since the map to such
-  -- pairs is injective for a fixed input.
-  rw [← Finset.card_image_of_injective _ (inputPos_storage_injective input), Finset.image_image]
-  -- The pair image lies in the product of the input-head range with the storage image, so its
-  -- cardinality is bounded by `(n + 2)` times the storage count from `card_storages_le`.
-  calc ((Finset.range (t + 1)).image (fun t' =>
-          ((tm.configs (tm.initCfg input) t').inputPos.val,
-           (tm.configs (tm.initCfg input) t').storage))).card
-      ≤ (Finset.range (input.length + 2) ×ˢ (Finset.range (t + 1)).image
-          (fun t' => (tm.configs (tm.initCfg input) t').storage)).card := by
-        apply Finset.card_le_card
-        intro x hx
-        simp only [Finset.mem_image, Finset.mem_range] at hx
-        obtain ⟨t, ht, rfl⟩ := hx
-        simp only [Finset.mem_product, Finset.mem_range, Finset.mem_image]
-        exact ⟨(tm.configs (tm.initCfg input) t).inputPos.isLt, t, ht, rfl⟩
-    _ = (input.length + 2) * ((Finset.range (t + 1)).image
-          (fun t => (tm.configs (tm.initCfg input) t).storage)).card := by
-        rw [Finset.card_product, Finset.card_range]
-    _ ≤ (input.length + 2) * storageBound Symbol State k s :=
-        Nat.mul_le_mul_left _ (card_storages_le t s hs)
-
-open scoped Classical in
-/-- The number of distinct configurations reachable in space `s` is at most `2 ^ (O(s))`, up to the
-`(n + 2)` factor for the input-head position: there are constants `a` and `c` (depending only on
-the machine's alphabet, state set and tape count) that bound the configuration count for *every*
-input and step count. This is the form used to time-bound space-bounded machines. -/
-theorem card_configs_le_pow
-    [Finite Symbol] [Finite State] :
-    ∃ a c : ℕ, ∀ (input : List Symbol) (t s : ℕ),
-      tm.spaceUsed (tm.initCfg input) t ≤ s →
-      ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
+  calc (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+      ≤ ((Set.univ : Set (Fin (input.length + 2)))
+          ×ˢ (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage)).encard := by
+        refine Set.encard_le_encard ?_
+        rintro _ ⟨t, rfl⟩
+        exact ⟨Set.mem_univ _, t, rfl⟩
+    _ = (Set.univ : Set (Fin (input.length + 2))).encard
+          * (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard := Set.encard_prod
+    _ ≤ (input.length + 2) * storageBound Symbol State k s := by
+        refine mul_le_mul' ?_ (tm.encard_storages_le hs)
+        simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]
+
+/-- The storage bound in exponential form: the number of storages a space-`s`-bounded machine
+passes through is at most `2 ^ (O(s))`, with constants depending only on the machine. -/
+theorem encard_storages_le_pow [Finite Symbol] [Finite State] :
+    ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
+      (∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) →
+      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard ≤ a * 2 ^ (c * s) := by
+  have : Fintype Symbol := Fintype.ofFinite Symbol
+  have : Fintype State := Fintype.ofFinite State
+  obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
+  refine ⟨a, c, fun input s hs => (tm.encard_storages_le hs).trans ?_⟩
+  exact_mod_cast hpow s
+
+/-- The core bound in exponential form: the number of cores a space-`s`-bounded machine can reach
+is at most `(n + 2) * 2 ^ (O(s))`, with constants depending only on the machine and not on the
+input. This is the form used to time-bound space-bounded machines. -/
+theorem encard_cores_le_pow [Finite Symbol] [Finite State] :
+    ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
+      (∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) →
+      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
         ≤ (input.length + 2) * a * 2 ^ (c * s) := by
   have : Fintype Symbol := Fintype.ofFinite Symbol
   have : Fintype State := Fintype.ofFinite State
-  obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State)
-  refine ⟨a, c, fun input t s hs => ?_⟩
-  calc ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card
-      ≤ (input.length + 2) * storageBound Symbol State k s :=
-        tm.card_configs_le t s hs
-    _ ≤ (input.length + 2) * (a * 2 ^ (c * s)) := Nat.mul_le_mul_left _ (hpow s)
-    _ = (input.length + 2) * a * 2 ^ (c * s) := by ring
+  obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
+  refine ⟨a, c, fun input s hs => (tm.encard_cores_le hs).trans ?_⟩
+  calc ((input.length + 2) * storageBound Symbol State k s : ℕ∞)
+      ≤ ((input.length + 2) * (a * 2 ^ (c * s)) : ℕ) := by
+        exact_mod_cast Nat.mul_le_mul_left _ (hpow s)
+    _ = (input.length + 2) * a * 2 ^ (c * s) := by push_cast; ring
 
 end Turing.MultiTapeTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
index 15145637a..f51de84ee 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -7,6 +7,7 @@ Authors: Christian Reitwiessner
 module
 
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Mathlib.Order.Lattice.Nat
 
 /-!
 # Tape head visitation and space-usage lemmas
@@ -16,6 +17,10 @@ This file collects lemmas about the set of positions visited by a work-tape head
 (`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.spaceUsed`) and how the tape head positions
 influence the cells that are modified on a tape.
 
+`MultiTapeTM.exists_spaceUsedByTape_max` shows that a computation whose space usage is bounded
+attains its per-tape space usage at a single step, which makes a bound that holds at every point
+in time usable as a bound for the whole run.
+
 -/
 
 @[expose] public section
@@ -147,4 +152,25 @@ lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State
   intro t t' h
   exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h)
 
+/-- A computation whose total space usage stays below a bound reaches a step `T` at which the space
+usage of *every* tape is maximal. This turns a bound that holds at every point in time into a
+bound for the whole run. -/
+lemma exists_spaceUsedByTape_max (cfg : Cfg k Symbol State input) {s : ℕ}
+    (hs : ∀ t, tm.spaceUsed cfg t ≤ s) :
+    ∃ T, ∀ t i, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg T i := by
+  -- The total space usage is bounded, so it attains its supremum at some step `T`.
+  have hbdd : BddAbove (Set.range (tm.spaceUsed cfg ·)) := ⟨s, by rintro _ ⟨t, rfl⟩; exact hs t⟩
+  obtain ⟨T, hT⟩ := Nat.sSup_mem (Set.range_nonempty (tm.spaceUsed cfg ·)) hbdd
+  refine ⟨T, fun t i => ?_⟩
+  -- After `max t T` steps the total space usage is the same as after `T` steps, and since it is
+  -- tape-wise monotone, every single tape uses the same space as after `T` steps.
+  have hmono : ∀ j, tm.spaceUsedByTape cfg T j ≤ tm.spaceUsedByTape cfg (max t T) j :=
+    fun j => tm.spaceUsedByTape_mono cfg j (le_max_right t T)
+  have hsup : tm.spaceUsed cfg (max t T) ≤ tm.spaceUsed cfg T :=
+    (le_csSup hbdd ⟨max t T, rfl⟩).trans hT.ge
+  have hsum : ∑ j, tm.spaceUsedByTape cfg T j = ∑ j, tm.spaceUsedByTape cfg (max t T) j :=
+    le_antisymm (Finset.sum_le_sum fun j _ => hmono j) hsup
+  have heq := (Finset.sum_eq_sum_iff_of_le fun j _ => hmono j).mp hsum i (Finset.mem_univ i)
+  exact heq ▸ tm.spaceUsedByTape_mono cfg i (le_max_left t T)
+
 end Turing.MultiTapeTM

From 4876d0335a715babb8dc19455d9d0c2066697234 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Sat, 29 Aug 2026 11:53:40 +0200
Subject: [PATCH 3/6] cleanup

---
 .../Turing/MultiTape/ConfigBound.lean         | 120 +++++++++---------
 1 file changed, 59 insertions(+), 61 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index 465a49da5..aac293534 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -19,9 +19,9 @@ public import Mathlib.Tactic.Ring
 /-!
 # Bounds on the number of reachable configurations in bounded space
 
-A deterministic multi-tape Turing machine that uses at most `s` cells of work-tape space can only
-be in exponentially many (in `s`) different *storages*, i.e. states, work tape contents and work
-tape head positions. Together with the `n + 2` possible positions of the input head this bounds
+A multi-tape Turing machine that uses at most `s` cells of work-tape space can only reach a number
+of configurations that differ in their storage content (state and work tapes) that is bounded
+exponentially in `s`. Together with the `n + 2` possible positions of the input head this bounds
 the number of configurations the machine can be in, disregarding the write-only output tape.
 
 ## Important Definitions
@@ -78,15 +78,23 @@ variable {State Symbol : Type*}
 variable {input : List Symbol}
 variable {tm : MultiTapeTM k Symbol State}
 
-/-! ## Storages -/
+/-!
+## Storage
+
+Defines the core data structure for this file, `Storage`, which contains the state and the work
+tapes of a multi-tape Turing machine, where the work tape cells are indexed over a generic index
+type.
+
+Then `UnboundedStorage` uses `ℤ` as index type and thus is equivalent to a projection of `Cfg`.
+
+Finally, `BoundedStorage` is introduced which uses `[-s, s]` as index type (with different `s`
+for each tape) and it is proven that there is an injective mapping from `UnboundedStorage`
+to `BoundedStorage` if the non-blank cells and head positions of the `UnboundedStorage` all lie
+inside the `[-s, s]` windows for all tapes.
+-/
 
 /-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed
-by an arbitrary type `ι i`. Adding the input head position and using `ι i = ℤ` gives `Cfg.core`,
-a configuration without its write-only output tape (cf. `Cfg.storage`).
-The index set is useful for cardinality arguments if we have a bound on the tape cells that
-are actually used.
-The input head position is not included because leaving it out is useful for arguments below
-logarithmic space, where there are fewer storages than input head positions. -/
+by an arbitrary type `ι i`. -/
 @[ext]
 structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where
   /-- the state of the TM (cf. `Cfg.state`) -/
@@ -96,7 +104,7 @@ structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where
   /-- the position of the head on work tape `i` (cf. `Cfg.workTapePos`) -/
   workTapePos (i : Fin k) : ι i
 
-/-- A `Storage` is just a product of its fields; this equivalence is used for counting. -/
+/-- A `Storage` is just a product of its fields. -/
 def Storage.equivProd (Symbol State : Type*) (ι : Fin k → Type*) :
     Storage Symbol State ι ≃
       Option State × ((i : Fin k) → ι i → Option Symbol) × ((i : Fin k) → ι i) where
@@ -108,28 +116,25 @@ instance (Symbol State : Type*) [Fintype Symbol] [Fintype State]
     Fintype (Storage Symbol State ι) :=
   Fintype.ofEquiv _ (Storage.equivProd Symbol State ι).symm
 
-/-- A `Storage` over the unrestricted index type `ℤ` for every tape, as extracted from a full
-configuration by `Cfg.storage`. -/
-abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) :=
-  Storage Symbol State (fun _ : Fin k => ℤ)
+/-- A `Storage` using the tape index type `ℤ`. -/
+abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) := Storage Symbol State (fun _ : Fin k => ℤ)
 
 /-- The window `[-s, s]` of tape positions allotted to a tape that uses `s` cells. -/
-def Storage.window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
+@[scoped grind =]
+def window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
 
 @[scoped grind =]
-lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ Storage.window s ↔ z.natAbs ≤ s := by
-  grind [Storage.window]
+lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s := by
+  grind
 
 @[simp]
-lemma Storage.card_window (s : ℕ) : (Storage.window s).card = 2 * s + 1 := by
-  grind [Storage.window, Int.card_Icc]
+lemma Storage.card_window (s : ℕ) : (window s).card = 2 * s + 1 := by
+  grind [Int.card_Icc]
 
 /-- A bounded storage: a `Storage` whose tape `i` is restricted to the finite window
-`[-(w i), w i]`. The storages of a computation that visits at most the window of each tape embed
-injectively into this finite type (`Storage.toBounded`), so its cardinality bounds the number of
-reachable storages. -/
+`[-(w i), w i]`. -/
 abbrev BoundedStorage (Symbol State : Type*) {k : ℕ} (w : Fin k → ℕ) :=
-  Storage Symbol State (fun i => Storage.window (w i))
+  Storage Symbol State (fun i => window (w i))
 
 /-- A storage fits in the per-tape windows `w`: on each tape `j`, the head position and every
 non-blank cell have absolute value `≤ w j`. -/
@@ -155,7 +160,7 @@ def Storage.toBounded (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ)
   state := x.state
   workTapes j z := x.workTapes j z.1
   workTapePos j :=
-    if h : x.workTapePos j ∈ Storage.window (w j) then ⟨x.workTapePos j, h⟩
+    if h : x.workTapePos j ∈ window (w j) then ⟨x.workTapePos j, h⟩
     else ⟨0, Storage.mem_window.mpr (Nat.zero_le _)⟩
 
 /-- The restriction is injective on storages that fit in the windows. -/
@@ -165,11 +170,10 @@ lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
   simp only [Storage.toBounded, Storage.mk.injEq] at hxy
   obtain ⟨hstate, htapes, hpos⟩ := hxy
   refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
-  · by_cases hz : z ∈ Storage.window (w j)
+  · by_cases hz : z ∈ window (w j)
     · exact congrFun (congrFun htapes j) ⟨z, hz⟩
     · grind
-  · have := congrFun hpos j
-    grind [Subtype.ext_iff]
+  · grind [congrFun hpos j]
 
 /-! ## Counting storages
 
@@ -192,8 +196,7 @@ lemma card_storage [Fintype Symbol] [Fintype State]
 /-- An upper bound on the number of storages a `k`-tape machine can be in while using
 at most `s` cells of total work-tape space, over the given alphabet and state set. The `(2s + 1)^k`
 factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(2s + k)` uses the
-*total* space `s` in the exponent (the `k` tapes share the space budget), matching the textbook
-`|State| · |Symbol|^{O(s)} · poly(s)` count. -/
+*total* space `s` in the exponent (the `k` tapes share the space budget). -/
 def storageBound (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ :=
   (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k))
 
@@ -216,8 +219,7 @@ lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
 
 /-- The counting result at the heart of this file: a `Storage` whose non-blank cells and head
 positions stay within per-tape windows of total size at most `s` can take at most
-`storageBound Symbol State k s` different values. This does not refer to a machine, a run, or an
-input; it only counts how much a memory of that shape can hold. -/
+`storageBound Symbol State k s` different values. -/
 theorem encard_fitsIn_le [Fintype Symbol] [Fintype State]
     {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i, w i ≤ s) :
     {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
@@ -232,17 +234,16 @@ theorem encard_fitsIn_le [Fintype Symbol] [Fintype State]
     _ ≤ storageBound Symbol State k s := by
         exact_mod_cast card_boundedStorage_le hsum
 
-/-! ### The exponential form of `storageBound` -/
+/-! ### The exponential form of `storageBound`
 
-/-- The constant factor in the exponential form of `storageBound`, see
-`storageBound_le_base_mul_pow`. It only depends on the alphabet, the state set and the number of
-work tapes, but not on the space. -/
+This proves that `storageBound` is exponential in the space `s`.
+ -/
+
+/-- The base factor in the resulting exponential form of `storageBound`. -/
 def storageBoundBase (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k : ℕ) : ℕ :=
   (Fintype.card State + 1) * 2 ^ ((Fintype.card Symbol + 1) * k + k)
 
-/-- The factor in the exponent of the exponential form of `storageBound`, see
-`storageBound_le_base_mul_pow`. It only depends on the alphabet and the number of work tapes,
-but not on the space. -/
+/-- The factor in the exponent of the exponential form of `storageBound`. -/
 def storageBoundExp (Symbol : Type*) [Fintype Symbol] (k : ℕ) : ℕ :=
   2 * (Fintype.card Symbol + 1) + k
 
@@ -263,9 +264,9 @@ lemma storageBound_le_base_mul_pow [Fintype Symbol] [Fintype State] (s : ℕ) :
       = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl
     _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by
         gcongr <;> exact Nat.zero_le _
-    _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by rw [← pow_mul, ← pow_mul, ← pow_add]
+    _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by ring
     _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf
-    _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by rw [pow_add, mul_assoc]
+    _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by ring
 
 /-- `storageBound` grows at most exponentially in the space `s`: there exist constants `a` and `c`
 (depending on the machine's alphabet, state set and tape count) with
@@ -274,23 +275,23 @@ lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
     ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) :=
   ⟨_, _, storageBound_le_base_mul_pow⟩
 
-/-! ## The storage and the core of a configuration -/
+/-! ## The storage and the core of a configuration
+
+Now we relate `Cfg` and `Storage` by givin the projection.
+-/
 
 /-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/
 def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k :=
   ⟨c.state, c.workTapes, c.workTapePos⟩
 
 /-- The part of a configuration that the machine can still read: the input head position together
-with the `Storage`. This is the configuration without its write-only output tape, which `step`
-never looks at, so the core of the next configuration only depends on the core of the current
-one. -/
+with the `Storage`, i.e. the configuration without the write-only output tape. -/
 def Cfg.core (c : Cfg k Symbol State input) :
     Fin (input.length + 2) × UnboundedStorage Symbol State k :=
   (c.inputPos, c.storage)
 
 /-- `step` never reads the output tape, so the core of the next configuration is determined by the
-core of the current one. This is what makes the bounds below usable to bound the running time of a
-machine: two configurations with the same core behave the same from then on. -/
+core of the current one. -/
 lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) :
     (tm.step c₁).core = (tm.step c₂).core := by
   simp only [Cfg.core, Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
@@ -302,7 +303,11 @@ lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.c
   simp only [Cfg.core, Cfg.storage, step, hstate, hsym, hws]
   cases c₂.state <;> simp [hpos, hstate, hwt, hwp]
 
-/-! ## The storages and cores of a space-bounded run -/
+/-! ## The storages and cores of a space-bounded run
+
+These are the main results giving upper bounds on the number of storages and configuration cores
+reachable in bounded space.
+-/
 
 /-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up
 to step `t`. -/
@@ -315,14 +320,9 @@ lemma storage_fitsIn (t : ℕ) :
   · intro j
     exact content_natAbs_le_spaceUsedByTape t
 
-/-- **The storage bound.** A machine that uses at most `s` cells of work-tape space at every point
-in time passes through at most `storageBound Symbol State k s` different storages during its whole
-run — independently of the length of the input and of how long (or whether) it runs.
-
-Note that the input head position is deliberately not counted here: below logarithmic space this
-bound is much smaller than the number of input head positions, which is what makes arguments such
-as crossing sequences possible. Use `encard_cores_le` for the bound that includes the input head
-position. -/
+/-- A machine that uses at most `s` cells of work-tape space at every point in time passes through
+at most `storageBound Symbol State k s` different storages during its whole run — independently of
+the length of the input and of how long it runs. -/
 theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ}
     (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) :
     (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard
@@ -332,10 +332,8 @@ theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ}
   rintro _ ⟨t, rfl⟩
   exact Storage.FitsIn_mono (fun i => hT t i) (tm.storage_fitsIn t)
 
-/-- The number of cores (`Cfg.core`, i.e. configurations without their write-only output tape) that
-a machine bounded by space `s` can reach is at most `(n + 2) * storageBound Symbol State k s`,
-where `n` is the length of the input. The factor `n + 2` counts the positions of the input head,
-which — unlike the output tape — the machine can read and therefore cannot be dropped. -/
+/-- The number of configuration cores that a machine bounded by space `s` can reach is at most
+`(n + 2) * storageBound Symbol State k s`, where `n` is the length of the input. -/
 theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
     (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) :
     (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
@@ -366,7 +364,7 @@ theorem encard_storages_le_pow [Finite Symbol] [Finite State] :
 
 /-- The core bound in exponential form: the number of cores a space-`s`-bounded machine can reach
 is at most `(n + 2) * 2 ^ (O(s))`, with constants depending only on the machine and not on the
-input. This is the form used to time-bound space-bounded machines. -/
+input. -/
 theorem encard_cores_le_pow [Finite Symbol] [Finite State] :
     ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
       (∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s) →

From fa7ed1d3afc548a8ace1ce92557bc35c14f24ba3 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Sat, 29 Aug 2026 13:49:13 +0200
Subject: [PATCH 4/6] Review comments.

---
 Cslib.lean                                    |  2 +-
 .../Turing/MultiTape/ConfigBound.lean         | 21 ++++++++--------
 .../Machines/Turing/MultiTape/TapeLemmas.lean | 25 ++++++++-----------
 3 files changed, 22 insertions(+), 26 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index bdd080764..0cea16445 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -45,8 +45,8 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
-public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
 public import Cslib.Computability.Languages.SafetyLiveness
+public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index aac293534..991d59655 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -124,11 +124,11 @@ abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) := Storage Symbol State
 def window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
 
 @[scoped grind =]
-lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s := by
+lemma mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s := by
   grind
 
 @[simp]
-lemma Storage.card_window (s : ℕ) : (window s).card = 2 * s + 1 := by
+lemma card_window (s : ℕ) : (window s).card = 2 * s + 1 := by
   grind [Int.card_Icc]
 
 /-- A bounded storage: a `Storage` whose tape `i` is restricted to the finite window
@@ -149,9 +149,9 @@ lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.Fit
   intro w₁ w₂ h_le h_fits
   refine ⟨?_, ?_⟩
   · intro j
-    grind [h_fits.pos_le j, h_le j]
+    exact (h_fits.pos_le j).trans (h_le j)
   · intro j z h_ne
-    grind [h_fits.cell_le j z h_ne, h_le j]
+    exact (h_fits.cell_le j z h_ne).trans (h_le j)
 
 /-- Restriction of a storage over `ℤ` to the finite windows `w` (with heads outside their window
 clamped to `0`). -/
@@ -161,7 +161,7 @@ def Storage.toBounded (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ)
   workTapes j z := x.workTapes j z.1
   workTapePos j :=
     if h : x.workTapePos j ∈ window (w j) then ⟨x.workTapePos j, h⟩
-    else ⟨0, Storage.mem_window.mpr (Nat.zero_le _)⟩
+    else ⟨0, mem_window.mpr (Nat.zero_le _)⟩
 
 /-- The restriction is injective on storages that fit in the windows. -/
 lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
@@ -169,7 +169,7 @@ lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
   rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
   simp only [Storage.toBounded, Storage.mk.injEq] at hxy
   obtain ⟨hstate, htapes, hpos⟩ := hxy
-  refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
+  apply Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
   · by_cases hz : z ∈ window (w j)
     · exact congrFun (congrFun htapes j) ⟨z, hz⟩
     · grind
@@ -207,7 +207,7 @@ lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
     Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s := by
   have hle : ∀ i, w i ≤ s := fun i =>
     (Finset.single_le_sum (fun i _ => Nat.zero_le (w i)) (Finset.mem_univ i)).trans hsum
-  simp only [card_storage, storageBound, Fintype.card_coe, Storage.card_window]
+  simp only [card_storage, storageBound, Fintype.card_coe, card_window]
   rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum]
   have hsc : ∑ i : Fin k, (2 * w i + 1) = 2 * (∑ i, w i) + k := by
     simp [two_mul, Finset.sum_add_distrib]
@@ -262,8 +262,7 @@ lemma storageBound_le_base_mul_pow [Fintype Symbol] [Fintype State] (s : ℕ) :
   have h2s1 : 2 * s + 1 ≤ 2 ^ (s + 1) := by grind [pow_succ, Nat.lt_two_pow_self]
   calc storageBound Symbol State k s
       = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl
-    _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by
-        gcongr <;> exact Nat.zero_le _
+    _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by gcongr <;> omega
     _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by ring
     _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf
     _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by ring
@@ -313,7 +312,7 @@ reachable in bounded space.
 to step `t`. -/
 lemma storage_fitsIn (t : ℕ) :
     (tm.runFrom (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) t) := by
-  refine ⟨?_, ?_⟩
+  constructor
   · intro j
     simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
       (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)
@@ -341,7 +340,7 @@ theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
   calc (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
       ≤ ((Set.univ : Set (Fin (input.length + 2)))
           ×ˢ (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage)).encard := by
-        refine Set.encard_le_encard ?_
+        apply Set.encard_le_encard
         rintro _ ⟨t, rfl⟩
         exact ⟨Set.mem_univ _, t, rfl⟩
     _ = (Set.univ : Set (Fin (input.length + 2))).encard
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
index f51de84ee..c0c6913f8 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -158,19 +158,16 @@ bound for the whole run. -/
 lemma exists_spaceUsedByTape_max (cfg : Cfg k Symbol State input) {s : ℕ}
     (hs : ∀ t, tm.spaceUsed cfg t ≤ s) :
     ∃ T, ∀ t i, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg T i := by
-  -- The total space usage is bounded, so it attains its supremum at some step `T`.
-  have hbdd : BddAbove (Set.range (tm.spaceUsed cfg ·)) := ⟨s, by rintro _ ⟨t, rfl⟩; exact hs t⟩
-  obtain ⟨T, hT⟩ := Nat.sSup_mem (Set.range_nonempty (tm.spaceUsed cfg ·)) hbdd
-  refine ⟨T, fun t i => ?_⟩
-  -- After `max t T` steps the total space usage is the same as after `T` steps, and since it is
-  -- tape-wise monotone, every single tape uses the same space as after `T` steps.
-  have hmono : ∀ j, tm.spaceUsedByTape cfg T j ≤ tm.spaceUsedByTape cfg (max t T) j :=
-    fun j => tm.spaceUsedByTape_mono cfg j (le_max_right t T)
-  have hsup : tm.spaceUsed cfg (max t T) ≤ tm.spaceUsed cfg T :=
-    (le_csSup hbdd ⟨max t T, rfl⟩).trans hT.ge
-  have hsum : ∑ j, tm.spaceUsedByTape cfg T j = ∑ j, tm.spaceUsedByTape cfg (max t T) j :=
-    le_antisymm (Finset.sum_le_sum fun j _ => hmono j) hsup
-  have heq := (Finset.sum_eq_sum_iff_of_le fun j _ => hmono j).mp hsum i (Finset.mem_univ i)
-  exact heq ▸ tm.spaceUsedByTape_mono cfg i (le_max_left t T)
+  -- The space usage of a single tape is bounded, so it attains its supremum at some step `T i`.
+  have h : ∀ i, ∃ Ti, ∀ t, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg Ti i := by
+    intro i
+    have hbdd : BddAbove (Set.range (tm.spaceUsedByTape cfg · i)) :=
+      ⟨s, by rintro _ ⟨t, rfl⟩; exact (tm.spaceUsedByTape_le_spaceUsed cfg t i).trans (hs t)⟩
+    obtain ⟨Ti, hTi⟩ := Nat.sSup_mem (Set.range_nonempty (tm.spaceUsedByTape cfg · i)) hbdd
+    exact ⟨Ti, fun t => (le_csSup hbdd ⟨t, rfl⟩).trans hTi.ge⟩
+  choose T hT using h
+  -- Monotonicity lets us use a single step that is late enough for every tape.
+  exact ⟨Finset.univ.sup T, fun t i =>
+    (hT i t).trans (tm.spaceUsedByTape_mono cfg i (Finset.le_sup (Finset.mem_univ i)))⟩
 
 end Turing.MultiTapeTM

From 2ac2da54b17c1e25e588d856e2bddefb0e5da33e Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Sat, 29 Aug 2026 14:38:05 +0200
Subject: [PATCH 5/6] Define Storage only for \Int-indexed tapes and use tuple
 for the bounded version.

---
 .../Turing/MultiTape/ConfigBound.lean         | 103 +++++++-----------
 1 file changed, 38 insertions(+), 65 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index 991d59655..9f9ba646a 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -82,42 +82,25 @@ variable {tm : MultiTapeTM k Symbol State}
 ## Storage
 
 Defines the core data structure for this file, `Storage`, which contains the state and the work
-tapes of a multi-tape Turing machine, where the work tape cells are indexed over a generic index
-type.
-
-Then `UnboundedStorage` uses `ℤ` as index type and thus is equivalent to a projection of `Cfg`.
-
-Finally, `BoundedStorage` is introduced which uses `[-s, s]` as index type (with different `s`
-for each tape) and it is proven that there is an injective mapping from `UnboundedStorage`
-to `BoundedStorage` if the non-blank cells and head positions of the `UnboundedStorage` all lie
-inside the `[-s, s]` windows for all tapes.
+tapes of a multi-tape Turing machine, with the work tape cells indexed over all of `ℤ`. It is
+thus equivalent to a projection of `Cfg`.
+
+Then `BoundedStorage` is introduced, which restricts the cells and the head position of each tape
+to a window `[-s, s]` (with a different `s` for each tape) and is therefore a finite type. It is
+proven that the restriction map is injective on those `Storage`s whose non-blank cells and head
+positions all lie inside the `[-s, s]` windows, so that counting `BoundedStorage` bounds the
+number of such `Storage`s.
 -/
 
-/-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed
-by an arbitrary type `ι i`. -/
+/-- The state and work-tape data of a machine. -/
 @[ext]
-structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where
+structure Storage (Symbol State : Type*) (k : ℕ) where
   /-- the state of the TM (cf. `Cfg.state`) -/
   state : Option State
   /-- the contents of work tape `i` (cf. `Cfg.workTapes`) -/
-  workTapes (i : Fin k) : ι i → Option Symbol
+  workTapes (i : Fin k) : ℤ → Option Symbol
   /-- the position of the head on work tape `i` (cf. `Cfg.workTapePos`) -/
-  workTapePos (i : Fin k) : ι i
-
-/-- A `Storage` is just a product of its fields. -/
-def Storage.equivProd (Symbol State : Type*) (ι : Fin k → Type*) :
-    Storage Symbol State ι ≃
-      Option State × ((i : Fin k) → ι i → Option Symbol) × ((i : Fin k) → ι i) where
-  toFun x := (x.state, x.workTapes, x.workTapePos)
-  invFun := fun ⟨state, workTapes, workTapePos⟩ => ⟨state, workTapes, workTapePos⟩
-
-instance (Symbol State : Type*) [Fintype Symbol] [Fintype State]
-    (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] :
-    Fintype (Storage Symbol State ι) :=
-  Fintype.ofEquiv _ (Storage.equivProd Symbol State ι).symm
-
-/-- A `Storage` using the tape index type `ℤ`. -/
-abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) := Storage Symbol State (fun _ : Fin k => ℤ)
+  workTapePos (i : Fin k) : ℤ
 
 /-- The window `[-s, s]` of tape positions allotted to a tape that uses `s` cells. -/
 @[scoped grind =]
@@ -131,21 +114,21 @@ lemma mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s := by
 lemma card_window (s : ℕ) : (window s).card = 2 * s + 1 := by
   grind [Int.card_Icc]
 
-/-- A bounded storage: a `Storage` whose tape `i` is restricted to the finite window
-`[-(w i), w i]`. -/
+/-- A bounded storage: the state and work-tape data of a machine, but with the cells and the head
+position of tape `i` restricted to the finite window `[-(w i), w i]`. -/
 abbrev BoundedStorage (Symbol State : Type*) {k : ℕ} (w : Fin k → ℕ) :=
-  Storage Symbol State (fun i => window (w i))
+  Option State × ((i : Fin k) → window (w i) → Option Symbol) × ((i : Fin k) → window (w i))
 
 /-- A storage fits in the per-tape windows `w`: on each tape `j`, the head position and every
 non-blank cell have absolute value `≤ w j`. -/
-structure Storage.FitsIn (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) : Prop where
+structure Storage.FitsIn (x : Storage Symbol State k) (w : Fin k → ℕ) : Prop where
   /-- the head position on every tape lies within its window -/
   pos_le : ∀ j, (x.workTapePos j).natAbs ≤ w j
   /-- every non-blank cell on every tape lies within its window -/
   cell_le : ∀ j z, x.workTapes j z ≠ none → z.natAbs ≤ w j
 
-/-- If an `UnboundedStorage` fits in a smaller window, it also fits in the larger window. -/
-lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.FitsIn := by
+/-- If a `Storage` fits in a smaller window, it also fits in the larger window. -/
+lemma Storage.FitsIn_mono {x : Storage Symbol State k} : Monotone x.FitsIn := by
   intro w₁ w₂ h_le h_fits
   refine ⟨?_, ?_⟩
   · intro j
@@ -153,21 +136,19 @@ lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.Fit
   · intro j z h_ne
     exact (h_fits.cell_le j z h_ne).trans (h_le j)
 
-/-- Restriction of a storage over `ℤ` to the finite windows `w` (with heads outside their window
+/-- Restriction of a storage to the finite windows `w` (with heads outside their window
 clamped to `0`). -/
-def Storage.toBounded (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) :
-    BoundedStorage Symbol State w where
-  state := x.state
-  workTapes j z := x.workTapes j z.1
-  workTapePos j :=
-    if h : x.workTapePos j ∈ window (w j) then ⟨x.workTapePos j, h⟩
-    else ⟨0, mem_window.mpr (Nat.zero_le _)⟩
+def Storage.toBounded (x : Storage Symbol State k) (w : Fin k → ℕ) :
+    BoundedStorage Symbol State w :=
+  (x.state, fun j z => x.workTapes j z.1,
+    fun j => if h : x.workTapePos j ∈ window (w j) then ⟨x.workTapePos j, h⟩
+      else ⟨0, mem_window.mpr (Nat.zero_le _)⟩)
 
 /-- The restriction is injective on storages that fit in the windows. -/
 lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
     Set.InjOn (Storage.toBounded (Symbol := Symbol) (State := State) · w) {x | x.FitsIn w} := by
   rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
-  simp only [Storage.toBounded, Storage.mk.injEq] at hxy
+  simp only [Storage.toBounded, Prod.mk.injEq] at hxy
   obtain ⟨hstate, htapes, hpos⟩ := hxy
   apply Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
   · by_cases hz : z ∈ window (w j)
@@ -181,18 +162,6 @@ This section is purely combinatorial: it counts how many values a `Storage` rest
 windows can take, without reference to a machine or a run.
 -/
 
-/-- The number of storages over finite position types is the per-tape product of
-"cell contents × head position" counts. -/
-lemma card_storage [Fintype Symbol] [Fintype State]
-    (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] :
-    Fintype.card (Storage Symbol State ι)
-      = (Fintype.card State + 1)
-        * ∏ i, Fintype.card (ι i) * (Fintype.card Symbol + 1) ^ Fintype.card (ι i) := by
-  rw [Fintype.card_congr (Storage.equivProd Symbol State ι)]
-  simp only [Fintype.card_prod, Fintype.card_option, Fintype.card_pi, Finset.prod_const,
-    Finset.card_univ, Finset.prod_mul_distrib]
-  ring
-
 /-- An upper bound on the number of storages a `k`-tape machine can be in while using
 at most `s` cells of total work-tape space, over the given alphabet and state set. The `(2s + 1)^k`
 factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(2s + k)` uses the
@@ -200,15 +169,18 @@ factor counts the possible head positions; the dominant factor `(|Symbol| + 1)^(
 def storageBound (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ :=
   (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k))
 
-/-- The per-tape product is bounded by `storageBound`: each tape uses at most the total space `s`,
-and the tapes together use at most `s`, which collapses the alphabet exponent to `2s + k`. -/
+/-- The number of bounded storages is at most `storageBound`. Counting the tapes separately gives
+the per-tape product `∏ᵢ (2 wᵢ + 1) · (|Symbol| + 1) ^ (2 wᵢ + 1)`; each tape uses at most the
+total space `s`, and the tapes together use at most `s`, which collapses the alphabet exponent
+to `2s + k`. -/
 lemma card_boundedStorage_le [Fintype Symbol] [Fintype State]
     {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i, w i ≤ s) :
     Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s := by
   have hle : ∀ i, w i ≤ s := fun i =>
     (Finset.single_le_sum (fun i _ => Nat.zero_le (w i)) (Finset.mem_univ i)).trans hsum
-  simp only [card_storage, storageBound, Fintype.card_coe, card_window]
-  rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum]
+  simp only [BoundedStorage, storageBound, Fintype.card_prod, Fintype.card_option,
+    Fintype.card_pi, Finset.prod_const, Finset.card_univ, Fintype.card_coe, card_window]
+  rw [mul_comm (∏ i, (Fintype.card Symbol + 1) ^ (2 * w i + 1)), Finset.prod_pow_eq_pow_sum]
   have hsc : ∑ i : Fin k, (2 * w i + 1) = 2 * (∑ i, w i) + k := by
     simp [two_mul, Finset.sum_add_distrib]
   gcongr
@@ -222,9 +194,9 @@ positions stay within per-tape windows of total size at most `s` can take at mos
 `storageBound Symbol State k s` different values. -/
 theorem encard_fitsIn_le [Fintype Symbol] [Fintype State]
     {w : Fin k → ℕ} {s : ℕ} (hsum : ∑ i, w i ≤ s) :
-    {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
+    {x : Storage Symbol State k | x.FitsIn w}.encard
       ≤ storageBound Symbol State k s := by
-  calc {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
+  calc {x : Storage Symbol State k | x.FitsIn w}.encard
       = ((Storage.toBounded · w) '' {x | x.FitsIn w}).encard :=
         ((Storage.toBounded_injOn w).encard_image).symm
     _ ≤ (Set.univ : Set (BoundedStorage Symbol State w)).encard :=
@@ -279,14 +251,15 @@ lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
 Now we relate `Cfg` and `Storage` by givin the projection.
 -/
 
-/-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/
-def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k :=
+/-- This function maps a `Cfg` to `Storage`, forgetting the input head position and the
+write-only output tape. -/
+def Cfg.storage (c : Cfg k Symbol State input) : Storage Symbol State k :=
   ⟨c.state, c.workTapes, c.workTapePos⟩
 
 /-- The part of a configuration that the machine can still read: the input head position together
 with the `Storage`, i.e. the configuration without the write-only output tape. -/
 def Cfg.core (c : Cfg k Symbol State input) :
-    Fin (input.length + 2) × UnboundedStorage Symbol State k :=
+    Fin (input.length + 2) × Storage Symbol State k :=
   (c.inputPos, c.storage)
 
 /-- `step` never reads the output tape, so the core of the next configuration is determined by the

From 261bfa23c5948437c9fbbffac3506c21b142c15d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 2 Sep 2026 10:15:58 +0200
Subject: [PATCH 6/6] Review comments.

---
 .../Machines/Turing/MultiTape/ConfigBound.lean              | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
index 9f9ba646a..c722fc2d3 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean
@@ -69,8 +69,6 @@ time attains its per-tape space usage at a single step (`MultiTapeTM.exists_spac
 
 @[expose] public section
 
-open Cslib
-
 namespace Turing.MultiTapeTM
 
 variable {k : ℕ}
@@ -147,7 +145,7 @@ def Storage.toBounded (x : Storage Symbol State k) (w : Fin k → ℕ) :
 /-- The restriction is injective on storages that fit in the windows. -/
 lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
     Set.InjOn (Storage.toBounded (Symbol := Symbol) (State := State) · w) {x | x.FitsIn w} := by
-  rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
+  rintro x ⟨_, _⟩ y ⟨_, _⟩ hxy
   simp only [Storage.toBounded, Prod.mk.injEq] at hxy
   obtain ⟨hstate, htapes, hpos⟩ := hxy
   apply Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
@@ -248,7 +246,7 @@ lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
 
 /-! ## The storage and the core of a configuration
 
-Now we relate `Cfg` and `Storage` by givin the projection.
+Now we relate `Cfg` and `Storage` by giving the projection.
 -/
 
 /-- This function maps a `Cfg` to `Storage`, forgetting the input head position and the