synapse_cost

formal source

 180/-! ## §4  Hebbian Learning = J-Cost Gradient (Theorem 7.1, rigorous) -/
 181
 182/-- J-cost of a firing-rate ratio. -/
 183noncomputable def synapse_cost (f_u f_v : ℝ) : ℝ :=
 184  Jcost (f_u / f_v)
 185
 186/-- **KEY LEMMA**: J-cost is strictly increasing on (1, ∞).
 187    For r > 1, J(r) > J(1) = 0. Combined with J(r) = J(1/r),
 188    this means any deviation from r = 1 increases cost.
 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