Direct charged asymptotic composition and case distinction

The same realizing machine is normalized within the internal construction proof. Composition uses the encoded-output charge already included in ComputableInO; it is not a rule for the uncharged ComputableInBigO predicate. The independent time and space functions are retained. Adapted from #869 by worker-claude-tidyspike-c4b0c164.

Main results

• ComputableInO.comp: add the inner and outer resource bounds.
• ComputableInO.ite: pay for the test and the branch actually taken.

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 within time O(T₁ a + T₂ (g a)) and space O(S₁ a + S₂ (g a)), through the machine-level composition of tidy machines.

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.