anomaly_dissolved
plain-language theorem explainer
The declaration establishes non-negativity of thrust arising from thermal asymmetry in the flyby model. Experimental physicists checking spacecraft gravity-assist data would cite it to rule out exotic contributions. The proof is a direct one-line reference to the prior non-negativity result for the same quantity.
Claim. Thrust generated by thermal asymmetry satisfies $F = P_*/c$ with $F$ non-negative, where $P_*$ denotes the product of spacecraft thermal power and asymmetry factor, and $c$ is the speed of light.
background
The EA-008 module treats the flyby anomaly as an apparent energy change during Earth gravity assists and concludes that thermal plus gravity-model updates suffice. The central definition is thermal_thrust, the quantity spacecraft_thermal_power multiplied by thermal_asymmetry and divided by c_speed. The upstream theorem bsm_not_needed already records that this quantity is non-negative by unfolding the definition and applying non-negativity of each factor.
proof idea
The proof is a one-line term wrapper that invokes bsm_not_needed. That lemma unfolds thermal_thrust together with c_speed, obtains non-negativity of the three factors by norm_num, and closes with mul_nonneg followed by div_nonneg.
why it matters
The result finishes the EA-008 case by confirming the thermal hypothesis and supplies the non-negativity fact used inside ea008_certificate. It mirrors the pattern in the muon g-2 module where the corresponding anomaly_dissolved theorem likewise dissolves the discrepancy inside standard physics. The declaration therefore closes one experimental scaffolding item without invoking beyond-standard-model structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.