Direct charged folds with full reachable-prefix bounds

The original independent time/workspace formulas are retained. Each plain input certificate supplies its own normalized machine within the internal construction; no higher tidy O calculus is imported or used. The state invariant applies only to actual reachable prefixes.

Main results

• ComputableInO.foldl: independent callback time/workspace bounds and a full prefix invariant.
• ComputableInO.foldlWith: the same with an encoded runtime parameter retained in state.

theorem Turing.MultiTapeTM.ComputableInO.foldl {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} {Tl Ti Sl Si R Q B : γ → ℕ} {Ts Ss : β × α → ℕ} (hlist : ComputableInO list encIn encL Tl Sl) (hinit : ComputableInO init encIn encB Ti Si) (hstep : ComputableInO (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB Ts Ss) (hround : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ts (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ R x) (hspace : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ss (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ Q x) (hstate : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableInO (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (fun (x : γ) => Tl x + Ti x + ((list x).length + 1) * (R x + B x + (encL (list x)).length)) fun (x : γ) => Sl x + Si x + Q x + B x + (encL (list x)).length

Left folds within given bounds. If every round is within the time R x and the space Q x, and every state has length at most B x, a fold takes the time of the list and of the initial state, plus R x, B x and the length of the encoded list for every round, and the space of the list and of the initial state, plus Q x, B x and the length of the encoded list once.

theorem Turing.MultiTapeTM.ComputableInO.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} {Tp Tl Ti Sp Sl Si R Q B : γ → ℕ} {Ts Ss : (π × β) × α → ℕ} (hpar : ComputableInO par encIn encP Tp Sp) (hlist : ComputableInO list encIn encL Tl Sl) (hinit : ComputableInO init encIn encB Ti Si) (hstep : ComputableInO (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB Ts Ss) (hround : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ts ((par x, List.foldl (step (par x)) (init x) (List.take i (list x))), (list x)[i]) ≤ R x) (hspace : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ss ((par x, List.foldl (step (par x)) (init x) (List.take i (list x))), (list x)[i]) ≤ Q x) (hstate : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableInO (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB (fun (x : γ) => Tp x + Tl x + Ti x + ((list x).length + 1) * (R x + B x + (encP (par x)).length + (encL (list x)).length)) fun (x : γ) => Sp x + Sl x + Si x + Q x + B x + (encP (par x)).length + (encL (list x)).length

Left folds with a parameter, within given bounds. The step may depend on a parameter par x, which is kept in the state.