modified_coherence_defect_simplify

formal source

 103  rfl
 104
 105/-- Closed form: modified coherence defect = |2·extent·(∇Φ_grav + ∇Φ_ext + a)| -/
 106lemma modified_coherence_defect_simplify
 107    (field : ProcessingField) (ext : ExternalPhaseField)
 108    (obj : ExtendedObject) (a : ℝ) :
 109    modified_coherence_defect field ext obj a =
 110      abs (2 * obj.extent * (deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a)) := by
 111  rw [modified_coherence_defect_expand]
 112  congr 1
 113  ring
 114
 115/-! ## 3. The Levitation Theorem -/
 116
 117/-- THEOREM: Modified Falling Condition.
 118
 119    With an external phase field, the unique acceleration restoring coherence is
 120    a = -(∇Φ_grav + ∇Φ_ext), NOT just -∇Φ_grav.
 121
 122    The external field SHIFTS the equilibrium acceleration. -/
 123theorem modified_falling_condition
 124    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) :
 125    ∃! a : ℝ, modified_coherence_defect field ext obj a = 0 := by
 126  use -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm)
 127  refine ⟨?_, ?_⟩
 128  · show modified_coherence_defect field ext obj
 129        (-(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm)) = 0
 130    rw [modified_coherence_defect_simplify]
 131    have : deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm +
 132           -(deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm) = 0 := by ring
 133    rw [this, mul_zero, abs_zero]
 134  · intro a' h_zero
 135    rw [modified_coherence_defect_simplify] at h_zero
 136    have h0 : 2 * obj.extent * (deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a') = 0 := by