coherence_defect

formal source

  59/-- Coherence Defect: Variance of the potential across the object.
  60    If Potential is flat, Defect is 0.
  61-/
  62def coherence_defect (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) : ℝ :=
  63  -- Difference in potential between Head (z = +extent) and Feet (z = -extent)
  64  let pot_head := total_potential_in_frame field obj a obj.extent
  65  let pot_feet := total_potential_in_frame field obj a (-obj.extent)
  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-/