pith. machine review for the scientific record. sign in
theorem proved term proof high

standard_physics_sufficient

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  86theorem standard_physics_sufficient : thermal_asymmetry > 0 :=

proof body

Term-mode proof.

  87  thermal_can_produce_thrust
  88
  89/-- **THEOREM EA-008.8**: No BSM physics is needed. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.