P closure properties — proof internals

This file contains the proof helpers used by DTIME_union (stated in P.lean). The key simulation theorem unionTM_decidesInTime establishes that the composite machine from TM.unionTM correctly decides L₁ ∪ L₂.

theorem Complexity.TM.unionTM_decidesInTime {n₁ n₂ : ℕ} {tm₁ : TM n₁} {tm₂ : TM n₂} {L₁ L₂ : Language} {f₁ f₂ : ℕ → ℕ} (h₁ : tm₁.DecidesInTime L₁ f₁) (h₂ : tm₂.DecidesInTime L₂ f₂) : (tm₁.unionTM tm₂).DecidesInTime (L₁ ∪ L₂) fun (n : ℕ) => 10 * f₁ n + f₂ n

The union TM correctly decides L₁ ∪ L₂ with time bound 10·f₁ + f₂.

The factor 10 arises from Phase 1 (f₁ steps), transition (≤ 2·f₁ + 7 steps absorbed into 9·f₁ since f₁ ≥ 1), and Phase 2 (f₂ steps).

theorem Complexity.bigO_union_bound {f₁ f₂ T₁ T₂ : ℕ → ℕ} (ho₁ : BigO f₁ T₁) (ho₂ : BigO f₂ T₂) : BigO (fun (n : ℕ) => 10 * f₁ n + f₂ n) fun (n : ℕ) => T₁ n + T₂ n

If f₁ =O T₁ and f₂ =O T₂, then 10·f₁ + f₂ =O (T₁ + T₂).