Gravity Coherence Fall Total Potential In Frame

The local potential

In classical physics, a falling elevator is a local inertial frame: inside it, gravity seems to vanish. The Recognition Science declaration total_potential_in_frame formalizes the same idea in the framework's own terms. It defines the total potential at a point z relative to an object's center of mass, in a frame accelerating with acceleration a, as the sum of two parts: the gravitational potential from the field, linearly approximated around the center, plus an inertial potential equal to a times z. The declaration is a definition, not a theorem; it chooses how to combine the two effects.

The choice matters because it makes the later theorem possible. With this definition, the coherence defect, the variance of potential across an extended object, becomes a simple closed form: the absolute value of twice the object's extent times the sum of the field's derivative and the acceleration. The framework's library proves that there exists a unique acceleration that drives this defect to zero, and that this acceleration is exactly the gravitational acceleration. This is the formal version of the falling-elevator thought experiment: free fall cancels the gradient, so the potential is flat across the object.

The library's interpretation section states the physical picture plainly: standing still in a gravitational field means experiencing a coherence defect, while free falling cancels it. The declaration itself, however, does not claim that this is the only way to define total potential, nor does it assert that real gravity is caused by acceleration. It only establishes the linearized combination of gravitational and inertial potentials in a local frame, and the coherence defect that follows from that choice.

/-- Total Potential in a frame accelerating with `a` at position `h` (relative to CM).
    Φ_tot(z) ≈ Φ_grav(h_cm + z) + a * z
    (Linear approximation for local frame)
-/
def total_potential_in_frame (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
  -- Taylor expand phi around h_cm: phi(h_cm) + phi'(h_cm) * z
  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  -- Inertial potential from acceleration a (pointing up? a is vertical acceleration)
  -- If object accelerates down (a < 0), inertial force is up.
  -- Potential Φ_acc such that F = -∇Φ_acc. F_inertial = -a, hence Φ_acc = a * z.
  let phi_acc := a * z

  phi_grav + phi_acc

/-- Closed form for the linearized coherence defect:
    `coherence_defect = | 2 * extent * (∂ϕ + a) |`. -/
lemma coherence_defect_simplify (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
    coherence_defect field obj a =
      abs (2 * obj.extent * (deriv field.phi obj.h_cm + a)) := by
  rw [coherence_defect_expand]
  congr 1
  ring

/-- Falling (Acceleration) Restores Coherence.

    Theorem: There exists a unique acceleration `a` that reduces the
    linear Coherence Defect to zero.

    This `a` is exactly the gravitational acceleration `g = -∇Φ`.
-/
theorem falling_restores_coherence (field : ProcessingField) (obj : ExtendedObject) :
    ∃! a : ℝ, coherence_defect field obj a = 0 := by
  -- We want |2 * e * (ϕ' + a)| = 0 ⇒ a = -ϕ' (since e > 0).
  -- This is exactly "Falling with acceleration = -Gradient".
  use -(deriv field.phi obj.h_cm)
  constructor
  · -- Existence
    -- | 2 * e * (ϕ' + (-ϕ')) | = |0| = 0
    simp [coherence_defect_simplify]
  · -- Uniqueness
    intro a' h_zero
    -- Reduce to a product equals zero
    have h0 : 2 * obj.extent * (deriv field.phi obj.h_cm + a') = 0 := by
      simpa [coherence_defect_simplify, abs_eq_zero] using h_zero
    -- From |x| = 0 we get x = 0
    -- Since obj.extent > 0, we have 2 * obj.extent ≠ 0
    have h_extent_pos : (0 : ℝ) < 2 * obj.extent := by
      have htwo : (0 : ℝ) < 2 := by norm_num
      exact mul_pos htwo obj.extent_pos
    have h_extent_ne : 2 * obj.extent ≠ 0 := ne_of_gt h_extent_pos
    -- So (deriv field.phi obj.h_cm + a') = 0
    have h2 : deriv field.phi obj.h_cm + a' = 0 := by
      have := mul_eq_zero.mp h0
      cases this with
      | inl h => exact absurd h h_extent_ne
      | inr h => exact h
    -- Therefore a' = -(deriv field.phi obj.h_cm)
    linarith

What this page does not claim

It does not claim that the total potential is defined non-linearly or exactly in strong fields. It does not claim that gravity itself is caused by acceleration; that interpretation is a separate, informal reading in the library. It does not claim that the coherence defect is the only measure of gravitational effects on extended objects.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/CoherenceFall.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: