Direct degree certificates for option encoding machines

Construction and fixed-default elimination reuse the encoding capability's degree certificates. The Boolean test retains its constant output degree. No higher tidy calculus 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.

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.