Independent computation bounds and encoded-output growth

Time, workspace and encoded output are separate obligations. These rules package or forget the actual realizing machine; they do not normalize it or import a higher construction calculus. computableInO_iff_computableInBigO_and_length_le separates the charged convenience predicate into uncharged machine bounds and the existing pointwise output-length relation.

theorem Turing.MultiTapeTM.ComputableInO.computableInBigO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableInO f encIn encOut T S) : ComputableInBigO f encIn encOut T S

Forget the encoded-output charge, retaining the same realizing machine.

theorem Turing.MultiTapeTM.ComputableInO.length_le {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableInO f encIn encOut T S) : ∃ (c : ℕ), ∀ (a : α), (encOut (f a)).length ≤ c * (S a + 1)

The encoded value is within the certificate's existing workspace charge.

theorem Turing.MultiTapeTM.ComputableInO.of_bounds {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S t s : α → ℕ} (hf : ComputableInTimeAndSpace f encIn encOut t s) (k : ℕ) (ht : ∀ (a : α), t a ≤ k * (T a + 1)) (hs : ∀ (a : α), s a ≤ k * (S a + 1)) (hl : ∀ (a : α), (encOut (f a)).length ≤ k * (S a + 1)) : ComputableInO f encIn encOut T S

Exact plain machine bounds and an explicit output charge supply asymptotic bounds.

theorem Turing.MultiTapeTM.ComputableInO.mono {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' S' : α → ℕ} (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ (a : α), T a ≤ k * (T' a + 1)) (hS : ∀ (a : α), S a ≤ k * (S' a + 1)) : ComputableInO f encIn encOut T' S'

Weaken both bounds by independent pointwise estimates and a common constant.

theorem Turing.MultiTapeTM.ComputableInO.mono_time {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' : α → ℕ} (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ (a : α), T a ≤ k * (T' a + 1)) : ComputableInO f encIn encOut T' S

Weaken only the time bound up to a constant, keeping the space bound.

theorem Turing.MultiTapeTM.ComputableInO.mono_le {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' S' : α → ℕ} (h : ComputableInO f encIn encOut T S) (hT : ∀ (a : α), T a ≤ T' a) (hS : ∀ (a : α), S a ≤ S' a) : ComputableInO f encIn encOut T' S'

Pointwise larger bounds retain the same encoded-output charge.

theorem Turing.MultiTapeTM.ComputableInO.weaken {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' S' : α → ℕ} (h : ComputableInO f encIn encOut T S) (hT : BigOLe T T') (hS : BigOLe S S') : ComputableInO f encIn encOut T' S'

Weaken independent time and charged workspace bounds up to constants.

theorem Turing.MultiTapeTM.ComputableInO.of_enc_eq {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} {γ : Type u_3} {encC : γ ↪ List Bool} {g : α → γ} (h : ComputableInO f encIn encOut T S) (hg : ∀ (a : α), encC (g a) = encOut (f a)) : ComputableInO g encIn encC T S

An equal encoded output reuses the same machine and both resource budgets.

theorem Turing.MultiTapeTM.ComputableInO.of_encIn_eq {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} {δ : Type u_3} {encD : δ ↪ List Bool} (h : ComputableInO f encIn encOut T S) (g : δ → α) (hg : ∀ (a : δ), encIn (g a) = encD a) : ComputableInO (f ∘ g) encD encOut (T ∘ g) (S ∘ g)

Pull back along an input map preserving the complete encoded word. No algorithm for the semantic map is assumed: the realizing machine receives exactly the same word.

theorem Turing.MultiTapeTM.ComputableInO.computableInPolyTime {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableInO f encIn encOut T S) (hT : PolyBounded (fun (a : α) => (encIn a).length) T) (hS : PolyBounded (fun (a : α) => (encIn a).length) S) : ComputableInPolyTime f encIn encOut

Polynomial bounds on both resource functions give a plain polynomial-time certificate.

theorem Turing.MultiTapeTM.ComputableInBigO.with_output_bound {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableInBigO f encIn encOut T S) (hl : BigOLe (fun (a : α) => (encOut (f a)).length) S) : ComputableInO f encIn encOut T S

Add an independently proved output-length bound to an uncharged machine certificate.

theorem Turing.MultiTapeTM.computableInO_iff_computableInBigO_and_length_le {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} : ComputableInO f encIn encOut T S ↔ ComputableInBigO f encIn encOut T S ∧ BigOLe (fun (a : α) => (encOut (f a)).length) S

Charged computability is exactly uncharged computation and a separate output-growth bound. The two existential constants can be enlarged to a common constant without changing machines.

theorem Turing.MultiTapeTM.ComputableInBigO.of_bounds {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (ht : BigOLe t T) (hs : BigOLe s S) : ComputableInBigO f encIn encOut T S

Bounds up to constant factors.

theorem Turing.MultiTapeTM.ComputableInBigO.weaken {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' S' : α → ℕ} (h : ComputableInBigO f encIn encOut T S) (hT : BigOLe T T') (hS : BigOLe S S') : ComputableInBigO f encIn encOut T' S'

Weakening the bounds, up to constant factors.