microscope_bound
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from Recognition Science axioms.
- Does not prove any inequality or bound on the Eötvös parameter.
- Does not incorporate units, error bars, or experimental systematics.
- Does not address other equivalence tests such as torsion-balance experiments.
Lean usage
theorem rs_consistent_with_microscope : eotvos_parameter 9.80665 9.80665 < microscope_bound := by rw [rs_eotvos_zero]; unfold microscope_bound; norm_numformal statement (Lean)
184def microscope_bound : ℝ := 1e-15
proof body
Definition body.
185