coherence_defect_expand
plain-language theorem explainer
The lemma expands the coherence defect for an extended object in an accelerating frame into the absolute difference of linearized total potentials evaluated at the positive and negative extremities. Modelers deriving closed-form coherence loss in gravitational settings cite this step when moving from the general defect definition to its local arithmetic form. The proof is a one-line reflexivity that unfolds the total potential approximation and the coherence defect definition.
Claim. Let $h$ be the center-of-mass position of an extended object with positive extent $e$, let $a$ be the frame acceleration, and let $phi$ be the potential function of a processing field. The coherence defect then equals $|(phi(h) + phi'(h) e + a e) - (phi(h) + phi'(h) (-e) + a (-e))|$.
background
ProcessingField is a structure containing a potential function $phi : Position to real numbers. ExtendedObject carries a center-of-mass position $h_cm$, a positive extent, and the linear frame approximation $Phi_tot(z) approx phi(h_cm + z) + a z$, which expands to $phi(h_cm) + phi'(h_cm) z + a z$ at the extremities. Coherence defect is the absolute difference of these total potentials at $z = +e$ and $z = -e$. The lemma lives in the Gravity.CoherenceFall module and rests on the defect functional from LawOfExistence, where defect(x) equals J(x).
proof idea
The proof is a single reflexivity tactic. It unfolds the definition of coherence_defect, substitutes the linear total-potential expression at the two extremities, and obtains the explicit arithmetic difference shown in the signature.
why it matters
The expansion feeds directly into coherence_defect_simplify, which reduces the expression to the closed form absolute value of 2 times extent times (partial phi plus a). It supplies the intermediate arithmetic step required to quantify coherence loss under acceleration in the Recognition Science gravity development and connects the J-functional defect to the local frame analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.