Direct degree bounds from encoding capabilities

Pair projections reuse the degree certificates supplied by the encoding capability.

theorem Turing.MultiTapeTM.ComputableInDegree.fst {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInDegree Prod.fst (encPair enc₁ enc₂) enc₁ 1 1

The first component of a standard framed pair.

theorem Turing.MultiTapeTM.ComputableInDegree.snd {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInDegree Prod.snd (encPair enc₁ enc₂) enc₂ 1 1

The second component of a standard framed pair.

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.