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

coherence_defect_of_combined

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)

  89theorem coherence_defect_of_combined (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ)
  90    (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi obj.h_cm)
  91    (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi obj.h_cm) :
  92    coherence_defect pair.combined obj a =
  93    abs (2 * obj.extent *
  94      (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a)) := by

proof body

Term-mode proof.

  95  rw [coherence_defect_simplify]
  96  congr 1; congr 1; congr 1
  97  exact gradient_superposition pair obj.h_cm h_diff_grav h_diff_ext
  98
  99/-! ## 3. The Superposition Justification Certificate -/
 100
 101/-- Structure packaging the full weak-field superposition justification. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.