Jcost_pos_away_from_one
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.