modified_coherence_defect_simplify
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove existence or stability of any concrete external phase field.
- Assumes the processing field and object obey the coherence defect definitions without further constraints.
- Does not address time-dependent fields or motion beyond the vertical height coordinate.
- Remains within the classical one-dimensional coherence model.
Lean usage
rw [modified_coherence_defect_simplify]formal statement (Lean)
106lemma modified_coherence_defect_simplify
107 (field : ProcessingField) (ext : ExternalPhaseField)
108 (obj : ExtendedObject) (a : ℝ) :
109 modified_coherence_defect field ext obj a =
110 abs (2 * obj.extent * (deriv field.phi obj.h_cm + deriv ext.psi obj.h_cm + a)) := by
proof body
Term-mode proof.
111 rw [modified_coherence_defect_expand]
112 congr 1
113 ring
114
115/-! ## 3. The Levitation Theorem -/
116
117/-- THEOREM: Modified Falling Condition.
118
119 With an external phase field, the unique acceleration restoring coherence is
120 a = -(∇Φ_grav + ∇Φ_ext), NOT just -∇Φ_grav.
121
122 The external field SHIFTS the equilibrium acceleration. -/