def
definition
modified_coherence_defect
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.AcousticPhaseLevitation on GitHub at line 85.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
82 phi_grav + phi_ext + phi_acc
83
84/-- Modified coherence defect with external phase field present. -/
85def modified_coherence_defect
86 (field : ProcessingField) (ext : ExternalPhaseField)
87 (obj : ExtendedObject) (a : ℝ) : ℝ :=
88 let pot_head := modified_total_potential field ext obj a obj.extent
89 let pot_feet := modified_total_potential field ext obj a (-obj.extent)
90 abs (pot_head - pot_feet)
91
92/-- Helper: expand modified_coherence_defect into explicit arithmetic. -/
93private lemma modified_coherence_defect_expand
94 (field : ProcessingField) (ext : ExternalPhaseField)
95 (obj : ExtendedObject) (a : ℝ) :
96 modified_coherence_defect field ext obj a =
97 abs ((field.phi obj.h_cm + deriv field.phi obj.h_cm * obj.extent +
98 (ext.psi obj.h_cm + deriv ext.psi obj.h_cm * obj.extent) +
99 a * obj.extent) -
100 (field.phi obj.h_cm + deriv field.phi obj.h_cm * (-obj.extent) +
101 (ext.psi obj.h_cm + deriv ext.psi obj.h_cm * (-obj.extent)) +
102 a * (-obj.extent))) := by
103 rfl
104
105/-- Closed form: modified coherence defect = |2·extent·(∇Φ_grav + ∇Φ_ext + a)| -/
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
111 rw [modified_coherence_defect_expand]
112 congr 1
113 ring
114
115/-! ## 3. The Levitation Theorem -/