modified_coherence_defect_simplify
plain-language theorem explainer
The lemma supplies the closed-form expression for the modified coherence defect when an external phase field is present, equating it to the absolute value of twice the object's extent times the sum of the gravitational gradient, external gradient, and acceleration. Researchers deriving acoustic levitation equilibria from Recognition Science principles would cite this reduction when analyzing coherence restoration under superimposed fields. The proof is a one-line algebraic wrapper that expands the defect definition and simplifies via ring.
Claim. The modified coherence defect for a processing field, external phase field, extended object, and acceleration $a$ equals $|2 · extent(obj) · (dΦ_grav/dh at center of mass + dΦ_ext/dh at center of mass + a)|.
background
In the AcousticPhaseLevitation module, coherence defects are extended to include external phase or acoustic fields that modify local processing potentials. The ExternalPhaseField structure supplies an additional potential ψ whose gradient is obtained by differentiation at a position. The modified coherence defect itself is defined via the absolute difference of modified total potentials evaluated at the head and feet of an ExtendedObject, which has extent and center-of-mass height. This lemma rests on the prior expansion of that difference into a linear expression in the gradients and acceleration.
proof idea
The proof rewrites the left-hand side with the modified_coherence_defect_expand lemma, then applies congr 1 followed by the ring tactic to algebraically collapse the difference of potentials into the stated closed form.
why it matters
This simplification is invoked in the acoustic_levitation theorem (which shows zero defect when the external gradient cancels the gravitational one at zero acceleration) and in the modified_falling_condition theorem (which establishes the unique restoring acceleration as the negative sum of both gradients). It supplies the algebraic bridge needed to derive phase-based levitation from the Recognition Science coherence framework, directly supporting the shift from pure gravitational to modified equilibrium conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.