Jcost_pos_away_from_one

formal source

 189
 190    This is the mathematical content of Hebb's rule: correlated firing (r ≈ 1)
 191    has minimal cost; uncorrelated firing (r ≠ 1) has positive cost. -/
 192theorem Jcost_pos_away_from_one (r : ℝ) (hr : 0 < r) (hr_ne : r ≠ 1) :
 193    0 < Jcost r := by
 194  have h := Jcost_eq_sq (ne_of_gt hr)
 195  rw [h]
 196  apply div_pos
 197  · have : r - 1 ≠ 0 := sub_ne_zero.mpr hr_ne
 198    positivity
 199  · positivity
 200
 201/-- **THEOREM (Hebbian Sign Structure)**:
 202
 203  J(r) = 0 iff r = 1 (balanced firing), and J(r) > 0 for r ≠ 1.
 204  Therefore the unique J-cost minimum on the neural graph is at
 205  balanced (correlated) firing rates.
 206
 207  The Hebbian covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing
 208  is correlated (r ≈ 1, J ≈ 0) and negative when uncorrelated (r ≠ 1, J > 0).
 209  Thus J-cost descent ↔ Hebbian sign structure. -/
 210theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
 211    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by
 212  constructor
 213  · constructor
 214    · intro h
 215      -- J(r) = (r-1)²/(2r) = 0 iff r = 1
 216      have heq := Jcost_eq_sq (ne_of_gt hr)
 217      rw [heq] at h
 218      have hden : (2 * r) ≠ 0 := by positivity
 219      have h0 : (r - 1) ^ 2 = 0 := by
 220        by_contra hne
 221        have : 0 < (r - 1) ^ 2 / (2 * r) := div_pos (by positivity) (by positivity)
 222        linarith