diff --git a/Complexity.lean b/Complexity.lean
index 12dd9699e..9a64c549e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1861,6 +1861,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.D
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalSimulation
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IterateWhile
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Loop
@@ -2622,6 +2623,7 @@ public import Complexity.Foundations.Combinatorics.WeightBudget
 public import Complexity.Foundations.Control.Monad.IsMonadHom.StateT
 public import Complexity.Foundations.Control.Monad.Memoize
 public import Complexity.Foundations.Data.BiTape
+public import Complexity.Foundations.Data.BiTape.OfCells
 public import Complexity.Foundations.Data.BitString.Affine
 public import Complexity.Foundations.Data.BitString.AffineSubspace
 public import Complexity.Foundations.Data.BitString.Agree
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalSimulation.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalSimulation.lean
new file mode 100644
index 000000000..cba94354c
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalSimulation.lean
@@ -0,0 +1,363 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor
+public import Complexity.Computability.Machines.Turing.MultiTape.Run
+public import Complexity.Foundations.Data.BiTape.OfCells
+
+/-!
+# Interval steps by finite simulation
+
+An interval step (`Turing.MultiTapePTM.IntervalStep`) replays coins from a configuration whose
+work tapes are functions on `ℤ`. This module decides it by a simulation on finite storage, the
+first step towards computing the block-counting networks of #1833 in polynomial time.
+
+**Finite storage** (`Turing.MultiTapePTM.LocalCfg`) keeps the control, the input position as a
+natural number, every work tape as a `Cslib.Turing.BiTape` around its head together with the
+head's absolute position, and only the track of the output
+(`Turing.MultiTapeNTM.ChoiceTable.OutputTrack`), which is all a control record keeps. One coin
+step (`Turing.MultiTapePTM.localCoinStep`) applies the table's action; on halted storage it changes
+nothing. Finite storage *represents* a configuration (`Turing.MultiTapePTM.LocalCfg.Represents`)
+when it has its control, input position, head positions, output track and the contents of every
+work tape around its head; steps preserve this
+(`Turing.MultiTapePTM.LocalCfg.Represents.localRun`).
+
+**The window.** The configuration embedded at block indices `J` with control record `cIn` and
+window contents `wIn` (`Turing.embedCfg`) is represented by `Turing.MultiTapePTM.localStart`,
+which loads the `3 b` cells of each window into a tape (`Cslib.Turing.BiTape.ofCells`). Its control
+record, block indices and window contents are read back from finite storage
+(`Turing.MultiTapePTM.LocalCfg.blockControl`, `Turing.MultiTapePTM.LocalCfg.blockIndex`,
+`Turing.MultiTapePTM.LocalCfg.windowContents`).
+
+## Main definitions
+
+* `Turing.MultiTapePTM.LocalCfg`: finite storage for replaying an interval.
+* `Turing.MultiTapePTM.coinAction`, `Turing.MultiTapePTM.localCoinStep`,
+  `Turing.MultiTapePTM.localRun`: one coin step and a replay on finite storage.
+* `Turing.MultiTapePTM.windowCells`, `Turing.MultiTapePTM.localStart`: the finite storage of an
+  embedded window.
+* `Turing.MultiTapePTM.LocalIntervalStep`: the interval condition on finite storage.
+
+## Main results
+
+* `Turing.MultiTapePTM.LocalCfg.Represents.localRun`: replays preserve the representation.
+* `Turing.MultiTapePTM.represents_localStart`: the finite storage of an embedded window.
+* `Turing.MultiTapePTM.intervalStep_iff_localIntervalStep`: interval steps are decided by finite
+  simulation.
+* `Turing.MultiTapePTM.intervalCount_eq_card_localIntervalStep`: so are the interval tensors.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+open MultiTapeNTM.ChoiceTable Cslib.Turing
+
+variable {k : ℕ} {State : Type}
+
+/-! ### Finite storage and its steps -/
+
+/-- **Finite storage** for replaying an interval: the control, the input position (`0` and
+`|input| + 1` are the end cells), every work tape around its head with the head's absolute
+position, and the track of the output. -/
+structure LocalCfg (k : ℕ) (State : Type) where
+  /-- The control, or `none` when halted. -/
+  state : Option State
+  /-- The input position, as in `Turing.Cfg.inputPos`. -/
+  inputPos : ℕ
+  /-- Every work tape, around its head. -/
+  workTapes : Fin k → BiTape Bool
+  /-- The absolute position of every work head. -/
+  workTapePos : Fin k → ℤ
+  /-- The track of the output. -/
+  track : OutputTrack
+
+variable (machine : MultiTapePTM k Bool State)
+
+/-- The action from a control under a coin: the table's action when running, and the action that
+changes nothing when halted. -/
+@[expose] def coinAction (state : Option State) (symbol : Option Bool)
+    (work : Fin k → Option Bool) (bit : Bool) : Action k Bool State :=
+  match state with
+  | none => ⟨0, fun _ => (none, 0), none, none⟩
+  | some q => MultiTapeMachine.Action.emptyOracleEquiv (machine.tr q symbol work Empty.elim bit)
+
+/-- One coin step on finite storage. -/
+@[expose] def localCoinStep (input : List Bool) (l : LocalCfg k State) (bit : Bool) :
+    LocalCfg k State :=
+  let a := machine.coinAction l.state (inputAt input l.inputPos) (fun h => (l.workTapes h).head) bit
+  { state := a.state
+    inputPos := moveInputPosNat input.length l.inputPos a.inputTape
+    workTapes := fun h => (l.workTapes h).step (a.workTapes h)
+    workTapePos := fun h => l.workTapePos h + (a.workTapes h).2
+    track := l.track.emit a.output }
+
+/-- Replaying coins on finite storage. -/
+@[expose] def localRun (input : List Bool) (coins : List Bool) (l : LocalCfg k State) :
+    LocalCfg k State :=
+  coins.foldl (machine.localCoinStep input) l
+
+/-- Finite storage **represents** a configuration when it has its control, input position, head
+positions and output track, and every work tape holds the configuration's tape around its
+head. -/
+structure LocalCfg.Represents {input : List Bool} (l : LocalCfg k State)
+    (c : Cfg k Bool State input) : Prop where
+  /-- The controls agree. -/
+  state : l.state = c.state
+  /-- The input positions agree. -/
+  inputPos : l.inputPos = c.inputPos.val
+  /-- Every finite work tape holds the configuration's tape around its head. -/
+  workTapes : ∀ h, (l.workTapes h).Represents (c.workTapes h) (c.workTapePos h)
+  /-- The work head positions agree. -/
+  workTapePos : l.workTapePos = c.workTapePos
+  /-- The output track is the track of the configuration's output. -/
+  track : l.track = OutputTrack.ofWord c.output
+
+/-- A coin step of a fair-coin table applies `coinAction`. -/
+theorem withCoin_step_eq (bit : Bool) {input : List Bool} (c : Cfg k Bool State input) :
+    (machine.withCoin bit).toTM.step c =
+      (machine.coinAction c.state c.inputSymbol c.workTapeSymbols bit).apply c := by
+  cases hs : c.state with
+  | none =>
+    rw [MultiTapeTM.step_of_halt hs]
+    simp only [coinAction]
+    refine Cfg.ext ?_ ?_ ?_ ?_ ?_
+    · simp [Action.apply, hs]
+    · simp [Action.apply]
+    · funext h
+      simp [Action.apply]
+    · funext h
+      simp [Action.apply]
+    · simp [Action.apply]
+  | some q =>
+    rw [MultiTapeTM.step_of_state hs]
+    simp only [coinAction, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr]
+    rfl
+
+/-- **A coin step preserves the representation.** -/
+theorem LocalCfg.Represents.localCoinStep {input : List Bool} {l : LocalCfg k State}
+    {c : Cfg k Bool State input} (h : l.Represents c) (bit : Bool) :
+    (machine.localCoinStep input l bit).Represents ((machine.withCoin bit).toTM.step c) := by
+  have hsym : inputAt input l.inputPos = c.inputSymbol := by
+    rw [Cfg.inputSymbol_eq_inputAt, h.inputPos]
+  have hwork : (fun i => (l.workTapes i).head) = c.workTapeSymbols :=
+    funext fun i => (h.workTapes i).head
+  rw [withCoin_step_eq]
+  unfold MultiTapePTM.localCoinStep
+  rw [hsym, hwork, h.state]
+  set a := machine.coinAction c.state c.inputSymbol c.workTapeSymbols bit
+  refine ⟨rfl, ?_, fun i => ?_, ?_, ?_⟩
+  · rw [h.inputPos]
+    exact (val_moveInputPos_eq_moveInputPosNat _ _).symm
+  · have hstep := (h.workTapes i).step (a.workTapes i)
+    rcases hw : (a.workTapes i) with ⟨w, m⟩
+    rw [hw] at hstep
+    cases w <;> simpa [Action.apply, hw] using hstep
+  · funext i
+    simp [Action.apply, h.workTapePos]
+  · simp [Action.apply, h.track, OutputTrack.ofWord_append]
+
+/-- **A replay preserves the representation.** -/
+theorem LocalCfg.Represents.localRun {input : List Bool} {l : LocalCfg k State}
+    {c : Cfg k Bool State input} (h : l.Represents c) (coins : List Bool) :
+    (machine.localRun input coins l).Represents (machine.stepCoins coins c) := by
+  induction coins generalizing l c with
+  | nil => exact h
+  | cons bit coins ih => exact ih (h.localCoinStep machine bit)
+
+/-! ### Reading a configuration's view off finite storage -/
+
+section View
+
+variable (b : ℕ) [NeZero b]
+
+/-- The control record of finite storage: its control, the offset of every head in its block,
+and its output track. -/
+@[expose] def LocalCfg.blockControl (l : LocalCfg k State) : BlockControl k State b :=
+  (l.state, fun head => match head with
+    | none => (((l.inputPos : ℤ) - 1 : ℤ) : ZMod b)
+    | some h => ((l.workTapePos h : ℤ) : ZMod b), l.track)
+
+/-- The block index of every head of finite storage. -/
+@[expose] def LocalCfg.blockIndex (l : LocalCfg k State) : Option (Fin k) → ℤ
+  | none => ((l.inputPos : ℤ) - 1) / b
+  | some h => l.workTapePos h / b
+
+/-- The contents of the windows around block indices `J`, read off finite storage. -/
+@[expose] def LocalCfg.windowContents (J : Option (Fin k) → ℤ) (l : LocalCfg k State) :
+    Fin k → Fin 3 → ZMod b → Option Bool := fun h d r =>
+  (l.workTapes h).read (b * (J (some h) + d - 1) + r.val - l.workTapePos h)
+
+variable {b} {input : List Bool} {l : LocalCfg k State} {c : Cfg k Bool State input}
+
+omit [NeZero b] in
+theorem LocalCfg.Represents.blockControl (h : l.Represents c) :
+    l.blockControl b = c.blockControl b := by
+  simp only [LocalCfg.blockControl, Cfg.blockControl, h.state, h.track, h.inputPos,
+    h.workTapePos]
+  congr 2
+  funext head
+  cases head <;> simp
+
+omit [NeZero b] in
+theorem LocalCfg.Represents.blockIndex (h : l.Represents c) :
+    l.blockIndex b = c.blockIndex b := by
+  funext head
+  cases head <;> simp [LocalCfg.blockIndex, Cfg.blockIndex, h.inputPos, h.workTapePos]
+
+omit [NeZero b] in
+theorem LocalCfg.Represents.windowContents (h : l.Represents c) (J : Option (Fin k) → ℤ) :
+    l.windowContents b J = c.windowContents b J := by
+  funext i d r
+  simp only [LocalCfg.windowContents, Cfg.windowContents, Cfg.blockContents,
+    h.workTapes i _, h.workTapePos]
+  congr 1
+  ring
+
+end View
+
+/-! ### The finite storage of an embedded window -/
+
+section Window
+
+variable (b : ℕ) [NeZero b]
+
+/-- The `3 b` cells of the three blocks of a window, left to right. -/
+@[expose] def windowCells (w : Fin 3 → ZMod b → Option Bool) : List (Option Bool) :=
+  (List.range (3 * b)).map fun c => if hc : c / b < 3 then w ⟨c / b, hc⟩ (c : ZMod b) else none
+
+/-- The finite storage of the configuration embedded at block indices `J` with control record
+`cIn` and window contents `wIn` (`Turing.embedCfg`): each work tape holds the cells of its window
+with its head on cell `b + offset`, in the middle block. -/
+@[expose] def localStart (input : List Bool) (J : Option (Fin k) → ℤ)
+    (cIn : BlockControl k State b) (wIn : Fin k → Fin 3 → ZMod b → Option Bool) :
+    LocalCfg k State where
+  state := cIn.1
+  inputPos := (inputPosOfCoord input (b * J none + (cIn.2.1 none).val)).val
+  workTapes h := BiTape.ofCells (windowCells b (wIn h)) (b + (cIn.2.1 (some h)).val)
+  workTapePos h := b * J (some h) + (cIn.2.1 (some h)).val
+  track := cIn.2.2
+
+/-- The window cells hold the window: the cell at offset `c` from the start of the window is
+entry `c / b` of the window at `c mod b`. -/
+private theorem windowCell_eq (J : Option (Fin k) → ℤ) (w : Fin k → Fin 3 → ZMod b → Option Bool)
+    (h : Fin k) (c : ℤ) :
+    windowCell b J w h (b * (J (some h) - 1) + c) =
+      if 0 ≤ c then (windowCells b (w h)).getD c.toNat none else none := by
+  have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b
+  have hdiv : (b * (J (some h) - 1) + c) / b = J (some h) - 1 + c / b := by
+    rw [add_comm, Int.add_mul_ediv_left _ _ hb.ne', add_comm]
+  unfold windowCell
+  by_cases hc : 0 ≤ c
+  · rw [ite_eq_left hc]
+    have hcn : (c.toNat : ℤ) = c := Int.toNat_of_nonneg hc
+    obtain ⟨d, hd⟩ : ∃ d, d = c.toNat / b := ⟨_, rfl⟩
+    have hcd : c / b = (d : ℤ) := by
+      rw [hd, Int.natCast_div, hcn]
+    by_cases hlt : c.toNat < 3 * b
+    · have hcb : d < 3 := by
+        rw [hd, Nat.div_lt_iff_lt_mul (Nat.pos_of_neZero b)]
+        linarith
+      have hcond : 0 ≤ (b * (J (some h) - 1) + c) / b - J (some h) + 1 ∧
+          (b * (J (some h) - 1) + c) / b - J (some h) + 1 < 3 := by
+        rw [hdiv, hcd]
+        omega
+      have hidx : ((b * (J (some h) - 1) + c) / b - J (some h) + 1).toNat = d := by
+        rw [hdiv, hcd]
+        omega
+      have hcast : (((b * (J (some h) - 1) + c : ℤ)) : ZMod b) = ((c.toNat : ℕ) : ZMod b) := by
+        rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, ZMod.natCast_self, zero_mul, zero_add,
+          ← Int.cast_natCast, hcn]
+      rw [dite_eq_left hcond, windowCells, List.getD_eq_getElem?_getD, List.getElem?_map,
+        List.getElem?_range hlt, Option.map_some, Option.getD_some, ← hd, dite_eq_left hcb,
+        hcast]
+      simp only [hidx]
+    · have hlen : (windowCells b (w h)).length ≤ c.toNat := by
+        simp only [windowCells, List.length_map, List.length_range]
+        omega
+      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none hlen]
+      have : 3 ≤ c / b := by
+        rw [hcd]
+        have : 3 ≤ d := hd ▸ (Nat.le_div_iff_mul_le (Nat.pos_of_neZero b)).mpr (by omega)
+        omega
+      rw [dite_eq_right (by rw [hdiv]; omega)]
+      rfl
+  · rw [ite_eq_right hc]
+    have : c / b < 0 := Int.ediv_neg_of_neg_of_pos (by omega) hb
+    exact dite_eq_right (by rw [hdiv]; omega)
+
+/-- **The finite storage of an embedded window represents it.** -/
+theorem represents_localStart (input : List Bool) (J : Option (Fin k) → ℤ)
+    (cIn : BlockControl k State b) (wIn : Fin k → Fin 3 → ZMod b → Option Bool) :
+    (localStart b input J cIn wIn).Represents (embedCfg (input := input) b J cIn wIn) := by
+  refine ⟨rfl, rfl, fun h z => ?_, rfl, (OutputTrack.ofWord_toWord _).symm⟩
+  rw [localStart, BiTape.read_ofCells]
+  change _ = windowCell b J wIn h (b * J (some h) + (cIn.2.1 (some h)).val + z)
+  rw [show (b : ℤ) * J (some h) + (cIn.2.1 (some h)).val + z =
+      b * (J (some h) - 1) + (((b + (cIn.2.1 (some h)).val : ℕ) : ℤ) + z) by push_cast; ring,
+    windowCell_eq]
+
+end Window
+
+/-! ### Interval steps by finite simulation -/
+
+section Interval
+
+variable (b : ℕ) [NeZero b]
+
+/-- **The interval condition on finite storage**: replaying `coins` on the finite storage of the
+embedded window leaves the control record `cOut` and the window contents `wOut`, and moves the
+block of every head `h` by `δ h`. -/
+@[expose] def LocalIntervalStep (input : List Bool) (J : Option (Fin k) → ℤ)
+    (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
+    (wIn : Fin k → Fin 3 → ZMod b → Option Bool) (coins : List Bool)
+    (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : Prop :=
+  (machine.localRun input coins (localStart b input J cIn wIn)).blockControl b = cOut ∧
+    (machine.localRun input coins (localStart b input J cIn wIn)).windowContents b J = wOut ∧
+    ∀ head, (machine.localRun input coins (localStart b input J cIn wIn)).blockIndex b head =
+      J head + δ head
+
+instance [DecidableEq State] (input : List Bool) (J : Option (Fin k) → ℤ)
+    (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
+    (wIn : Fin k → Fin 3 → ZMod b → Option Bool) (coins : List Bool)
+    (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) :
+    Decidable (machine.LocalIntervalStep b input J δ cIn wIn coins cOut wOut) := by
+  unfold LocalIntervalStep
+  infer_instance
+
+/-- **Interval steps are decided by finite simulation.** -/
+theorem intervalStep_iff_localIntervalStep (input : List Bool) (J : Option (Fin k) → ℤ)
+    (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
+    (wIn : Fin k → Fin 3 → ZMod b → Option Bool) (coins : List Bool)
+    (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) :
+    machine.IntervalStep b input J δ cIn wIn coins cOut wOut ↔
+      machine.LocalIntervalStep b input J δ cIn wIn coins cOut wOut := by
+  have h := (represents_localStart b input J cIn wIn).localRun machine coins
+  simp only [IntervalStep, LocalIntervalStep, h.blockControl, h.windowContents,
+    h.blockIndex]
+
+open scoped Classical in
+/-- **Interval tensors by finite simulation**: the interval tensor counts the bit strings that
+satisfy the interval condition on finite storage. -/
+theorem intervalCount_eq_card_localIntervalStep (input : List Bool) (J : Option (Fin k) → ℤ)
+    (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
+    (wIn : Fin k → Fin 3 → ZMod b → Option Bool)
+    (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) :
+    machine.intervalCount b input J δ cIn wIn cOut wOut =
+      (Finset.univ.filter fun u : Fin b → Bool =>
+        machine.LocalIntervalStep b input J δ cIn wIn (List.ofFn u) cOut wOut).card := by
+  unfold intervalCount
+  congr 1
+  ext u
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and,
+    intervalStep_iff_localIntervalStep]
+
+end Interval
+
+end Turing.MultiTapePTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean
index 18eaa4a01..2d81fe6ad 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean
@@ -238,8 +238,9 @@ variable (b : ℕ) [NeZero b]
 /-- **An interval step.** Replaying `coins` from the configuration embedded at block indices `J`
 with entering control record `cIn` and window contents `wIn` leaves the control record `cOut`,
 the contents `wOut` of the same windows, and moves the block of every head `h` by `δ h`. -/
-def IntervalStep (input : List Bool) (J : Option (Fin k) → ℤ) (δ : Option (Fin k) → SignType)
-    (cIn : BlockControl k State b) (wIn : Fin k → Fin 3 → ZMod b → Option Bool)
+@[expose] def IntervalStep (input : List Bool) (J : Option (Fin k) → ℤ)
+    (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
+    (wIn : Fin k → Fin 3 → ZMod b → Option Bool)
     (coins : List Bool) (cOut : BlockControl k State b)
     (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : Prop :=
   (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).blockControl b = cOut ∧
@@ -252,7 +253,7 @@ open scoped Classical in
 step from the entering record `cIn` and contents `wIn` at block indices `J` to the leaving record
 `cOut` and contents `wOut`, moving the blocks by `δ`. This is the entry `F_i` of the note's
 equation (3). -/
-noncomputable def intervalCount (input : List Bool) (J : Option (Fin k) → ℤ)
+@[expose] noncomputable def intervalCount (input : List Bool) (J : Option (Fin k) → ℤ)
     (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b)
     (wIn : Fin k → Fin 3 → ZMod b → Option Bool)
     (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : ℕ :=
diff --git a/Complexity/Foundations/Data/BiTape/OfCells.lean b/Complexity/Foundations/Data/BiTape/OfCells.lean
new file mode 100644
index 000000000..fa63005b2
--- /dev/null
+++ b/Complexity/Foundations/Data/BiTape/OfCells.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Data.BiTape
+
+/-!
+# Tapes holding a finite list of cells
+
+`Cslib.Turing.BiTape.ofCells cells pos` is the tape that holds the list `cells` of optional
+symbols, blanks allowed anywhere, with its head on cell `pos`: cell `i` of the list is at
+displacement `i - pos` from the head and every other cell is blank
+(`Cslib.Turing.BiTape.read_ofCells`). It loads a finite window of a tape, such as the blocks
+around a head, into finite storage.
+
+## Main definitions
+
+* `Cslib.Turing.BiTape.ofCells`: the tape holding a list of cells.
+
+## Main results
+
+* `Cslib.Turing.StackTape.read_ofList`: a stack tape built from a list reads the list.
+* `Cslib.Turing.BiTape.read_ofCells`: the cells of the tape.
+-/
+
+public section
+
+namespace Cslib.Turing
+
+namespace StackTape
+
+variable {Symbol : Type*}
+
+/-- A stack tape built from a list reads the list, and blank past its end. -/
+@[simp] lemma read_ofList (l : List (Option Symbol)) (position : ℕ) :
+    (ofList l).read position = l.getD position none := by
+  induction l generalizing position with
+  | nil => simp
+  | cons a l ih =>
+    cases position with
+    | zero => simp [head_cons]
+    | succ position => simp [tail_cons, ih]
+
+end StackTape
+
+namespace BiTape
+
+variable {Symbol : Type*}
+
+/-- The tape holding `cells` with its head on cell `pos`: cell `i` of `cells` is at displacement
+`i - pos` from the head, and every other cell is blank. -/
+@[expose] def ofCells (cells : List (Option Symbol)) (pos : ℕ) : BiTape Symbol :=
+  ⟨cells.getD pos none,
+    StackTape.ofList ((List.range pos).map fun i => cells.getD (pos - 1 - i) none),
+    StackTape.ofList (cells.drop (pos + 1))⟩
+
+/-- **The cells of `ofCells cells pos`**: the cell at displacement `z` is cell `pos + z` of
+`cells`, blank when that is negative or past the end. -/
+lemma read_ofCells (cells : List (Option Symbol)) (pos : ℕ) (z : ℤ) :
+    (ofCells cells pos).read z =
+      if 0 ≤ (pos : ℤ) + z then cells.getD ((pos : ℤ) + z).toNat none else none := by
+  rcases z with (_ | n) | n
+  · simp [read, ofCells]
+  · have h : ((pos : ℤ) + Int.ofNat (n + 1)).toNat = pos + 1 + n := by
+      simp only [Int.ofNat_eq_natCast]
+      omega
+    have h0 : 0 ≤ (pos : ℤ) + Int.ofNat (n + 1) := by
+      simp only [Int.ofNat_eq_natCast]
+      omega
+    simp only [h0, ↓reduceIte, h]
+    simp [read, ofCells, List.getD_eq_getElem?_getD, List.getElem?_drop]
+  · simp only [read, ofCells, StackTape.read_ofList, List.getD_eq_getElem?_getD,
+      List.getElem?_map]
+    by_cases hn : n < pos
+    · have h : ((pos : ℤ) + Int.negSucc n).toNat = pos - 1 - n := by
+        simp only [Int.negSucc_eq]
+        omega
+      have h0 : 0 ≤ (pos : ℤ) + Int.negSucc n := by
+        simp only [Int.negSucc_eq]
+        omega
+      simp only [h0, ↓reduceIte, h, List.getElem?_range hn]
+      rfl
+    · have h0 : ¬ 0 ≤ (pos : ℤ) + Int.negSucc n := by
+        simp only [Int.negSucc_eq]
+        omega
+      simp only [h0, ↓reduceIte,
+        List.getElem?_eq_none (by simpa using hn : (List.range pos).length ≤ n)]
+      rfl
+
+end BiTape
+
+end Cslib.Turing
diff --git a/ComplexityTests/HPVIntervalSimulation.lean b/ComplexityTests/HPVIntervalSimulation.lean
new file mode 100644
index 000000000..bd65757af
--- /dev/null
+++ b/ComplexityTests/HPVIntervalSimulation.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalSimulation
+
+/-! Interval steps of a concrete fair-coin machine, decided by finite simulation: the finite
+storage of an embedded window is evaluated, and the semantic interval step follows. -/
+
+namespace ComplexityTests.HPVIntervalSimulation
+
+open Turing MultiTapeMachine MultiTapePTM MultiTapeNTM.ChoiceTable Cslib.Turing
+
+/-- On one work tape, write every coin and move right; the input head moves right too. The first
+step emits its coin; then the machine keeps walking without output. -/
+private def walk : MultiTapePTM 1 Bool Bool where
+  initial := false
+  tr state _ _ _ bit := .step
+    { inputTape := 1,
+      workTapes := fun _ => (some (some bit), 1),
+      output := if state then none else some bit, state := some true }
+    Empty.elim Empty.elim
+
+/-- The blocks of the start: every head in block `0` at offset `0`. -/
+private def J₀ : Option (Fin 1) → ℤ := fun _ => 0
+
+/-- The start record: state `false`, offsets `0`, nothing emitted. -/
+private def c₀ : BlockControl 1 Bool 2 := (some false, fun _ => 0, .empty)
+
+/-- After the coins `true, false`: state `true`; the input head at coordinate `1` (clamped at the
+right end cell of the one-symbol input), offset `1`; the work head at `2`, offset `0` in block
+`1`; and the emitted word `[true]`. -/
+private def c₁ : BlockControl 1 Bool 2 :=
+  (some true, fun head => match head with | none => 1 | some _ => 0, .accept)
+
+/-- The work tape after the coins `true, false`: the middle block holds them. -/
+private def w₁ : Fin 1 → Fin 3 → ZMod 2 → Option Bool := fun _ d r =>
+  if d = 1 then some (r = 0) else none
+
+/-- The blocks move: the input head stays in block `0`, the work head moves to block `1`. -/
+private def δ₁ : Option (Fin 1) → SignType := fun head => match head with | none => 0 | some _ => 1
+
+-- The finite simulation decides the interval condition by evaluation.
+example : walk.LocalIntervalStep 2 [true] J₀ δ₁ c₀ (fun _ _ _ => none) [true, false] c₁ w₁ := by
+  decide
+
+-- A different leaving record (output track `other`) fails.
+example : ¬ walk.LocalIntervalStep 2 [true] J₀ δ₁ c₀ (fun _ _ _ => none) [true, false]
+    (some true, fun head => match head with | none => 1 | some _ => 0, .other) w₁ := by
+  decide
+
+-- So the semantic interval step on the integer-indexed tapes holds.
+example : walk.IntervalStep 2 [true] J₀ δ₁ c₀ (fun _ _ _ => none) [true, false] c₁ w₁ :=
+  (walk.intervalStep_iff_localIntervalStep 2 _ _ _ _ _ _ _ _).mpr (by decide)
+
+end ComplexityTests.HPVIntervalSimulation