modified_coherence_defect_expand
plain-language theorem explainer
The lemma expands the definition of the modified coherence defect into an explicit difference of linearly approximated potentials evaluated at the head and feet of an extended object. Researchers deriving closed-form expressions for acoustic levitation or coherence-modified gravity would cite this step. The proof is a direct reflexivity after unfolding the definition of the modified coherence defect.
Claim. Let Φ be the potential of a processing field, Ψ the potential of an external phase field, h the center-of-mass position, L > 0 the object extent, and a ∈ ℝ the acceleration parameter. Then the modified coherence defect equals |[Φ(h) + Φ'(h)·L + Ψ(h) + Ψ'(h)·L + a·L] − [Φ(h) + Φ'(h)·(−L) + Ψ(h) + Ψ'(h)·(−L) + a·(−L)]|.
background
A ProcessingField supplies a potential function Φ : Position → ℝ. An ExternalPhaseField supplies an additional potential Ψ : Position → ℝ whose gradient is obtained by differentiation. An ExtendedObject is a structure carrying center-of-mass position h and positive extent L. The modified coherence defect is defined as the absolute difference between the modified total potential evaluated at +L and at −L. This extends the basic defect functional defect(x) = J(x) from the Law of Existence.
proof idea
The proof is a one-line wrapper that applies reflexivity after the definition of modified_coherence_defect is unfolded into the difference of the two modified_total_potential calls, each expanded with first-order derivative terms.
why it matters
The lemma is invoked by modified_coherence_defect_simplify to reach the closed form |2·extent·(∇Φ + ∇Ψ + a)|. It supports the acoustic_levitation and equilibrium_acceleration results in the same module and contributes to the analysis of external phase fields modifying gravitational coherence. The step fills the arithmetic bridge between the general defect definition and the simplified gradient expression used in levitation conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.