pith. machine review for the scientific record. sign in
lemma proved term proof

modified_coherence_defect_simplify

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.