294structure SpectralTuringBridgeHypothesis where 295 /-- The spectral gap of the SAT J-cost Laplacian is positive -/ 296 spectral_gap_positive : ∀ n : ℕ, ∃ gap : ℝ, 0 < gap ∧ gap ≤ 1 297 /-- R̂ convergence time is O(n) recognition steps -/ 298 rhat_convergence : ∀ n : ℕ, ∃ T_R : ℕ, T_R ≤ n + 1 299 /-- Simulating one global gradient step requires Ω(n) TM tape operations -/ 300 simulation_cost_per_step : ∀ n : ℕ, ∃ cost : ℕ, cost ≥ n / 2 301 /-- Therefore TM time ≥ T_R × (n/2) = Ω(n²) -/ 302 tm_time_lower_bound : ∀ n : ℕ, ∃ T_TM : ℕ, T_TM ≥ n * (n / 2) 303 304/-- **CONDITIONAL THEOREM**: Given SpectralTuringBridgeHypothesis, 305 the TM time for SAT is Ω(n²), while R̂ needs only O(n) steps. 306 For n ≥ 4, the TM lower bound exceeds the R̂ upper bound. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.