total_potential_in_frame

formal source

  46    Φ_tot(z) ≈ Φ_grav(h_cm + z) + a * z
  47    (Linear approximation for local frame)
  48-/
  49def total_potential_in_frame (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
  50  -- Taylor expand phi around h_cm: phi(h_cm) + phi'(h_cm) * z
  51  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  52  -- Inertial potential from acceleration a (pointing up? a is vertical acceleration)
  53  -- If object accelerates down (a < 0), inertial force is up.
  54  -- Potential Φ_acc such that F = -∇Φ_acc. F_inertial = -a, hence Φ_acc = a * z.
  55  let phi_acc := a * z
  56
  57  phi_grav + phi_acc
  58
  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