c_speed
The declaration assigns the SI value of the speed of light as a real number. Analysts of the flyby anomaly cite it when converting thermal power asymmetry into thrust. The definition is a direct constant assignment with no derivation or computation steps.
claimThe speed of light is the constant $c = 299792458$ in meters per second.
background
The module analyzes the flyby anomaly as an Earth gravity-assist effect and concludes that thermal radiation asymmetry plus standard gravity modeling accounts for the observed velocity shifts. The speed of light appears as the denominator in the thrust relation $F = P_{asym}/c$, converting power into force for spacecraft of typical mass. Upstream imports supply gap functions $F(Z) = log(1 + Z/φ)/log(φ)$ and the master generator $F(z) = log(1 + z/φ)$, which fix the Recognition Science constants used in the broader mass and coupling ladders.
proof idea
Direct noncomputable definition that binds the literal integer 299792458 to the identifier c_speed.
why it matters in Recognition Science
The constant feeds the thermal_thrust definition, which is unfolded to establish thermal_acceleration_positive and the theorem that no beyond-standard-model physics is required. It therefore supports the module-level claim that thermal plus gravity updates suffice for the anomaly. The placement keeps all numerical constants explicit while the rest of the Recognition Science chain (T5 J-uniqueness through T8 D=3) remains in native phi units.
scope and limits
- Does not derive the numerical value from Recognition Science axioms or the phi ladder.
- Does not incorporate variable-c or quantum-gravity corrections.
- Does not specify the reference frame or medium in which the value is measured.
- Does not link the constant to the alpha band or G = phi^5/pi relations.
Lean usage
unfold c_speedformal statement (Lean)
44noncomputable def c_speed : ℝ := 299792458
proof body
Definition body.
45
46/-- Thrust from thermal asymmetry (N). F = P_asym / c -/