H_SATTMRuntime

formal source

 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 -/
 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/-!
 233theorem sat_computation_time (n : ℕ) (hn : 0 < n) :
 234    ∃ (c : ℝ), c > 0 ∧
 235    (sat_eval_time n n : ℝ) ≤ c * n^(1/3 : ℝ) * Real.log n
 236-/
 237
 238/-- **Recognition time** for SAT output (documentation / TODO): Ω(n) due to balanced-parity encoding.
 239
 240Intended claim: By balanced-parity hiding, reading fewer than n bits is insufficient to determine
 241the SAT result. Any decoder reading a proper subset of the input bits will fail on at least
 242one pair of tapes that match on the observed bits but differ in the total parity (and thus
 243the result). -/
 244/-!
 245theorem sat_recognition_time (n : ℕ) (hn : 0 < n) :
 246    ∃ (c : ℝ), c > 0 ∧
 247    ∀ (decoder : Fin n → Bool → Prop),
 248      -- Any decoder that reads fewer than n bits cannot determine SAT result