Internal machine normal forms for plain resource bounds

These witness operations normalize a single plain realizing machine. They do not introduce a second computability calculus or register bridges for automation. The degree operation preserves the time/workspace degree, including zero; the caller retains its independent output-degree proof. The charged asymptotic operation preserves independent time and workspace functions and the full encoded-output charge, using the same machine's space bound together with its time-derived bound.

Main results

• Turing.MultiTapeTM.Internal.NormalForm.polyTime: one polynomial machine bound.
• Turing.MultiTapeTM.Internal.NormalForm.degree: degree-preserving machine witnesses.
• Turing.MultiTapeTM.Internal.NormalForm.inO: independent charged asymptotic witnesses.

theorem Turing.MultiTapeTM.Internal.NormalForm.polyTime {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInPolyTime f encIn encMid) : ∃ (c : ℕ) (d : ℕ) (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encMid (f a)) (c * ((encIn a).length + 1) ^ d) (c * ((encIn a).length + 1) ^ d)

A polynomial certificate gives one normalized realizing machine at a common polynomial bound.

theorem Turing.MultiTapeTM.Internal.NormalForm.degree {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} {d e : ℕ} (h : ComputableInDegree f encIn encMid d e) : ∃ (t : α → ℕ) (s : α → ℕ), DegreeBounded (fun (a : α) => (encIn a).length) t d ∧ DegreeBounded (fun (a : α) => (encIn a).length) s d ∧ ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encMid (f a)) (t a) (s a)

Normalization preserves the cost degree; the original encoded-output degree is separate.

theorem Turing.MultiTapeTM.Internal.NormalForm.bigO {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} {T S : α → ℕ} (h : ComputableInBigO f encIn encMid T S) : ∃ (c : ℕ) (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encMid (f a)) (c * (T a + 1)) (c * (S a + 1))

Independent asymptotic time/workspace bounds normalize without an output-length premise.

theorem Turing.MultiTapeTM.Internal.NormalForm.inO {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} {T S : α → ℕ} (h : ComputableInO f encIn encMid T S) : ∃ (c : ℕ), (∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encMid (f a)) (c * (T a + 1)) (c * (S a + 1))) ∧ ∀ (a : α), (encMid (f a)).length ≤ c * (S a + 1)

Normalize charged bounds, retaining their existing encoded-output bound.

theorem Turing.MultiTapeTM.Internal.NormalForm.linear {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLinearTimeAndSpace f encIn encMid) : ∃ (c : ℕ) (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encMid (f a)) (c * ((encIn a).length + 1)) (c * ((encIn a).length + 1))

Linear certificates normalize at a common linear bound without changing the encoding.