coherence_defect_simplify

formal source

  74
  75/-- Closed form for the linearized coherence defect:
  76    `coherence_defect = | 2 * extent * (∂ϕ + a) |`. -/
  77lemma coherence_defect_simplify (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
  78    coherence_defect field obj a =
  79      abs (2 * obj.extent * (deriv field.phi obj.h_cm + a)) := by
  80  rw [coherence_defect_expand]
  81  congr 1
  82  ring
  83
  84/-! ## The Theorem -/
  85
  86/-- Falling (Acceleration) Restores Coherence.
  87
  88    Theorem: There exists a unique acceleration `a` that reduces the
  89    linear Coherence Defect to zero.
  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