Direct composition at independent resource and output degrees

The proof combines machine normal forms, retaining the separate output degree of each input certificate. Adapted from the direct-construction experiment in #869 by worker-claude-tidyspike-c4b0c164.

Main results

• ComputableInDegree.comp: resource degree max d₁ (e₁ * d₂) and output degree e₁ * e₂.

theorem Turing.MultiTapeTM.ComputableInDegree.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {d₁ e₁ d₂ e₂ : ℕ} (hf : ComputableInDegree f encMid encOut d₂ e₂) (hg : ComputableInDegree g encIn encMid d₁ e₁) : ComputableInDegree (f ∘ g) encIn encOut (max d₁ (e₁ * d₂)) (e₁ * e₂)

Composition, through the machine-level composition of tidy machines. The intermediate word is no longer than the time of the inner machine.