Direct linear capabilities used by codecs

The witnesses normalize only realizing machines. No higher tidy computability rule is used.

theorem Turing.MultiTapeTM.ComputableInDegree.of_cons_true {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = true :: encIn a) : ComputableInDegree f encIn encMid 1 1

Prepend the marker of the existing option encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.of_tail {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = (encIn a).tail) : ComputableInDegree f encIn encMid 1 1

Drop the input word's first symbol using the existing head machine.

theorem Turing.MultiTapeTM.ComputableInDegree.of_take_one {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = List.take 1 (encIn a)) : ComputableInDegree f encIn encMid 1 1

Keep the input word's first symbol using the existing head machine.

theorem Turing.MultiTapeTM.ComputableInDegree.of_isEmpty {α : Type u_1} {encIn : α ↪ List Bool} {f : α → Bool} (h : ∀ (a : α), f a = (encIn a).isEmpty) : ComputableInDegree f encIn encBool 1 1

Test the encoded input for emptiness using the existing finite transducer.

theorem Turing.MultiTapeTM.ComputableInDegree.of_isEmpty_ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (d : β) (hd : ∀ (a : α), encIn a = [] → f a = d) (h : ComputableInDegree (f ∘ Subtype.val) ((Function.Embedding.subtype fun (a : α) => (encIn a).isEmpty = false).trans encIn) encMid 1 1) : ComputableInDegree f encIn encMid 1 1

A fixed default on the empty word and a linear certificate on nonempty encoded inputs.