def
definition
eotvos_parameter
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.EquivalencePrinciple on GitHub at line 176.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
194end IndisputableMonolith