computation_takes_time

formal source

 125
 126/-- **THEOREM IC-003.9**: Any RS computation taking n steps requires at least n ticks.
 127    Time(n steps) ≥ n × τ₀ (by discreteness of time in RS). -/
 128theorem computation_takes_time (n : ℕ) (hn : n > 0) :
 129    n * fundamental_tick > 0 := by
 130  exact mul_pos (Nat.cast_pos.mpr hn) tick_pos
 131
 132/-! ## V. The Physical Church-Turing Bridge -/
 133
 134/-- **THEOREM IC-003.10**: Every finite function on a finite type is "computable"
 135    in the sense that it can be represented by a lookup table. -/
 136theorem finite_function_is_computable {α β : Type*} [Fintype α] [Fintype β]
 137    [DecidableEq α] [DecidableEq β]
 138    (f : α → β) :
 139    ∃ (table : Finset (α × β)),
 140      ∀ a : α, ∃ b : β, (a, b) ∈ table ∧ f a = b := by
 141  use Finset.image (fun a => (a, f a)) Finset.univ
 142  intro a
 143  exact ⟨f a, Finset.mem_image.mpr ⟨a, Finset.mem_univ a, rfl⟩, rfl⟩
 144
 145/-- **THEOREM IC-003.11**: The 8-tick step function is computable (it's a function
 146    on a finite phase space, hence encodable as a lookup table). -/
 147theorem eight_tick_step_computable (step : Phase → Phase) :
 148    ∃ (table : Finset (Phase × Phase)),
 149      ∀ p : Phase, ∃ p' : Phase, (p, p') ∈ table ∧ step p = p' :=
 150  finite_function_is_computable (α := Phase) (β := Phase) step
 151
 152/-! ## VI. RS Complexity Classes -/
 153
 154/-- **THEOREM IC-003.12**: φ is irrational, so RS dynamics involving φ-ladders
 155    cannot be exactly computed by finite rational algorithms.
 156    This places exact RS computations in the class of "real number computations"
 157    (beyond classical Turing machines for exact values). -/
 158theorem rs_dynamics_beyond_rational : ¬ ∃ q : ℚ, (q : ℝ) = phi :=