eotvos_parameter
plain-language theorem explainer
Recognition Science predicts a vanishing Eötvös parameter because both inertial and gravitational masses derive from the single unique cost function J. Experimentalists testing the equivalence principle cite this definition to express the observable ratio of accelerations for two test bodies. The definition is a direct transcription of the classical formula into the RS setting where equal J-cost forces the numerator to zero.
Claim. $η(a_1, a_2) := |a_1 - a_2| / |a_1 + a_2|$ for real accelerations $a_1, a_2$ of two test bodies.
background
The module G-003 derives the equivalence principle from the single cost function J(x) = ½(x + x^{-1}) - 1 whose uniqueness follows from T5. Inertial mass is the quadratic coefficient in the small-deviation expansion of J around balance while gravitational mass is the integrated J-cost defect; both therefore coincide for any body composition. The Eötvös parameter quantifies any possible violation as the normalized difference between observed accelerations. The supplied definition expresses this observable directly in the RS context.
proof idea
The declaration is a one-line definition that implements the classical Eötvös ratio without invoking lemmas or tactics.
why it matters
It underpins rs_eotvos_zero, which proves the parameter equals zero for equal accelerations, and rs_consistent_with_microscope, which places the result below the MICROSCOPE bound. The definition thereby realizes the G-003 claim that the equivalence principle is a tautology once a unique J is adopted. It connects directly to the T5 uniqueness result and the consequent equality of inertial and gravitational mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.