rs_eotvos_zero
plain-language theorem explainer
rs_eotvos_zero establishes that the Eötvös parameter vanishes identically for any pair of equal test bodies, confirming exact inertial-gravitational mass equality under Recognition Science's single J-cost function. Experimental physicists testing the MICROSCOPE bound would cite this algebraic identity to anchor the framework's zero prediction. The proof is a one-line term-mode wrapper that unfolds the parameter definition and applies simplification.
Claim. For any real number $a$, the Eötvös parameter satisfies $eotvos_parameter(a,a)=0$, where $eotvos_parameter(a_1,a_2) := |a_1 - a_2| / |a_1 + a_2|$.
background
In the G-003 derivation, inertial mass arises as the quadratic coefficient of J-cost for small deviations from balance while gravitational mass is the integrated J-cost defect sourcing curvature; both functionals derive from the identical unique J, so they coincide. The Eötvös parameter is defined directly as the normalized absolute difference of the two accelerations. Upstream results supply the parameter definition itself together with consistency predicates from SAT backpropagation and decision modules that ensure the underlying ledger states remain compatible with the single cost function.
proof idea
The proof is a one-line term-mode wrapper that unfolds the definition of eotvos_parameter and applies the simp tactic, which reduces the numerator to zero when the two arguments are identical.
why it matters
This supplies the exact zero that the downstream theorem rs_consistent_with_microscope invokes to verify consistency with the MICROSCOPE bound. It directly realizes the G-003 registry item by showing that the single J-cost forces inertial-gravitational equality, aligning with the T5 J-uniqueness landmark and the claim that any nonzero Eötvös parameter would falsify the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.