falling_restores_coherence

proof body

Tactic-mode proof.

  95  -- We want |2 * e * (ϕ' + a)| = 0 ⇒ a = -ϕ' (since e > 0).
  96  -- This is exactly "Falling with acceleration = -Gradient".
  97  use -(deriv field.phi obj.h_cm)
  98  constructor
  99  · -- Existence
 100    -- | 2 * e * (ϕ' + (-ϕ')) | = |0| = 0
 101    simp [coherence_defect_simplify]
 102  · -- Uniqueness
 103    intro a' h_zero
 104    -- Reduce to a product equals zero
 105    have h0 : 2 * obj.extent * (deriv field.phi obj.h_cm + a') = 0 := by
 106      simpa [coherence_defect_simplify, abs_eq_zero] using h_zero
 107    -- From |x| = 0 we get x = 0
 108    -- Since obj.extent > 0, we have 2 * obj.extent ≠ 0
 109    have h_extent_pos : (0 : ℝ) < 2 * obj.extent := by
 110      have htwo : (0 : ℝ) < 2 := by norm_num
 111      exact mul_pos htwo obj.extent_pos
 112    have h_extent_ne : 2 * obj.extent ≠ 0 := ne_of_gt h_extent_pos
 113    -- So (deriv field.phi obj.h_cm + a') = 0
 114    have h2 : deriv field.phi obj.h_cm + a' = 0 := by
 115      have := mul_eq_zero.mp h0
 116      cases this with
 117      | inl h => exact absurd h h_extent_ne
 118      | inr h => exact h
 119    -- Therefore a' = -(deriv field.phi obj.h_cm)
 120    linarith
 121
 122/-! ## Interpretation
 123
 124"Gravity" is the requirement to accelerate in order to maintain
 125a locally constant processing environment (Coherence).
 126
 127In this view:
 128- Standing still (a = 0) in a gravitational field means experiencing a coherence defect
 129- Free-falling (a = -∇Φ) cancels the defect, restoring coherence
 130- This is why free fall feels like nothing: you're in the coherent state
 131-/
 132
 133end IndisputableMonolith.Gravity