hebbian_sign_structure
plain-language theorem explainer
The declaration proves that for positive real r the J-cost vanishes precisely when r equals 1 and is strictly positive otherwise. Neural network theorists and researchers studying Hebbian plasticity would cite this to equate J-cost descent with the emergence of correlated firing patterns. The proof is a short tactic script that reduces the zero condition to the squared expression of J-cost and invokes a separate positivity result for the nonzero case.
Claim. For all real numbers $r > 0$, the J-cost satisfies $J(r) = 0$ if and only if $r = 1$, and $J(r) > 0$ whenever $r ≠ 1$.
background
The J-cost function is defined as $J(r) = (r + r^{-1})/2 - 1$ for positive r, which the upstream lemma Jcost_eq_sq rewrites as the squared ratio $(r-1)^2/(2r)$. This module develops local cache theorems in the context of the Inevitability of Local Minds paper, showing how caching reduces access costs and how optimal partitions force the golden ratio. Upstream results include the algebraic identity Jcost_eq_sq that rewrites J-cost as a square and the unit value Jcost_unit0 showing J(1) = 0.
proof idea
The proof splits into two parts via constructor. The first part shows the equivalence by substituting the squared expression from Jcost_eq_sq and using nlinarith to conclude that the numerator vanishes only at r=1. The reverse direction substitutes r=1 and applies Jcost_unit0. The second conjunct invokes the lemma Jcost_pos_away_from_one directly.
why it matters
This result sits inside the Local Cache module and supports the link between J-cost minimization and Hebbian covariance structure as described in the module documentation. It fills in the claim that J-cost descent corresponds to Hebbian sign structure, connecting to the broader Recognition Science framework where J-uniqueness (T5) underpins cost functions. No downstream uses are recorded yet, leaving open how this integrates with the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.