Gravity Coherence Fall Coherence Defect Simplify

The coherence defect

The coherence defect is a measure of how much a physical quantity varies across the length of an extended object. In the Recognition Science framework, the quantity is a potential function Φ(h), and the object is modeled as a segment with a center of mass and a positive extent. The defect is defined as the absolute difference between the potential at the object's head and at its feet, in a frame that may be accelerating. If the potential is flat, the defect is zero.

The declaration coherence_defect_simplify is a lemma in the framework's machine-checked library of formal theorems. It proves a closed form for this linearized defect: coherence_defect equals the absolute value of 2 times the extent times the sum of the potential's derivative at the center of mass and the frame's acceleration. The proof is a direct expansion using the definition and the algebraic ring tactic. This is a purely computational result; it does not by itself assert anything about gravity or falling.

The lemma's payoff appears in the theorem that follows it in the same file. That theorem, falling_restores_coherence, states that there exists a unique acceleration that reduces the linear coherence defect to zero. The closed form makes the uniqueness immediate: the defect is zero exactly when the acceleration equals the negative of the potential's derivative. The framework interprets this as gravity: a body at rest in a gravitational field experiences a coherence defect, while free fall cancels it. This is why free fall feels like nothing.

What the lemma does not claim is important. It does not prove that the potential function has any particular form, nor that the derivative is nonzero. It does not establish that the coherence defect is the correct physical measure of anything; that is a modeling choice. The lemma is a step in a formal derivation, not an empirical statement about the world. Its role is to make the subsequent theorem's proof short and transparent.

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

/-- 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 lemma does not prove that the potential function has any particular form. The lemma does not establish that the coherence defect is the correct physical measure of anything. The theorem does not claim that gravity is caused by the coherence defect, only that free fall cancels it.

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: