Direct closure of independent degree bounds

These constructions combine machine witnesses, retaining independent resource and encoded-output degrees, including degree zero. No higher tidy asymptotic calculus is used.

theorem Turing.MultiTapeTM.ComputableInDegree.append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {d₁ e₁ d₂ e₂ : ℕ} {enc₂ : δ ↪ List Bool} {f₁ : α → β} {f₂ : α → δ} {g : α → γ} (h₁ : ComputableInDegree f₁ encIn encMid d₁ e₁) (h₂ : ComputableInDegree f₂ encIn enc₂ d₂ e₂) (hg : ∀ (x : α), encOut (g x) = encMid (f₁ x) ++ enc₂ (f₂ x)) : ComputableInDegree g encIn encOut (max d₁ d₂) (max e₁ e₂)

Concatenate encoded outputs without merging their independent cost and output degrees.

theorem Turing.MultiTapeTM.ComputableInDegree.pair {d₁ e₁ d₂ e₂ : ℕ} {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [hP : PairEncoding enc₁ enc₂ enc] {f : α → β₁} {g : α → β₂} (hf : ComputableInDegree f encIn enc₁ d₁ e₁) (hg : ComputableInDegree g encIn enc₂ d₂ e₂) : ComputableInDegree (fun (x : α) => (f x, g x)) encIn enc (max d₁ d₂) (max d₁ d₂)

Generic pairing retains the resource degree as its encoded-output bound.

theorem Turing.MultiTapeTM.ComputableInDegree.prod {d₁ e₁ d₂ e₂ : ℕ} {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁} {g : α → β₂} (hf : ComputableInDegree f encIn enc₁ d₁ e₁) (hg : ComputableInDegree g encIn enc₂ d₂ e₂) : ComputableInDegree (fun (x : α) => (f x, g x)) encIn (encPair enc₁ enc₂) (max d₁ d₂) (max e₁ e₂)

Framed pairing retains the independent encoded-output degrees.

theorem Turing.MultiTapeTM.ComputableInDegree.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d₁ e₁ d₂ e₂ : ℕ} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} {dc ec : ℕ} (hc : ComputableInDegree c encIn encC dc ec) (hf : ComputableInDegree (f ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = true).trans encIn) encMid d₁ e₁) (hg : ComputableInDegree (g ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = false).trans encIn) encMid d₂ e₂) : ComputableInDegree (fun (x : α) => if c x = true then f x else g x) encIn encMid (max dc (max d₁ d₂)) (max e₁ e₂)

Case distinction retains independent branch output degrees, including zero.