coherence_defect_simplify
plain-language theorem explainer
The lemma derives the closed-form expression for the coherence defect of an extended object under linear potential approximation in an accelerating frame. Researchers modeling the equivalence principle via coherence restoration would reference this identity when simplifying defect calculations. The proof proceeds by rewriting the defect definition via its expansion lemma followed by algebraic normalization with ring.
Claim. Let $phi$ be the potential of a processing field and let an extended object have center-of-mass position $h_{cm}$ and positive extent $e$. Then the coherence defect at acceleration $a$ satisfies $|2e (phi'(h_{cm}) + a)|$.
background
ProcessingField is a structure holding a differentiable potential function $phi : Position to R$. ExtendedObject consists of a center-of-mass position $h_{cm}$ together with a positive scalar extent. The coherence_defect functional measures the absolute difference in total potential (gravitational plus frame acceleration term) evaluated at the head and feet of the object. The upstream lemma coherence_defect_expand supplies the explicit arithmetic form of this difference before simplification.
proof idea
The proof applies the rewrite rule coherence_defect_expand to replace the defect definition with its expanded arithmetic expression. It then uses congr 1 to focus on the argument of the absolute value, followed by the ring tactic to cancel symmetric terms and obtain the factorized form.
why it matters
This simplification is invoked directly by the theorem falling_restores_coherence, which concludes that the unique acceleration nulling the defect is exactly the negative gradient of the potential, i.e., gravitational free-fall acceleration. It is also used in the superposition result coherence_defect_of_combined for combined fields. Within the Recognition Science framework the identity supports the derivation of gravitational acceleration as the coherence-restoring term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.