coherence_defect_of_combined
plain-language theorem explainer
The coherence defect of a combined weak-field pair equals the absolute value of twice the object's extent times the sum of the gravitational and external potential gradients at the center of mass plus the acceleration term. Physicists deriving linear approximations in Recognition Science gravity would cite this to confirm defect additivity. The proof is a one-line wrapper that rewrites via the closed-form defect lemma and substitutes the gradient superposition result.
Claim. Let $P_g$ and $P_e$ be gravitational and external processing fields forming a weak-field pair, with combined potential the pointwise sum. For an extended object with center-of-mass position $h_{cm}$ and positive extent $r$, and real parameter $a$, assuming differentiability of both potentials at $h_{cm}$, the coherence defect of the combined field satisfies $D = |2r (P_g'(h_{cm}) + P_e'(h_{cm}) + a)|$.
background
A WeakFieldPair consists of two independent ProcessingField structures (gravitational and external) whose combined potential is their pointwise sum. The coherence_defect of a field across an ExtendedObject (defined by center-of-mass height $h_{cm}$ and positive extent) is the absolute difference in total potential between head and feet positions. The upstream lemma coherence_defect_simplify reduces this exactly to the absolute value of twice the extent times the derivative of the potential plus the acceleration parameter $a$.
proof idea
The proof rewrites the left-hand side with coherence_defect_simplify to expose the absolute-value expression involving the combined derivative. Congruence tactics align the subexpressions, after which gradient_superposition is applied exactly to replace the combined derivative by the sum of the individual gradients.
why it matters
This result supplies the coherence_defect_additivity component inside the superposition_justified theorem, which packages the full weak-field justification (quadratic regime, gradient additivity, and defect additivity) from RS first principles. It directly supports the claim that weak-field gravity emerges from linear processing-field superposition in the Gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.