strong_cp_gap

formal source

 274    J-cost ≥ 1 − cos(π/4) ≈ 0.293. So the structural selection of θ = 0
 275    is not just a minimum but is separated from the next-best by a
 276    macroscopic gap. -/
 277theorem strong_cp_gap :
 278    1 - Real.cos (Real.pi / 4) > 0.29 := by
 279  have : Real.cos (Real.pi / 4) = Real.sqrt 2 / 2 := Real.cos_pi_div_four
 280  rw [this]
 281  have h_sqrt2 : Real.sqrt 2 < 1.42 := by
 282    rw [show (1.42 : ℝ) = Real.sqrt (1.42 ^ 2) from by
 283      rw [Real.sqrt_sq]; norm_num]
 284    apply Real.sqrt_lt_sqrt
 285    · norm_num
 286    · norm_num
 287  linarith
 288
 289/-- **STRONG CP NUMERICAL CERTIFICATE**.
 290    Combines the structural (8-tick + J-min) and numerical (interval) statements. -/
 291structure StrongCPNumericalCert where
 292  predicted : theta_RS_predicted = 0
 293  inside_experimental :
 294    -theta_experimental_max < theta_RS_predicted ∧
 295    theta_RS_predicted < theta_experimental_max
 296  abs_lt : |theta_RS_predicted| < theta_experimental_max
 297  gap_to_next : 1 - Real.cos (Real.pi / 4) > 0.29
 298  J_cost_min : ∀ θ, thetaJCost 0 ≤ thetaJCost θ
 299
 300noncomputable def strongCPNumericalCert : StrongCPNumericalCert where
 301  predicted := rfl
 302  inside_experimental := theta_RS_inside_experimental
 303  abs_lt := abs_theta_RS_lt_bound
 304  gap_to_next := strong_cp_gap
 305  J_cost_min := theta_zero_minimizes
 306
 307/-! ## Falsification Criteria -/