Jcost_pos_away_from_one
J-cost is strictly positive for every positive real ratio r away from 1. Researchers modeling Hebbian plasticity cite the result to ground the claim that only balanced firing rates achieve minimal recognition cost. The argument substitutes the squared-ratio identity for J-cost and verifies positivity of the resulting fraction via div_pos.
claimFor every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$, where $J(r) = (r-1)^2 / (2r)$.
background
The J-cost function quantifies recognition cost of a firing-rate ratio r in the information domain. Upstream, Jcost_eq_sq supplies the identity J(r) = (r-1)^2 / (2r) for r ≠ 0. The Local Cache module derives caching benefits and φ-optimal hierarchies from the Recognition Composition Law, with this lemma supplying the strict positivity needed for sign structure.
proof idea
The proof is a one-line wrapper that invokes Jcost_eq_sq to obtain the squared form, then applies div_pos. It uses sub_ne_zero.mpr on the hypothesis r ≠ 1 to confirm the numerator is nonzero and positivity on both numerator and denominator.
why it matters in Recognition Science
The lemma feeds hebbian_sign_structure, which asserts J(r) = 0 precisely when r = 1. This encodes the mathematical content of Hebb's rule inside the Recognition Science framework and corresponds to T5 J-uniqueness, where the cost minimum occurs at the balanced fixed point. It closes a supporting step for the local-cache theorems without touching open questions.
scope and limits
- Does not claim anything about the case r = 1.
- Does not apply when r is non-positive.
- Does not establish the symmetry J(r) = J(1/r).
- Does not provide bounds on the magnitude of J(r).
- Does not connect directly to the golden ratio or spatial dimensions.
formal statement (Lean)
192theorem Jcost_pos_away_from_one (r : ℝ) (hr : 0 < r) (hr_ne : r ≠ 1) :
193 0 < Jcost r := by
proof body
Term-mode proof.
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. -/