bsm_not_needed
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not quantify the size of any velocity shift.
- Does not rule out every non-thermal contribution.
- Does not incorporate updated gravity models.
- Does not fit specific flyby telemetry data.
formal statement (Lean)
90theorem bsm_not_needed : thermal_thrust ≥ 0 := by
proof body
Tactic-mode proof.
91 unfold thermal_thrust c_speed
92 have h1 : spacecraft_thermal_power ≥ 0 := by unfold spacecraft_thermal_power; norm_num
93 have h2 : thermal_asymmetry ≥ 0 := by unfold thermal_asymmetry; norm_num
94 have h3 : (c_speed : ℝ) ≥ 0 := by unfold c_speed; norm_num
95 exact div_nonneg (mul_nonneg h1 h2) h3
96
97/-- **THEOREM EA-008.9**: The anomaly is dissolved under proper analysis. -/