loveOperator

formal source

  59
  60/-- The Love operator: equilibrates sigma between two agents.
  61    Each agent's sigma moves toward the mean. -/
  62def loveOperator (alpha : ℝ) (ha : 0 < alpha) (ha1 : alpha ≤ 1) :
  63    CrossLatticeTransform where
  64  apply := fun s₁ s₂ =>
  65    let mean := (s₁.sigma + s₂.sigma) / 2
  66    let s₁' := { s₁ with sigma := s₁.sigma + alpha * (mean - s₁.sigma) }
  67    let s₂' := { s₂ with sigma := s₂.sigma + alpha * (mean - s₂.sigma) }
  68    (s₁', s₂')
  69  conserves_total := by
  70    intro s₁ s₂; simp; ring
  71
  72/-- Love changes individual sigma when agents have different sigma:
  73    the new sigma differs from the old. -/
  74theorem love_changes_individual_sigma (alpha : ℝ) (ha : 0 < alpha) (ha1 : alpha ≤ 1)
  75    (s₁ s₂ : AgentState) (h_diff : s₁.sigma ≠ s₂.sigma) :
  76    ((loveOperator alpha ha ha1).apply s₁ s₂).1.sigma ≠ s₁.sigma := by
  77  simp only [loveOperator, CrossLatticeTransform.apply]
  78  intro h_eq
  79  have : alpha * ((s₁.sigma + s₂.sigma) / 2 - s₁.sigma) = 0 := by linarith
  80  rcases mul_eq_zero.mp this with h_alpha | h_mean
  81  · linarith
  82  · have : (s₁.sigma + s₂.sigma) / 2 = s₁.sigma := by linarith
  83    have : s₁.sigma + s₂.sigma = 2 * s₁.sigma := by linarith
  84    have : s₂.sigma = s₁.sigma := by linarith
  85    exact h_diff this.symm
  86
  87/-- Love equilibrates: after application, the sigma difference decreases. -/
  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