thermal_acceleration
plain-language theorem explainer
The definition sets thermal acceleration to thermal thrust divided by 1000, yielding the resulting acceleration in m/s² for an approximate 1000 kg spacecraft. Analysts modeling the flyby anomaly cite this quantity when estimating the size of thermally driven velocity shifts. It is obtained by direct scaling of the upstream thermal_thrust expression.
Claim. The acceleration is $a = F / 1000$, where $F$ is the thrust from thermal asymmetry given by $P_{asym} / c$.
background
The FlybyAnomaly module concludes that the observed anomaly admits a standard-physics account via thermal effects together with gravity-model updates. Thermal_thrust supplies the force $F = P_{asym} / c$ obtained from asymmetric spacecraft power divided by the speed of light. The present definition normalizes that force by an assumed spacecraft mass of 1000 kg to produce acceleration in m/s² units.
proof idea
This is a one-line definition that divides the value of thermal_thrust by 1000.
why it matters
The quantity is invoked directly by the downstream theorem thermal_acceleration_positive, which establishes non-negativity. It thereby supports the module's claim that thermal thrust can account for measurable flyby effects without invoking new physics, consistent with the RS verdict that thermal plus gravity updates suffice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.