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

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)

  77lemma coherence_defect_simplify (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
  78    coherence_defect field obj a =
  79      abs (2 * obj.extent * (deriv field.phi obj.h_cm + a)) := by

proof body

Term-mode proof.

  80  rw [coherence_defect_expand]
  81  congr 1
  82  ring
  83
  84/-! ## The Theorem -/
  85
  86/-- Falling (Acceleration) Restores Coherence.
  87
  88    Theorem: There exists a unique acceleration `a` that reduces the
  89    linear Coherence Defect to zero.
  90
  91    This `a` is exactly the gravitational acceleration `g = -∇Φ`.
  92-/

used by (2)

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

depends on (10)

Lean names referenced from this declaration's body.