rs_consistent_with_microscope
plain-language theorem explainer
RS predicts the Eötvös parameter vanishes identically because inertial and gravitational masses both derive from the single J-cost function. This result confirms that the exact zero value lies below the MICROSCOPE sensitivity threshold of 10^{-15}. Working physicists in precision gravity tests would reference it when comparing RS to experimental bounds. The proof is a direct term reduction that applies the zero-Eötvös lemma, unfolds the bound definition, and evaluates the numerical inequality.
Claim. The Eötvös parameter defined by $|a_1 - a_2| / |a_1 + a_2|$ evaluated at identical accelerations $a_1 = a_2 = 9.80665$ satisfies the inequality $0 < 10^{-15}$.
background
In the Recognition Science framework the equivalence principle is a direct consequence of the uniqueness of the cost function J(x) = (x + x^{-1})/2 - 1. Both inertial mass (resistance to ledger change) and gravitational mass (source of curvature via J-cost density) are extracted from this same J, so they must coincide for any body. The module formalizes this as G-003 by showing that any mass theory built on a single cost function yields equal inertial and gravitational masses. The Eötvös parameter quantifies possible violations as the relative difference in accelerations experienced by two test bodies. The upstream theorem establishes that this parameter is identically zero whenever the two accelerations are equal. The microscope bound is the experimental upper limit of 10^{-15} reported by the MICROSCOPE mission.
proof idea
The proof is a one-line term wrapper. It rewrites the goal using the lemma that the Eötvös parameter vanishes for equal inputs, unfolds the definition of the microscope bound, and applies norm_num to discharge the resulting numerical inequality.
why it matters
This theorem supplies a concrete consistency check between the RS derivation of the equivalence principle (G-003) and the MICROSCOPE experiment. It aligns with the T5 uniqueness of J, which forces the Eötvös parameter to zero and thereby guarantees inertial-gravitational mass equality. No downstream theorems depend on it yet; it functions as an independent verification that the exact-zero prediction survives the strongest current experimental bound. The result touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.