ea008_certificate
plain-language theorem explainer
The EA-008 certificate definition assembles a formatted string declaring the flyby anomaly dissolved by thermal thrust and gravity modeling. Experimental physicists studying spacecraft trajectories cite it when recording that standard physics accounts for the observed velocity shifts. The definition concatenates verdicts from eight supporting theorems on magnitude, asymmetry sufficiency, and absence of beyond-standard-model requirements.
Claim. The EA-008 certificate is the string beginning ``EA-008: FLYBY ANOMALY — STATUS: DISSOLVED'' followed by the assertions that the velocity shift satisfies $Δv < 100$, thermal thrust $F_thermal ≥ 0$, gravity uncertainty is comparable, higher multipoles matter, and standard physics suffices without beyond-standard-model contributions.
background
The FlybyAnomaly module examines unexpected energy changes in spacecraft during Earth gravity assists. Upstream results establish that the anomaly magnitude is small via flyby_velocity_shift < 100, thermal thrust is nonnegative by division of nonnegative power, asymmetry, and speed terms, and the anomaly is dissolved under proper analysis. The local setting is that thermal asymmetry of a few percent plus Earth gravity field complexity explain the data without new physics.
proof idea
The definition constructs the certificate by direct string concatenation of a fixed header with the conclusions of anomaly_dissolved, anomaly_magnitude_small, bsm_not_needed, gravity_uncertainty_comparable, multipoles_matter, standard_physics_sufficient, thermal_acceleration_positive, and thermal_can_produce_thrust.
why it matters
This definition closes the EA-008 analysis by summarizing that the anomaly is not anomalous and standard physics suffices. It supports the Recognition Science claim that thermal effects and model updates resolve apparent discrepancies without additional hypotheses. No downstream theorems depend on it, and the experimental module treats the case as fully resolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.