thermal_acceleration_positive
plain-language theorem explainer
Thermal acceleration from asymmetric spacecraft heat radiation is non-negative. Analysts of the flyby anomaly cite this to confirm the thermal contribution adds positively to velocity shifts during gravity assists. The proof unfolds the defining expressions for thrust and acceleration then applies non-negativity of division to the constant parameters.
Claim. Let $P = 300$ be spacecraft thermal power in W, $a = 0.03$ the emission asymmetry fraction, $c = 299792458$ the speed of light in m/s, and $m = 1000$ the spacecraft mass in kg. Define thrust $F = P a / c$ and acceleration $a = F / m$. Then $a ≥ 0$.
background
The module EA-008 examines the flyby anomaly of unexpected spacecraft velocity changes during Earth gravity assists. Recognition Science attributes the effect to standard thermal radiation plus gravity model updates rather than new physics.
proof idea
The tactic proof unfolds thermal_acceleration, thermal_thrust, and c_speed to expose the quotient form. Non-negativity of spacecraft_thermal_power, thermal_asymmetry, and c_speed follows from norm_num on their constant definitions. Two applications of div_nonneg then close the inequality.
why it matters
This theorem supplies one clause of the EA-008 certificate that declares the anomaly dissolved. It confirms thermal thrust yields positive acceleration, supporting the module verdict that classical effects suffice. The result sits downstream of the thermal_thrust definition and feeds the certificate string that lists thermal_can_produce_thrust as verified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.