Direct degree bounds from encoding machines

Pair projections unpack the encoding capability's machine witness directly. The temporary linear encoding fields are used only as machine constructors; no higher tidy degree or polynomial-time calculus is used. Both cost and output retain degree one.

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

The first framed component is computable with linear cost and output growth.

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

The second framed component is computable with linear cost and output growth.