thermal_thrust
plain-language theorem explainer
Thermal thrust is the force in newtons arising from asymmetric thermal emission on a spacecraft. Analysts of the flyby anomaly cite this quantity to quantify the contribution of standard thermal radiation to observed velocity shifts. The definition is a direct one-line algebraic expression that multiplies the module's thermal-power and asymmetry constants and divides by the speed of light.
Claim. The thermal thrust $F$ satisfies $F = P_thermal * alpha / c$, where $P_thermal$ is spacecraft thermal power in watts, $alpha$ is the fractional asymmetry in thermal emission, and $c$ is the speed of light.
background
In the EA-008 module the flyby anomaly receives a Recognition Science analysis whose verdict is that thermal radiation plus gravity-model updates suffice to explain unexpected energy changes during Earth gravity assists. The definition draws on three module-local constants: spacecraft thermal power (approximately 300 W), thermal asymmetry (0.03), and c_speed (exactly 299792458 m/s). These enter the thrust formula directly; upstream constants supply the numerical value of c while the power and asymmetry parameters are taken from typical spacecraft engineering estimates.
proof idea
The definition is a direct one-line algebraic expression that multiplies spacecraft thermal power by thermal asymmetry and divides by c_speed. It applies no lemmas beyond the module-local constants and functions as a one-line wrapper for the physical relation F equals asymmetric power over c.
why it matters
This definition supplies the force term used by the downstream theorems anomaly_dissolved, bsm_not_needed, and pattern_matches_thermal, which establish that the anomaly is dissolved and that no beyond-standard-model physics is required. It fills the EA-008 steps that compare the computed thrust against the mm/s-scale anomaly and confirm non-negativity. Within the Recognition framework the construction remains inside the experimental domain and is consistent with the scaling constraints already fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.