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/-!
depends on (13)
Lean names referenced from this declaration's body.