c_speed

formal source

  41/-! ## II. Thermal Recoil Explanation -/
  42
  43/-- Speed of light constant (m/s). -/
  44noncomputable def c_speed : ℝ := 299792458
  45
  46/-- Thrust from thermal asymmetry (N). F = P_asym / c -/
  47noncomputable def thermal_thrust : ℝ :=
  48  spacecraft_thermal_power * thermal_asymmetry / c_speed
  49
  50/-- Resulting acceleration (m/s²). a = F / m for ~1000 kg spacecraft -/
  51noncomputable def thermal_acceleration : ℝ := thermal_thrust / 1000
  52
  53/-- **THEOREM EA-008.3**: Thermal acceleration is positive. -/
  54theorem thermal_acceleration_positive : thermal_acceleration ≥ 0 := by
  55  unfold thermal_acceleration thermal_thrust c_speed
  56  have h1 : spacecraft_thermal_power ≥ 0 := by unfold spacecraft_thermal_power; norm_num
  57  have h2 : thermal_asymmetry ≥ 0 := by unfold thermal_asymmetry; norm_num
  58  have h3 : (c_speed : ℝ) ≥ 0 := by unfold c_speed; norm_num
  59  exact div_nonneg (div_nonneg (mul_nonneg h1 h2) h3) (by norm_num)
  60
  61/-- **THEOREM EA-008.4**: Thermal effect scales with power. -/
  62theorem thermal_scales_with_power : spacecraft_thermal_power > 0 := by
  63  unfold spacecraft_thermal_power
  64  norm_num
  65
  66/-! ## III. Gravity Model Updates -/
  67
  68/-- Earth gravity model accuracy (m/s²). EGM2008: ~10⁻⁹ g at surface -/
  69noncomputable def gravity_model_accuracy : ℝ := 1e-9 * 9.81
  70
  71/-- Uncertainty in velocity from gravity model (mm/s). -/
  72noncomputable def gravity_velocity_uncertainty : ℝ := 2.0
  73
  74/-- **THEOREM EA-008.5**: Gravity model uncertainty comparable to anomaly. -/