falling_restores_coherence

formal source

  90
  91    This `a` is exactly the gravitational acceleration `g = -∇Φ`.
  92-/
  93theorem falling_restores_coherence (field : ProcessingField) (obj : ExtendedObject) :
  94    ∃! a : ℝ, coherence_defect field obj a = 0 := by
  95  -- We want |2 * e * (ϕ' + a)| = 0 ⇒ a = -ϕ' (since e > 0).
  96  -- This is exactly "Falling with acceleration = -Gradient".
  97  use -(deriv field.phi obj.h_cm)
  98  constructor
  99  · -- Existence
 100    -- | 2 * e * (ϕ' + (-ϕ')) | = |0| = 0
 101    simp [coherence_defect_simplify]
 102  · -- Uniqueness
 103    intro a' h_zero
 104    -- Reduce to a product equals zero
 105    have h0 : 2 * obj.extent * (deriv field.phi obj.h_cm + a') = 0 := by
 106      simpa [coherence_defect_simplify, abs_eq_zero] using h_zero
 107    -- From |x| = 0 we get x = 0
 108    -- Since obj.extent > 0, we have 2 * obj.extent ≠ 0
 109    have h_extent_pos : (0 : ℝ) < 2 * obj.extent := by
 110      have htwo : (0 : ℝ) < 2 := by norm_num
 111      exact mul_pos htwo obj.extent_pos
 112    have h_extent_ne : 2 * obj.extent ≠ 0 := ne_of_gt h_extent_pos
 113    -- So (deriv field.phi obj.h_cm + a') = 0
 114    have h2 : deriv field.phi obj.h_cm + a' = 0 := by
 115      have := mul_eq_zero.mp h0
 116      cases this with
 117      | inl h => exact absurd h h_extent_ne
 118      | inr h => exact h
 119    -- Therefore a' = -(deriv field.phi obj.h_cm)
 120    linarith
 121
 122/-! ## Interpretation
 123