Direct primitives for plain degree bounds

These rules retain independent cost and encoded-output degrees. Constants have cost degree one and output degree zero; encoded equality uses the upstream copy machine. Output and input encoding transports reuse the same realizing machine and preserve both degrees, including zero. No higher computability calculus is used in their proofs.

Main results

• Turing.MultiTapeTM.ComputableInDegree.const: a constant encoded result.
• Turing.MultiTapeTM.ComputableInDegree.of_finite: a function on any finite input type.
• Turing.MultiTapeTM.ComputableInDegree.of_eq: copy an unchanged encoded word.
• Turing.MultiTapeTM.ComputableInDegree.of_enc_eq, .of_encIn_eq: transport encoded equality.

References

Uses cslib's constant and copy machines and the independent degree bounds of this library.

theorem Turing.MultiTapeTM.ComputableInDegree.const {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableInDegree (fun (x : α) => b) encIn encMid 1 0

A fixed encoded result has linear cost and constant encoded-output growth.

theorem Turing.MultiTapeTM.ComputableInDegree.of_finite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} [Finite α] (f : α → β) : ComputableInDegree f encIn encMid 1 0

A function on a finite input type has linear cost and constant output growth. The machine has constant time and zero workspace; no inhabitedness assumption is needed.

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

Copy a word whose output encoding is exactly its input encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.of_enc_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {d e : ℕ} {f : α → β} {g : α → γ} (hf : ComputableInDegree f encIn encMid d e) (h : ∀ (a : α), encOut (g a) = encMid (f a)) : ComputableInDegree g encIn encOut d e

Equal output words retain the realizing machine and both independent degrees.

theorem Turing.MultiTapeTM.ComputableInDegree.of_encIn_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d e : ℕ} {α' : Type u_4} {encIn' : α' ↪ List Bool} {f : α → β} (map : α' → α) (henc : ∀ (a : α'), encIn' a = encIn (map a)) (hf : ComputableInDegree f encIn encMid d e) : ComputableInDegree (f ∘ map) encIn' encMid d e

An input map preserving the complete encoded word retains the same machine and degrees. The semantic map needs no separate computational assumption: the machine sees the same word.

theorem Turing.MultiTapeTM.ComputableInDegree.restrict {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d e : ℕ} {f : α → β} (h : ComputableInDegree f encIn encMid d e) (p : α → Prop) : ComputableInDegree (f ∘ Subtype.val) ((Function.Embedding.subtype p).trans encIn) encMid d e

Restricting inputs preserves the same machine and both degrees.