ep_relative_error

formal source

 160def Jcost_exact (eps : ℝ) : ℝ := eps ^ 2 / (2 * (1 + eps))
 161
 162/-- The O(ε⁴) relative error between quadratic and exact. -/
 163def ep_relative_error (eps : ℝ) : ℝ :=
 164  (Jcost_quadratic eps - Jcost_exact eps) / Jcost_exact eps
 165
 166/-- For the EP, what matters is NOT the size of corrections, but whether
 167    they affect inertial and gravitational mass DIFFERENTLY.
 168    In SingleSourceMassTheory, they cannot differ: both use J_full. -/
 169theorem ep_exact_all_orders (T : SingleSourceMassTheory) (x : ℝ) (hx : 0 < x) :
 170    T.inertial_mass x = T.gravitational_mass x :=
 171  single_source_equivalence T x hx
 172
 173/-- The RS prediction: the Eötvös parameter η = 0 exactly.
 174    η = |a₁ - a₂| / |a₁ + a₂| for two test bodies.
 175    Since both experience the same J-cost, a₁ = a₂, so η = 0. -/
 176def eotvos_parameter (a1 a2 : ℝ) : ℝ := |a1 - a2| / |a1 + a2|
 177
 178theorem rs_eotvos_zero (a : ℝ) : eotvos_parameter a a = 0 := by
 179  unfold eotvos_parameter; simp
 180
 181/-- The MICROSCOPE experiment measures η < 10⁻¹⁵.
 182    RS predicts η = 0 exactly. This is consistent with experiment and
 183    makes the strongest possible prediction: any nonzero η falsifies RS. -/
 184def microscope_bound : ℝ := 1e-15
 185
 186theorem rs_consistent_with_microscope :
 187    eotvos_parameter 9.80665 9.80665 < microscope_bound := by
 188  rw [rs_eotvos_zero]; unfold microscope_bound; norm_num
 189
 190end
 191
 192end EquivalencePrinciple
 193end Gravity