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