thermal_thrust
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values of thermal power or asymmetry from Recognition Science axioms.
- Does not incorporate the gravity-model updates referenced in the module verdict.
- Does not compute the resulting velocity shift for any specific flyby trajectory.
- Does not address relativistic beaming or higher-order geometric effects.
formal statement (Lean)
47noncomputable def thermal_thrust : ℝ :=
proof body
Definition body.
48 spacecraft_thermal_power * thermal_asymmetry / c_speed
49
50/-- Resulting acceleration (m/s²). a = F / m for ~1000 kg spacecraft -/