pith. machine review for the scientific record. sign in
def definition def or abbrev

caTimeBound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  27def caTimeBound (M : CARuntimeModel) (n : ℕ) : Prop :=

proof body

Definition body.

  28  ∃ c : ℝ, 0 < c ∧ (M.sideLength n : ℝ) * (logicalDepth n : ℝ) ≤ c * (n : ℝ)^(1/3 : ℝ) * Real.log (n + 2)
  29
  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. -/

depends on (14)

Lean names referenced from this declaration's body.