coherence_defect_simplify
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.