strongCPCert

formal source

 229  zero_cost : thetaJCost 0 = 0
 230  nonzero_positive : ∀ θ, thetaJCost θ > 0 → θ ≠ 0
 231
 232def strongCPCert : StrongCPCert := {
 233  theta_minimizes := theta_zero_minimizes
 234  zero_cost := by unfold thetaJCost; simp [Real.cos_zero]
 235  nonzero_positive := by
 236    intro θ hpos hzero
 237    simp [hzero] at hpos
 238    unfold thetaJCost at hpos
 239    simp [Real.cos_zero] at hpos
 240}
 241
 242/-! ## Numerical Bound Bridge
 243
 244The structural derivation above selects θ = 0 exactly. Combined with the
 2458-tick quantization, the only J-minimizing θ in the allowed list is θ = 0,
 246and any nonzero allowed θ has J-cost ≥ 1 − cos(π/4) > 0.29.
 247
 248The empirical bound |θ| < 10⁻¹⁰ from neutron EDM is consistent with the
 249RS prediction θ = 0. We package this as a numerical interval theorem
 250so downstream cosmology code can cite it as a number, not just a structure.
 251-/
 252
 253/-- The RS prediction: θ_QCD = 0 exactly. -/
 254noncomputable def theta_RS_predicted : ℝ := 0
 255
 256/-- The experimental bound on |θ_QCD|: 10⁻¹⁰ from neutron EDM. -/
 257noncomputable def theta_experimental_max : ℝ := 1e-10
 258
 259/-- The RS-predicted θ lies strictly inside the experimental interval. -/
 260theorem theta_RS_inside_experimental :
 261    -theta_experimental_max < theta_RS_predicted ∧
 262    theta_RS_predicted < theta_experimental_max := by