gravity_uncertainty_comparable
The inequality shows gravity model velocity uncertainty exceeds one third the typical flyby velocity shift of 5 mm/s. Analysts of spacecraft Earth gravity assists would cite it when checking whether reported anomalies fall inside modeling error bars. The proof is a direct numerical comparison obtained by unfolding the two constant definitions and reducing with norm_num.
claimLet $δv_g$ be the velocity uncertainty arising from gravity model inaccuracies and let $Δv_f$ be the typical flyby velocity shift. Then $δv_g > Δv_f / 3$.
background
Module EA-008 analyzes the flyby anomaly: unexpected velocity changes in spacecraft during Earth gravity assists. The RS verdict is that standard physics suffices once thermal effects and gravity model updates are included. flyby_velocity_shift is the constant 5.0 (mm/s) standing for the observed anomaly magnitude in the 1-10 mm/s range. gravity_velocity_uncertainty is the constant 2.0 (mm/s) quantifying velocity error from current gravity models. The theorem also depends on the meta-realization structure for that supplies the orbit-coherence axioms.
proof idea
The term proof unfolds gravity_velocity_uncertainty and flyby_velocity_shift, then applies norm_num to compare the concrete values 2.0 and 5.0/3.
why it matters in Recognition Science
The result is invoked by ea008_certificate, which declares the flyby anomaly dissolved. It is labeled EA-008.5 and supplies the numerical comparison needed to show gravity-model uncertainty is comparable to the reported shift. Within Recognition Science this step supports the claim that thermal plus gravity-model refinements close the anomaly without new physics.
scope and limits
- Does not derive the numerical values of the constants from orbital equations.
- Does not include higher-order multipole corrections beyond the stated bound.
- Does not quantify thermal-thrust contributions to the same anomaly.
- Does not establish statistical significance of any residual discrepancy.
formal statement (Lean)
75theorem gravity_uncertainty_comparable :
76 gravity_velocity_uncertainty > flyby_velocity_shift / 3 := by
proof body
Term-mode proof.
77 unfold gravity_velocity_uncertainty flyby_velocity_shift
78 norm_num
79
80/-- **THEOREM EA-008.6**: Higher-order multipoles matter for close flybys. -/