`TMSimulator`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.CellularAutomata
domain: Complexity
line: 195 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.CellularAutomata on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 192/-! ## CA → TM Simulation -/
 193
 194/-- A Turing Machine simulating the CA -/
 195structure TMSimulator where
 196  /-- Number of CA steps to simulate -/
 197  ca_steps : ℕ
 198  /-- Tape size (number of cells) -/
 199  tape_size : ℕ
 200  /-- TM time per CA step (linear in tape size) -/
 201  time_per_step : ℕ := tape_size
 202
 203/-- TM time to simulate CA -/
 204def tm_simulation_time (sim : TMSimulator) : ℕ :=
 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 -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.