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

love_equilibrates

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)

  88theorem love_equilibrates (alpha : ℝ) (ha : 0 < alpha) (ha1 : alpha ≤ 1)
  89    (s₁ s₂ : AgentState) :
  90    |((loveOperator alpha ha ha1).apply s₁ s₂).1.sigma -
  91     ((loveOperator alpha ha ha1).apply s₁ s₂).2.sigma| ≤
  92    |s₁.sigma - s₂.sigma| := by

proof body

Tactic-mode proof.

  93  simp only [loveOperator, CrossLatticeTransform.apply]
  94  have h : s₁.sigma + alpha * ((s₁.sigma + s₂.sigma) / 2 - s₁.sigma) -
  95           (s₂.sigma + alpha * ((s₁.sigma + s₂.sigma) / 2 - s₂.sigma)) =
  96           (1 - alpha) * (s₁.sigma - s₂.sigma) := by ring
  97  rw [h]
  98  rw [abs_mul]
  99  have h1a : |1 - alpha| ≤ 1 := by
 100    rw [abs_le]; constructor <;> linarith
 101  calc |1 - alpha| * |s₁.sigma - s₂.sigma|
 102      ≤ 1 * |s₁.sigma - s₂.sigma| := by nlinarith [abs_nonneg (s₁.sigma - s₂.sigma)]
 103    _ = |s₁.sigma - s₂.sigma| := one_mul _
 104
 105end
 106
 107end IndisputableMonolith.Ethics.LoveUniquenessDerivation

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.