standard_physics_sufficient
plain-language theorem explainer
Standard physics explains the flyby anomaly once spacecraft thermal emission asymmetry is positive. Experimental physicists modeling Earth gravity assists would cite this result to close the case without new physics. The proof is a direct term reference to the companion theorem on thermal thrust production.
Claim. The thermal emission asymmetry of the spacecraft is positive, confirming that standard physics accounts for the observed velocity shifts during gravity assists.
background
The module analyzes the flyby anomaly as unexpected energy changes in spacecraft during Earth gravity assists, with the RS verdict that thermal effects plus gravity model updates suffice. thermal_asymmetry is introduced as the noncomputable real 0.03, representing the percentage difference in thermal emission. The upstream theorem thermal_can_produce_thrust states that this asymmetry can produce the required thrust and is documented under the thermal recoil explanation section.
proof idea
The proof is a term-mode one-liner that directly applies thermal_can_produce_thrust. That lemma unfolds the definition of thermal_asymmetry and uses norm_num to establish the inequality for the fixed value 0.03.
why it matters
This theorem realizes THEOREM EA-008.7 and feeds the ea008_certificate, which declares the anomaly dissolved after listing the 3 percent asymmetry check. It supports the module verdict that no BSM physics is needed. The result stays within empirical thermal modeling and does not engage core Recognition Science elements such as the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.