Round-independent workspace bounds for repeatUntilBlank

Every round of a RunsWords phase starts from a wordsCfg (where every work-tape head sits at position 0), runs for at most t steps (moving each head by at most 1 cell per step, so all heads stay in window t), and halts in a wordsCfg (returning all work-tape heads back to 0). Repeating such a phase any number of rounds via Turing.MultiTapePTM.repeatUntilBlank therefore keeps every work-tape head inside window t along every prefix of every branch, regardless of how large rounds is.

Main results

• Turing.MultiTapePTM.workTapePos_runsWords_mem_window: a closed RunsWords phase of time t keeps every work-tape head in window t along every fixed-coin replay.
• Turing.MultiTapePTM.workTapePos_repeatUntilBlank_mem_window: repeatUntilBlank of a closed RunsWords loop body of per-round time t keeps every work-tape head in window t for any number of rounds.
• Turing.MultiTapePTM.runsInSpace_toNTM_seq_repeatUntilBlank: sequencing an initial RunsWords preparation (t₁), repeatUntilBlank (t per round), and a final RunsWords phase (t₂) runs in nondeterministic workspace k * (2 * max t₁ (max t t₂) + 1), independent of rounds.

theorem Turing.MultiTapePTM.runOracleConfigFrom_empty {k : ℕ} {State : Type} {x : List Bool} (M : MultiTapePTM k Bool State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Bool State Empty x) : M.runOracleConfigFrom fuel cfg = Cslib.ProbOracleComp.sample (M.runClosedConfigFrom fuel cfg)

Running an oracle configuration with an Empty operation signature samples its closed run.

theorem Turing.MultiTapePTM.workTapePos_runsWords_mem_window {k : ℕ} {State : Type} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {t : ℕ} {α : Type} {prog : Cslib.ProbOracleComp (fun (x : Empty × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (M : MultiTapePTM k Bool State) (h : M.RunsWords x ws₀ out₀ t prog ws₁ emit) (cfg : MultiTapeMachine.Config k Bool State Empty x) (htapes : cfg.tapes = wordsCfg x (some M.initial) ws₀ out₀) (coins : List Bool) (j : Fin k) : (M.runClosedConfigFromCoins coins cfg).tapes.workTapePos j ∈ window t

Along any fixed-coin replay of a closed RunsWords phase of step bound t, every work-tape head remains in window t.

theorem Turing.MultiTapePTM.workTapePos_repeatUntilBlank_mem_window {k : ℕ} {State : Type} {x : List Bool} (i : Fin k) {body : MultiTapePTM k Bool State} {σ : Type} {ws : σ → Fin k → List Bool} {step last : σ → Cslib.ProbOracleComp (fun (x : Empty × List Bool) => List Bool) σ} {out₀ : List Bool} {t rounds : ℕ} {s₀ : σ} (invariant : ℕ → σ → Prop) (hbase : invariant 0 s₀) (hstep : ∀ n < rounds, ∀ (s : σ), invariant n s → body.RunsWords x (ws s) out₀ t (step s) ws fun (x : σ) => []) (hlast : ∀ (s : σ), invariant rounds s → body.RunsWords x (ws s) out₀ t (last s) ws fun (x : σ) => []) (hpreserve : ∀ n < rounds, ∀ (s : σ), invariant n s → ∀ (OracleState : Type) (oracle : Empty × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ (Cslib.ProbOracleComp.runWith oracle (step s) st).support → invariant (n + 1) s' ∧ ws s' i ≠ []) (hstop : ∀ (s : σ), invariant rounds s → ∀ (OracleState : Type) (oracle : Empty × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ (Cslib.ProbOracleComp.runWith oracle (last s) st).support → ws s' i = []) (cfg₀ : MultiTapeMachine.Config k Bool State Empty x) (hcfg₀ : cfg₀.tapes = wordsCfg x (some body.initial) (ws s₀) out₀) (coins : List Bool) (j : Fin k) : ((repeatUntilBlank i body).runClosedConfigFromCoins coins (RepeatUntilBlank.runConfig cfg₀)).tapes.workTapePos j ∈ window t

Round-independent head window for repeatUntilBlank. Under the closed RunsWords invariants of RunsWords.repeatUntilBlank with per-round step bound t, every fixed-coin replay of repeatUntilBlank i body keeps every work-tape head inside window t, for any rounds.

theorem Turing.MultiTapePTM.runsInSpace_toNTM_seq_repeatUntilBlank {k : ℕ} {x : List Bool} {S₀ S₁ S₂ : Type} (i : Fin k) (first : MultiTapePTM k Bool S₀) (body : MultiTapePTM k Bool S₁) (lastM : MultiTapePTM k Bool S₂) {σ : Type} {ws : σ → Fin k → List Bool} (hws : Function.Injective ws) {step last : σ → Cslib.ProbOracleComp (fun (x : Empty × List Bool) => List Bool) σ} {emitFinal : σ → List Bool} {t₁ t t₂ rounds : ℕ} {s₀ : σ} (hfirst : first.RunsWords x (fun (x : Fin k) => []) [] t₁ (pure ()) (fun (x : Unit) => ws s₀) fun (x : Unit) => []) (invariant : ℕ → σ → Prop) (hbase : invariant 0 s₀) (hstep : ∀ n < rounds, ∀ (s : σ), invariant n s → body.RunsWords x (ws s) [] t (step s) ws fun (x : σ) => []) (hlast : ∀ (s : σ), invariant rounds s → body.RunsWords x (ws s) [] t (last s) ws fun (x : σ) => []) (hpreserve : ∀ n < rounds, ∀ (s : σ), invariant n s → ∀ (OracleState : Type) (oracle : Empty × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ (Cslib.ProbOracleComp.runWith oracle (step s) st).support → invariant (n + 1) s' ∧ ws s' i ≠ []) (hstop : ∀ (s : σ), invariant rounds s → ∀ (OracleState : Type) (oracle : Empty × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s' : σ), (s', st') ∈ (Cslib.ProbOracleComp.runWith oracle (last s) st).support → ws s' i = []) (hlastM : ∀ (OracleState : Type) (oracle : Empty × List Bool → StateT OracleState PMF (List Bool)) (st st' : OracleState) (s : σ), (s, st') ∈ (Cslib.ProbOracleComp.runWith oracle (Cslib.OracleComp.iterate rounds step s₀ >>= last) st).support → lastM.RunsWords x (ws s) [] t₂ (pure ()) (fun (x : Unit) (x_1 : Fin k) => []) fun (x : Unit) => emitFinal s) : (first.seq ((repeatUntilBlank i body).seq lastM)).toNTM.RunsInSpace x (k * (2 * max t₁ (max t t₂) + 1))

Workspace bound for first.seq ((repeatUntilBlank i body).seq last). When first (t₁), each round of body (t), and last (t₂) satisfy closed RunsWords specifications, the combined machine visits at most k * (2 * max t₁ (max t t₂) + 1) work-tape cells on x, independently of rounds.