c_speed
plain-language theorem explainer
Defines the speed of light as the fixed real number 299792458 in meters per second. Analysts working on spacecraft flyby anomalies under the Recognition Science verdict cite this constant when evaluating thermal thrust and acceleration contributions. The definition supplies the denominator in F = P_asym / c without any derivation step. It appears as a noncomputable constant to anchor SI-unit calculations in the experimental module.
Claim. The speed of light in vacuum is the constant $c = 299792458$ (m/s).
background
The module EA-008 examines unexpected energy changes during Earth gravity assists and concludes that standard physics suffices once thermal asymmetry and gravity model updates are included. The constant c_speed enters the thrust formula F = P_asym / c and the derived acceleration a = F / m for a nominal 1000 kg spacecraft. Upstream imports supply gap functions and distinction axioms that frame the broader Recognition Science setting, yet this declaration itself is a direct numerical assignment independent of those structures.
proof idea
Direct definition that assigns the integer literal 299792458 to a noncomputable real. No lemmas or tactics are applied; the body is a single equality to the standard SI value.
why it matters
Supplies the fixed denominator required by thermal_thrust, thermal_acceleration_positive, and bsm_not_needed. These downstream results establish that thermal thrust is nonnegative and that no beyond-standard-model physics is required, directly supporting the module verdict that thermal plus gravity updates suffice. The declaration therefore closes the numerical input for the experimental claim without touching the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.