Direct charged iteration with a binary counter

A normalized plain round machine is iterated by the exact machine-level loop combinator. The same realizing machines retain independent time/workspace and complete encoded-output charges. Only actual trajectory states up to and including the final round must satisfy the given bounds. No unary representation of the runtime count is materialized.

theorem Turing.MultiTapeTM.ComputableInO.countStep_inO {β : Type} [Inhabited β] {encB : β ↪ List Bool} {step : β → β} {Ts Ss : β → ℕ} (hstep : ComputableInO step encB encB Ts Ss) : ComputableInO (Internal.BinaryCounter.countStep step) (encOption (encPair encNat encB)) (encOption (encPair encNat encB)) (fun (o : Option (ℕ × β)) => ((encOption (encPair encNat encB)) o).length + ((encNat (o.getD default).1).length + 1) ^ 2 + Ts (o.getD default).2) fun (o : Option (ℕ × β)) => ((encOption (encPair encNat encB)) o).length + Ss (o.getD default).2

A round of the counted iteration.

theorem Turing.MultiTapeTM.ComputableInO.iterate {γ β : Type} [Inhabited β] {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {n : γ → ℕ} {init : γ → β} {step : β → β} {Tn Ti Sn Si R Q B : γ → ℕ} {Ts Ss : β → ℕ} (hn : ComputableInO n encIn encNat Tn Sn) (hinit : ComputableInO init encIn encB Ti Si) (hstep : ComputableInO step encB encB Ts Ss) (hround : ∀ (x : γ), ∀ k ≤ n x, Ts (step^[k] (init x)) ≤ R x) (hspace : ∀ (x : γ), ∀ k ≤ n x, Ss (step^[k] (init x)) ≤ Q x) (hstate : ∀ (x : γ), ∀ k ≤ n x, (encB (step^[k] (init x))).length ≤ B x) : ComputableInO (fun (x : γ) => step^[n x] (init x)) encIn encB (fun (x : γ) => Tn x + Ti x + (n x + 1) * (R x + B x + ((encNat (n x)).length + 1) ^ 2)) fun (x : γ) => Sn x + Si x + Q x + B x + (encNat (n x)).length

Iterating n x times, with n x in binary. If the rounds are within the time R x and the space Q x, and the iterates have length at most B x, the iteration takes the time of the counter and of the start, plus R x, B x and the square of the length of the counter for every round, and the space of the counter and of the start, plus Q x, B x and the length of the counter.