Direct degree weakening and polynomial-time consequences

The original three plain rules are moved unchanged from the degree-calculus module to keep ordinary clients independent of its legacy construction calculus.

Charged ComputableInO bounds also give degree certificates: a lower workspace degree bounds encoded output at that lower degree, even when the time bound has a higher degree.

theorem Turing.MultiTapeTM.ComputableInDegree.mono {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {d e d' e' : ℕ} (h : ComputableInDegree f encIn encOut d e) (hd : d ≤ d' := by first | decide | omega) (he : e ≤ e' := by first | decide | omega) : ComputableInDegree f encIn encOut d' e'

Increasing either degree retains the same realizing machine.

theorem Turing.MultiTapeTM.ComputableInDegree.of_bounds {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {d : ℕ} {t s : α → ℕ} (ht : DegreeBounded (fun (a : α) => (encIn a).length) t d) (hs : DegreeBounded (fun (a : α) => (encIn a).length) s d) (hf : ComputableInTimeAndSpace f encIn encOut t s) : ComputableInDegree f encIn encOut d d

Exact time and workspace bounds of degree d also bound the output length in degree d.

theorem Turing.MultiTapeTM.ComputableInDegree.one_one_iff {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} : ComputableInDegree f encIn encOut 1 1 ↔ ∃ (c : ℕ), ComputableInTimeAndSpace f encIn encOut (fun (a : α) => c * ((encIn a).length + 1)) fun (a : α) => c * ((encIn a).length + 1)

Degree one is exactly one uniform machine with common linear time/workspace bounds. Independent constants can be enlarged to a common constant. The same machine's runtime bounds its output; output length is not charged to workspace.

theorem Turing.MultiTapeTM.ComputableInDegree.computableInPolyTime {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {d e : ℕ} (h : ComputableInDegree f encIn encOut d e) : ComputableInPolyTime f encIn encOut

Fixed time and workspace degrees give plain polynomial-time computability, including degree zero. Encoded output is bounded separately and is not charged to workspace.

theorem Turing.MultiTapeTM.ComputableInDegree.inO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {d e : ℕ} (h : ComputableInDegree f encIn encOut d e) : ComputableInO f encIn encOut (fun (a : α) => ((encIn a).length + 1) ^ d) fun (a : α) => ((encIn a).length + 1) ^ d

The realizing machine's own clock bounds its output, independently of the supplied output degree. Both asymptotic resource exponents remain d, including zero.

theorem Turing.MultiTapeTM.ComputableInDegree.inO_one {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {e : ℕ} (h : ComputableInDegree f encIn encOut 1 e) : ComputableInO f encIn encOut (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

Cost degree one gives linear charged resource bounds, without restricting the output degree.

theorem Turing.MultiTapeTM.ComputableInO.computableInDegree {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} {d e : ℕ} (h : ComputableInO f encIn encOut T S) (hT : DegreeBounded (fun (a : α) => (encIn a).length) T d) (hS : DegreeBounded (fun (a : α) => (encIn a).length) S e) (hed : e ≤ d) : ComputableInDegree f encIn encOut d e

Charged workspace of degree e bounds the encoded output at that same degree. When e ≤ d, independent degree bounds on time and workspace give cost degree d and output degree e, retaining the realizing machine and its original resource bounds.