tm_simulation_bound

formal source

 205  sim.ca_steps * sim.time_per_step
 206
 207/-- Simulation bound: TM time is CA_steps × tape_size -/
 208theorem tm_simulation_bound (sim : TMSimulator) :
 209    tm_simulation_time sim = sim.ca_steps * sim.tape_size := by
 210  simp only [tm_simulation_time, TMSimulator.time_per_step]
 211
 212/-- **HYPOTHESIS**: Turing Machine simulation of SAT evaluation via CA.
 213
 214    STATUS: SCAFFOLD — The total Turing time for SAT evaluation via CA is
 215    predicted to be O(n^{4/3} log n), but this depends on the CA runtime bound.
 216
 217    TODO: Formally prove the simulation time bound. -/
 218def H_SATTMRuntime (n m : ℕ) : Prop :=
 219  ∃ (T : ℕ), T ≤ n * sat_eval_time n m ∧
 220  -- This is the total Turing time for SAT evaluation via CA
 221  IsCorrectTMResult n m T -- SCAFFOLD: IsCorrectTMResult is not yet defined.
 222
 223-- axiom h_sat_tm_runtime : ∀ n m, 0 < n → H_SATTMRuntime n m
 224
 225/-! ## The Key Separation -/
 226
 227/-- **Computation time** for SAT via CA (documentation / TODO): O(n^{1/3} log n)
 228
 229Intended claim: The CA evaluation time for a SAT instance with n variables and m clauses is
 230O(n^{1/3} log(n+m)). This follows from arranging variables in a 3D-like grid on the 1D tape
 231and using parallel propagation. -/
 232/-!
 233theorem sat_computation_time (n : ℕ) (hn : 0 < n) :
 234    ∃ (c : ℝ), c > 0 ∧
 235    (sat_eval_time n n : ℝ) ≤ c * n^(1/3 : ℝ) * Real.log n
 236-/
 237
 238/-- **Recognition time** for SAT output (documentation / TODO): Ω(n) due to balanced-parity encoding.