microscope_bound
plain-language theorem explainer
The definition supplies the real number 10^{-15} as the experimental upper limit on the Eötvös parameter reported by the MICROSCOPE satellite. Equivalence-principle tests cite this threshold to confirm that the Recognition Science prediction of exact equality lies inside measured bounds. The declaration is a direct numerical assignment with no lemmas or computation.
Claim. The MICROSCOPE experimental bound on the Eötvös parameter is the real number $10^{-15}$.
background
The module derives the equivalence principle from the single cost function J(x) = ½(x + x^{-1}) - 1 whose uniqueness is established by T5. Inertial mass arises as the quadratic coefficient of J near balance while gravitational mass is the integrated J-cost defect; both therefore coincide for every body. The module states that any MassTheory extracting both masses from this J necessarily yields equal values, turning equivalence into a tautology rather than an independent assumption.
proof idea
The declaration is a direct constant definition that binds the identifier to the literal 1e-15. No lemmas are invoked and no tactics are executed.
why it matters
The constant is referenced by the downstream theorem rs_consistent_with_microscope, which shows that the RS Eötvös parameter is strictly less than this bound. It thereby converts the theoretical claim (any nonzero η falsifies RS) into a concrete consistency statement with the tightest available experiment. The definition closes the link between the single-J derivation of equivalence and the G-003 registry item.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.