coherence_defect_expand

formal source

  66  abs (pot_head - pot_feet)
  67
  68/-- Helper: expand coherence_defect into explicit arithmetic (no let bindings). -/
  69private lemma coherence_defect_expand (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
  70    coherence_defect field obj a =
  71      abs ((field.phi obj.h_cm + deriv field.phi obj.h_cm * obj.extent + a * obj.extent) -
  72           (field.phi obj.h_cm + deriv field.phi obj.h_cm * (-obj.extent) + a * (-obj.extent))) := by
  73  rfl
  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