`ca_to_tm_simulation_prop`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Runtime
domain: Complexity
line: 33 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Runtime on GitHub at line 33.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  30/-- CA→TM simulation cost: TM time = O(volume * steps).
  31    The actual content would specify that a Turing Machine can simulate
  32    a cellular automaton with volume V and time T in O(V·T) steps. -/
  33def ca_to_tm_simulation_prop {n} (rt : CARuntime n) : Prop :=
  34  ∃ c : Nat, c > 0 ∧ rt.volume * rt.steps ≤ c * n^2 -- Simplified polynomial bound
  35
  36/-- Target bound for the full 3-SAT algorithm.
  37    Total TM time is bounded by O(n^{11/3} log n). -/
  38def three_sat_runtime_prop (n : Nat) : Prop :=
  39  ∃ c : ℝ, c > 0 ∧ (n : ℝ)^(11/3 : ℝ) * Real.log (n + 2) ≤ c * (n : ℝ)^4
  40
  41
  42end SAT
  43end Complexity
  44end IndisputableMonolith

papers checked against this theorem

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