bsm_not_needed
plain-language theorem explainer
Thermal thrust from spacecraft power asymmetry is non-negative. Analysts of the flyby anomaly cite the result to exclude beyond-standard-model contributions. The proof reduces the defining expression to a quotient of non-negative reals by unfolding the constants and applying non-negativity lemmas.
Claim. Let $P$ be spacecraft thermal power, $a$ the fractional asymmetry in thermal emission, and $c$ the speed of light. The thrust $F = P a / c$ satisfies $F ≥ 0$.
background
The module EA-008 examines the flyby anomaly and concludes that standard physics suffices. Spacecraft thermal power is set to 300 W, thermal asymmetry to 0.03, and $c$ to 299792458 m/s. Thermal thrust is defined as the product of power and asymmetry divided by $c$. Upstream definitions supply these constants and the non-negativity predicates used in the argument.
proof idea
The tactic proof unfolds thermal_thrust and c_speed. It obtains non-negativity of spacecraft_thermal_power, thermal_asymmetry, and c_speed by norm_num. It then applies mul_nonneg followed by div_nonneg to reach the conclusion.
why it matters
The result feeds anomaly_dissolved and pattern_matches_thermal, which close the EA-008 certificate by confirming the anomaly dissolves under thermal analysis. It supplies the EA-008.8 step asserting no BSM physics is required. The declaration keeps the experimental section inside the Recognition Science bounds that rely on the existing constants and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.