modified_falling_condition

formal source

 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
 137      rwa [abs_eq_zero] at h_zero
 138    have h_extent_pos : (0 : ℝ) < 2 * obj.extent :=
 139      mul_pos (by norm_num : (0 : ℝ) < 2) obj.extent_pos
 140    have h_extent_ne : 2 * obj.extent ≠ 0 := ne_of_gt h_extent_pos
 141    have h2 : deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a' = 0 := by
 142      cases mul_eq_zero.mp h0 with
 143      | inl h => exact absurd h h_extent_ne
 144      | inr h => exact h
 145    linarith
 146
 147/-- LEVITATION THEOREM: If the external phase field gradient exactly cancels
 148    the gravitational gradient at the object's position, then the coherence-restoring
 149    acceleration is ZERO. The object maintains coherence while stationary.
 150
 151    This IS acoustic/phase levitation derived from RS first principles. -/
 152theorem acoustic_levitation
 153    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject)