theorem other other

`computation_recognition_separation`

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

formal statement (Lean)

 260theorem computation_recognition_separation (n : ℕ) (hn : 100 ≤ n) :
 261    ∃ (Tc Tr : ℝ),
 262      Tc ≤ n^(1/3 : ℝ) * Real.log n ∧
 263      Tr ≥ n ∧
 264      Tc < Tr
 265-/
 266
 267end CellularAutomata
 268end Complexity
 269end IndisputableMonolith