coherence_defect_of_combined
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply outside the weak-field regime where nonlinear interactions appear.
- Does not hold if either potential fails to be differentiable at the object's center of mass.
- Does not address strong-field or multi-body configurations.
- Does not incorporate higher-order corrections or quantum effects.
Lean usage
theorem use_in_justification (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ) (hg : DifferentiableAt ℝ pair.field_grav.phi obj.h_cm) (he : DifferentiableAt ℝ pair.field_ext.phi obj.h_cm) : coherence_defect pair.combined obj a = abs (2 * obj.extent * (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a)) := coherence_defect_of_combined pair obj a hg heformal statement (Lean)
89theorem coherence_defect_of_combined (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ)
90 (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi obj.h_cm)
91 (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi obj.h_cm) :
92 coherence_defect pair.combined obj a =
93 abs (2 * obj.extent *
94 (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a)) := by
proof body
Term-mode proof.
95 rw [coherence_defect_simplify]
96 congr 1; congr 1; congr 1
97 exact gradient_superposition pair obj.h_cm h_diff_grav h_diff_ext
98
99/-! ## 3. The Superposition Justification Certificate -/
100
101/-- Structure packaging the full weak-field superposition justification. -/