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