Asymptotic composition with explicit intermediate storage

The same realizing machine is normalized within the internal construction proof. Composition first accounts for the stored intermediate word explicitly in ComputableInBigO. The charged ComputableInO rule then absorbs that word using its separate output-growth bound. The independent time and space functions are retained. Adapted from #869 by worker-claude-tidyspike-c4b0c164.

Main results

• ComputableInBigO.comp: materializing composition with explicit intermediate storage.
• ComputableInO.comp: absorb intermediate storage using the output-growth bound.
• ComputableInO.ite: pay for the test and the branch actually taken.

theorem Turing.MultiTapeTM.ComputableInBigO.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂ : β → ℕ} (hf : ComputableInBigO f encMid encOut T₂ S₂) (hg : ComputableInBigO g encIn encMid T₁ S₁) : ComputableInBigO (f ∘ g) encIn encOut (fun (a : α) => T₁ a + T₂ (g a)) fun (a : α) => S₁ a + S₂ (g a) + (encMid (g a)).length

Materializing composition stores the inner encoded output on a work tape. Its length is charged explicitly to workspace; no output-growth hypothesis is needed. The copying time is already bounded by the inner runtime. This is not the recomputing small-space composition rule.

theorem Turing.MultiTapeTM.ComputableInO.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂ : β → ℕ} (hf : ComputableInO f encMid encOut T₂ S₂) (hg : ComputableInO g encIn encMid T₁ S₁) : ComputableInO (f ∘ g) encIn encOut (fun (a : α) => T₁ a + T₂ (g a)) fun (a : α) => S₁ a + S₂ (g a)

Composition absorbs the stored intermediate word using the inner output-growth bound, retaining time O(T₁ a + T₂ (g a)) and space O(S₁ a + S₂ (g a)).

theorem Turing.MultiTapeTM.ComputableInO.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} {Tc Tf Tg Sc Sf Sg : α → ℕ} (hc : ComputableInO c encIn encC Tc Sc) (hf : ComputableInO f encIn encMid Tf Sf) (hg : ComputableInO g encIn encMid Tg Sg) : ComputableInO (fun (x : α) => if c x = true then f x else g x) encIn encMid (fun (x : α) => Tc x + if c x = true then Tf x else Tg x) fun (x : α) => Sc x + if c x = true then Sf x else Sg x

Case distinction within the bounds of the test plus those of the branch taken, through the explicit-bound case-distinction combinator.