coherence_defect_simplify
The coherence_defect_simplify lemma supplies the closed algebraic expression for the linearized coherence defect as the absolute value of twice the object's extent times the sum of the potential gradient and frame acceleration. Gravitational physicists in the Recognition Science program cite it when reducing coherence variance across extended bodies in accelerating frames. The proof is a term-mode reduction that rewrites via the expansion lemma then applies congruence and ring normalization to the interior expression.
claimFor a processing field with potential function $Φ$ and an extended object with center-of-mass position $h_{cm}$ and positive extent $e$, the coherence defect at acceleration $a$ equals $|2e(Φ'(h_{cm})+a)|$.
background
In the CoherenceFall module a ProcessingField is a structure containing a potential function $Φ:$ Position $→ ℝ$. An ExtendedObject carries a center-of-mass position $h_{cm}$ together with a positive real extent. The coherence defect is defined as the absolute difference in total potential (gravitational plus frame term $a·z$) evaluated at the head and feet of the object under the linear approximation $Φ_{tot}(z)≈Φ(h_{cm}+z)+a z$ (see total_potential_in_frame).
proof idea
The term proof first rewrites the left-hand side with the coherence_defect_expand lemma, which replaces the let-bound definition by the explicit difference of potentials. It then applies congr 1 to isolate the argument of the absolute value and finishes with ring, which algebraically cancels to the factor $2·extent·(deriv Φ + a)$.
why it matters in Recognition Science
The lemma feeds the falling_restores_coherence theorem, which concludes there exists a unique acceleration $a=-Φ'(h_{cm})$ that nulls the defect and identifies it with gravitational acceleration $g=-∇Φ$. It is also invoked by coherence_defect_of_combined when superposing weak fields. In the Recognition framework it closes the linear step that shows free fall restores coherence, consistent with the equivalence principle in the gravity domain.
scope and limits
- Does not prove existence or uniqueness of the nulling acceleration.
- Does not treat nonlinear or higher-order terms in the potential.
- Does not apply outside the linear frame approximation.
- Does not address relativistic or curved-spacetime corrections.
formal statement (Lean)
77lemma coherence_defect_simplify (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
78 coherence_defect field obj a =
79 abs (2 * obj.extent * (deriv field.phi obj.h_cm + a)) := by
proof body
Term-mode proof.
80 rw [coherence_defect_expand]
81 congr 1
82 ring
83
84/-! ## The Theorem -/
85
86/-- Falling (Acceleration) Restores Coherence.
87
88 Theorem: There exists a unique acceleration `a` that reduces the
89 linear Coherence Defect to zero.
90
91 This `a` is exactly the gravitational acceleration `g = -∇Φ`.
92-/