Direct degree certificates for option encoding machines

Construction and fixed-default elimination unpack the existing encoding capability's machine witness. The temporary raw-linear encoding fields supply machine constructors only; no higher tidy degree, polynomial-time, or linear closure rule is used.

theorem Turing.MultiTapeTM.ComputableInDegree.optionSome {β : Type u_1} {enc₁ : β ↪ List Bool} {enc : Option β ↪ List Bool} [OptionEncoding enc₁ enc] : ComputableInDegree some enc₁ enc 1 1

Construct an optional value in an encoding with the option capability.

theorem Turing.MultiTapeTM.ComputableInDegree.getD {β : Type u_1} {enc₁ : β ↪ List Bool} {enc : Option β ↪ List Bool} [OptionEncoding enc₁ enc] (d : β) : ComputableInDegree (fun (o : Option β) => o.getD d) enc enc₁ 1 1

Eliminate an optional value using a fixed default, without a nonempty-type assumption.

theorem Turing.MultiTapeTM.ComputableInDegree.isSome {β : Type u_1} (enc : β ↪ List Bool) : ComputableInDegree (fun (o : Option β) => o.isSome) (encOption enc) encBool 1 0

Whether a standard encoded option holds a value; the Boolean output has degree zero.