Gravity Coherence Fall Coherence Defect Expand

The coherence defect

In classical physics, a gravitational field is a force per unit mass that varies with position. For an object of nonzero size, like a standing person, the field is slightly stronger at the feet than at the head. The difference matters for precision experiments and for understanding tidal effects. The Recognition Science framework models this situation with a simple numerical measure called the coherence defect: the absolute difference in total potential between the top and bottom of the object, where potential is a field's stored energy per unit mass at a given height.

The framework's library, a machine-checked collection of formal theorems, defines the defect for a linearized field. The declaration coherence_defect_expand is a lemma that expands the definition into explicit arithmetic, removing the intermediate definitions. It shows that the defect equals the absolute value of the difference between the potential at the object's top and the potential at its bottom, where each potential is the sum of the gravitational potential at the center of mass, the field's gradient times the offset, and the inertial potential from any acceleration of the reference frame. This is a purely algebraic restatement; it establishes no physics by itself.

The expansion matters because it leads to a closed form. A second lemma, coherence_defect_simplify, derives that the defect equals |2 × extent × (∂Φ + a)|, where extent is half the object's height, ∂Φ is the field's gradient at the center of mass, and a is the frame's acceleration. The formula shows the defect vanishes when a = −∂Φ, which is exactly the free-fall acceleration in the field. The framework then proves a theorem, falling_restores_coherence, that there exists a unique acceleration making the defect zero, and that this acceleration is the gravitational acceleration.

In plain terms, the framework's account of gravity is this: standing still in a gravitational field means experiencing a coherence defect, because the field pulls differently on different parts of the body. Free fall cancels the defect, restoring coherence. That is why free fall feels like weightlessness: the object is in the coherent state. The expansion lemma is the first step in that argument, but it only rewrites a definition; it does not itself assert that free fall restores coherence, nor that gravity exists. Those claims come from the later theorems, and the framework presents them as formal consequences of its definitions, not as measured facts about the physical world.

/-- Coherence Defect: Variance of the potential across the object.
    If Potential is flat, Defect is 0.
-/
def coherence_defect (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) : ℝ :=
  -- Difference in potential between Head (z = +extent) and Feet (z = -extent)
  let pot_head := total_potential_in_frame field obj a obj.extent
  let pot_feet := total_potential_in_frame field obj a (-obj.extent)
  abs (pot_head - pot_feet)

/-- Helper: expand coherence_defect into explicit arithmetic (no let bindings). -/
private lemma coherence_defect_expand (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
    coherence_defect field obj a =
      abs ((field.phi obj.h_cm + deriv field.phi obj.h_cm * obj.extent + a * obj.extent) -
           (field.phi obj.h_cm + deriv field.phi obj.h_cm * (-obj.extent) + a * (-obj.extent))) := by
  rfl

/-- 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

The expansion lemma alone does not assert that free fall restores coherence or that gravity exists. The framework does not claim its coherence defect is a measured physical quantity. The framework does not claim its linearized potential model is valid for strong gravitational fields.

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: