gravity_model_accuracy
plain-language theorem explainer
The declaration assigns the numerical value of Earth gravity model accuracy to 1e-9 times standard surface gravity. Analysts of spacecraft flyby trajectories cite this bound when assessing whether observed anomalies exceed gravitational modeling errors. It is introduced as a direct constant definition without further reduction or derivation.
Claim. The accuracy of the Earth gravity model is defined as $10^{-9} times 9.81$ in units of m/s².
background
The Flyby Anomaly module examines unexpected energy changes in spacecraft during Earth gravity assists and concludes that standard physics suffices via thermal effects plus gravity model updates. This constant supplies the EGM2008-derived uncertainty bound at the surface. Upstream, PrimitiveDistinction.from reduces seven axioms to four structural conditions plus three definitional facts, Uncertainty provides lightweight reporting semantics for scalar measurements via sigma or interval forms, and CPM2D.model assembles a fluid model from a hypothesis bundle containing defect mass, ortho mass, and energy gap.
proof idea
The definition is a direct numerical assignment of the product 1e-9 * 9.81 with no lemmas or tactics applied.
why it matters
This supplies the gravitational uncertainty bound used in the flyby anomaly analysis, supporting the module verdict that thermal plus gravity model updates suffice. It provides a concrete numerical interface in the experimental domain for comparing predicted and observed accelerations. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.