eotvos_parameter
The Eötvös parameter is defined as the absolute difference of two accelerations divided by their absolute sum. Experimental physicists testing the equivalence principle cite this quantity when comparing RS predictions against MICROSCOPE bounds. The definition is a direct transcription of the standard observable with no additional structure or proof steps.
claimThe Eötvös parameter for two accelerations $a_1$ and $a_2$ is given by $η = |a_1 - a_2| / |a_1 + a_2|$.
background
In Recognition Science the equivalence principle is a direct consequence of the single cost function J(x) = ½(x + x⁻¹) − 1 whose uniqueness is established at T5. Both inertial mass (resistance to ledger change) and gravitational mass (source of curvature via J-cost density) are extracted from this identical J, so they must coincide for any body. The module G-003 therefore treats any mass theory that pulls both masses from the same J as automatically satisfying the principle.
proof idea
This is a direct definition with no proof body. It transcribes the conventional experimental formula for the Eötvös parameter η without invoking any lemmas or tactics.
why it matters in Recognition Science
The definition supplies the observable used by rs_eotvos_zero to prove that RS forces η = 0 exactly when the two bodies share the same J-cost. It is then invoked by rs_consistent_with_microscope to confirm consistency with the MICROSCOPE bound of 10^{-15}. It realizes the G-003 registry item by providing the concrete metric for the tautological equivalence that follows from T5 J-uniqueness.
scope and limits
- Does not derive equality of inertial and gravitational mass.
- Does not incorporate the explicit form of the J-cost function.
- Does not reference the MICROSCOPE experimental bound.
- Does not specify units or scaling conventions for the accelerations.
formal statement (Lean)
176def eotvos_parameter (a1 a2 : ℝ) : ℝ := |a1 - a2| / |a1 + a2|
proof body
Definition body.
177