gravity_velocity_uncertainty
plain-language theorem explainer
The definition assigns the constant value 2.0 to velocity uncertainty arising from gravity model inaccuracies during Earth flybys. Researchers comparing model errors to observed spacecraft velocity shifts would cite this value when assessing whether classical gravity refinements explain the anomaly. It is realized as a direct real-number assignment with no further computation or lemmas applied.
Claim. The uncertainty in spacecraft velocity due to gravity model errors is defined as $2.0$ mm/s.
background
The module examines the flyby anomaly consisting of unexpected energy changes in spacecraft during Earth gravity assists. The Recognition Science assessment concludes that thermal effects plus updates to gravity models suffice as an explanation. Upstream, CPM2D.model constructs a Model from a Hypothesis bundle that supplies parameters including defectMass, orthoMass, energyGap, and tests for use in classical continuum descriptions.
proof idea
The definition is a direct real-number assignment of 2.0 with no lemmas invoked and no tactic steps required.
why it matters
This supplies the numerical threshold for the downstream theorem gravity_uncertainty_comparable (EA-008.5), which shows the value exceeds one-third of the flyby velocity shift. It supports the module-level claim that gravity model uncertainty is comparable to the anomaly magnitude. Within the Recognition Science framework it contributes to the experimental verdict that standard physics accounts for the observed flyby effects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.