sat_computation_time

formal source

 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
 249      (∃ M : Finset (Fin n), M.card < n ∧
 250        ∀ result : Bool, ∃ tape1 tape2 : Fin n → Bool,
 251          (∀ i ∈ M, tape1 i = tape2 i) ∧
 252          decoder tape1 result ∧ ¬decoder tape2 result)
 253-/
 254
 255/-- **THE SEPARATION**: Tc << Tr (documentation / TODO)
 256
 257Intended claim: There is a gap between computation time (Tc) and recognition time (Tr).
 258For large n, Tc scales as O(n^{1/3} log n) while Tr scales as Ω(n). -/
 259/-!
 260theorem computation_recognition_separation (n : ℕ) (hn : 100 ≤ n) :
 261    ∃ (Tc Tr : ℝ),
 262      Tc ≤ n^(1/3 : ℝ) * Real.log n ∧
 263      Tr ≥ n ∧