Jcost_min_at_one
plain-language theorem explainer
The J-cost reaches its global minimum of zero at unit ratio. Researchers deriving phi-optimal cache hierarchies or the inevitability of local minds cite this result to anchor the zero-cost reference for balanced firing rates. The proof is a direct one-line application of the unit lemma for the J-cost definition.
Claim. $J(1) = 0$, where $J(r) := (r-1)^2/(2r)$ for $r > 0$ is the J-cost of a positive ratio.
background
The J-cost is defined by $J(r) = (r-1)^2/(2r)$ and measures the cost of a recognition event induced by a multiplicative recognizer on positive ratios. This module develops the local cache theorem as the machine-verified core of the inevitability of local minds paper, with main results including that caching strictly reduces total access cost and that optimal partition recurrences force the golden ratio. The declaration relies on the upstream Jcost_unit0 lemma, which states the same equality by direct simplification of the J-cost expression.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This theorem supplies the zero-cost reference point for the local cache hierarchy, which downstream localCacheStatus uses to derive the working memory capacity prediction phi^3 approximately 4.236. It fills the balanced firing rate minimum in the phi-optimal hierarchy of the inevitability of local minds paper and anchors the cost function at the fixed point of the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.