pattern_matches_thermal
The result establishes that thermal thrust is non-negative, confirming consistency with a conventional thermal explanation for spacecraft flyby energy shifts. Analysts of gravity-assist trajectories would cite it to exclude the need for beyond-standard-model contributions. The proof is a direct term reference to the prior theorem that unfolds the thrust definition and verifies non-negativity of its factors.
claimThe thermal thrust defined by $F = P_ {asym} / c$ satisfies $F ≥ 0$.
background
The module analyzes the flyby anomaly as unexpected energy changes during Earth gravity assists and concludes that standard physics suffices. Thermal thrust is defined as spacecraft_thermal_power times thermal_asymmetry divided by c_speed, representing net force from uneven thermal emission. The upstream theorem bsm_not_needed states 'No BSM physics is needed' and proves the identical inequality by unfolding the definition then applying non-negativity of power, asymmetry, and c via norm_num.
proof idea
The proof is a one-line term wrapper that directly applies the theorem bsm_not_needed.
why it matters in Recognition Science
This theorem supplies the final certificate in the EA-008 sequence, showing the thermal hypothesis yields non-negative thrust and thereby supports the module verdict that thermal plus gravity updates explain the anomaly. It aligns with Recognition Science experimental claims that observed discrepancies remain inside standard derivations without new constants or dimensions.
scope and limits
- Does not quantify the size of any observed velocity shift.
- Does not simulate specific spacecraft mass or power profiles.
- Does not incorporate updates to the gravity model itself.
- Does not address anomalies outside thermal radiation effects.
formal statement (Lean)
102theorem pattern_matches_thermal : thermal_thrust ≥ 0 := bsm_not_needed
proof body
Term-mode proof.
103
104/-- **EA-008 Certificate** -/