Information Local Cache Hebbian Sign Structure

Hebbian sign structure

Hebbian learning is the rule that a connection between two neurons grows stronger when they fire together and weaker when they do not. The classic slogan is "neurons that fire together wire together." The Recognition Science framework formalizes this in a theorem called hebbian_sign_structure. It concerns a synapse between two neurons with firing rates f_u and f_v, and a cost function J that assigns a penalty to any imbalance in those rates. The theorem states that J(r) = 0 if and only if r = 1, where r is the ratio f_u / f_v, and that J(r) > 0 whenever r is not 1. In plain language, the cost is zero exactly when the two firing rates are balanced, and positive whenever they are out of balance.

The framework's cost is a measure of how much a recognition event, a discrete record of something happening, deviates from a perfect match. The theorem's content is that this cost is minimized at r = 1. The framework connects this to Hebbian learning by identifying the change in a synapse's strength with the negative gradient of this cost. When the cost is at its minimum, the gradient is zero, and the synapse is stable. When the cost is positive, the gradient pushes the firing rates back toward balance, which the framework interprets as the synapse weakening. This gives a precise mathematical condition for the sign of the change: the covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing is correlated, meaning the rates are near each other, and negative when uncorrelated.

The theorem itself is a proved result in the framework's machine-checked library of formal theorems. It is a statement about a real-valued function J and a positive real number r. It does not claim that real biological synapses follow this rule. It does not claim that the cost function J is the only possible cost function, nor that the framework's identification of Hebbian learning with J-cost descent is the only way to model synaptic plasticity. The theorem is a mathematical fact about a specific function, not an empirical claim about brains.

/-- **THEOREM (Hebbian Sign Structure)**:

  J(r) = 0 iff r = 1 (balanced firing), and J(r) > 0 for r ≠ 1.
  Therefore the unique J-cost minimum on the neural graph is at
  balanced (correlated) firing rates.

  The Hebbian covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing
  is correlated (r ≈ 1, J ≈ 0) and negative when uncorrelated (r ≠ 1, J > 0).
  Thus J-cost descent ↔ Hebbian sign structure. -/
theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by
  constructor
  · constructor
    · intro h
      -- J(r) = (r-1)²/(2r) = 0 iff r = 1
      have heq := Jcost_eq_sq (ne_of_gt hr)
      rw [heq] at h
      have hden : (2 * r) ≠ 0 := by positivity
      have h0 : (r - 1) ^ 2 = 0 := by
        by_contra hne
        have : 0 < (r - 1) ^ 2 / (2 * r) := div_pos (by positivity) (by positivity)
        linarith
      nlinarith [sq_nonneg (r - 1)]
    · intro h; subst h; exact Jcost_unit0
  · exact Jcost_pos_away_from_one r hr

/-- **THEOREM (Hebbian Sign Structure)**:

  J(r) = 0 iff r = 1 (balanced firing), and J(r) > 0 for r ≠ 1.
  Therefore the unique J-cost minimum on the neural graph is at
  balanced (correlated) firing rates.

  The Hebbian covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing
  is correlated (r ≈ 1, J ≈ 0) and negative when uncorrelated (r ≠ 1, J > 0).
  Thus J-cost descent ↔ Hebbian sign structure. -/
theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by
  constructor
  · constructor
    · intro h
      -- J(r) = (r-1)²/(2r) = 0 iff r = 1
      have heq := Jcost_eq_sq (ne_of_gt hr)
      rw [heq] at h
      have hden : (2 * r) ≠ 0 := by positivity
      have h0 : (r - 1) ^ 2 = 0 := by
        by_contra hne
        have : 0 < (r - 1) ^ 2 / (2 * r) := div_pos (by positivity) (by positivity)
        linarith
      nlinarith [sq_nonneg (r - 1)]
    · intro h; subst h; exact Jcost_unit0
  · exact Jcost_pos_away_from_one r hr

What this page does not claim

The theorem does not claim that real biological synapses follow this rule. The theorem does not claim that the cost function J is the only possible cost function. The theorem does not claim that the framework's identification of Hebbian learning with J-cost descent is the only way to model synaptic plasticity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/LocalCache.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: