modified_total_potential

formal source

  73    in a frame accelerating with `a`.
  74    Φ_total(z) = Φ_grav(h_cm + z) + Φ_ext(h_cm + z) + a·z
  75    (linearized around center of mass) -/
  76def modified_total_potential
  77    (field : ProcessingField) (ext : ExternalPhaseField)
  78    (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
  79  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  80  let phi_ext := ext.psi obj.h_cm + (deriv ext.psi obj.h_cm) * z
  81  let phi_acc := a * z
  82  phi_grav + phi_ext + phi_acc
  83
  84/-- Modified coherence defect with external phase field present. -/
  85def modified_coherence_defect
  86    (field : ProcessingField) (ext : ExternalPhaseField)
  87    (obj : ExtendedObject) (a : ℝ) : ℝ :=
  88  let pot_head := modified_total_potential field ext obj a obj.extent
  89  let pot_feet := modified_total_potential field ext obj a (-obj.extent)
  90  abs (pot_head - pot_feet)
  91
  92/-- Helper: expand modified_coherence_defect into explicit arithmetic. -/
  93private lemma modified_coherence_defect_expand
  94    (field : ProcessingField) (ext : ExternalPhaseField)
  95    (obj : ExtendedObject) (a : ℝ) :
  96    modified_coherence_defect field ext obj a =
  97      abs ((field.phi obj.h_cm + deriv field.phi obj.h_cm * obj.extent +
  98            (ext.psi obj.h_cm + deriv ext.psi obj.h_cm * obj.extent) +
  99            a * obj.extent) -
 100           (field.phi obj.h_cm + deriv field.phi obj.h_cm * (-obj.extent) +
 101            (ext.psi obj.h_cm + deriv ext.psi obj.h_cm * (-obj.extent)) +
 102            a * (-obj.extent))) := by
 103  rfl
 104
 105/-- Closed form: modified coherence defect = |2·extent·(∇Φ_grav + ∇Φ_ext + a)| -/
 106lemma modified_coherence_defect_simplify