Jcost_pos_of_ne_one
plain-language theorem explainer
The theorem establishes that J-cost is strictly positive for every positive real ratio r different from 1. Researchers in acoustics, chemistry, and coherence systems cite the result to guarantee positive recognition penalties away from the optimum ratio. The short proof rewrites Jcost via its squared-ratio identity from the Cost module and reduces positivity to the square of a nonzero numerator together with a positive denominator.
Claim. Let $J(r)$ be the J-cost function. For every real number $r > 0$ with $r ≠ 1$, one has $0 < J(r)$.
background
The Local Cache module develops the machine-verified core of the Inevitability of Local Minds paper. It centers on the J-cost function that quantifies recognition cost for a firing-rate ratio r, with the key identity J(x) = (x-1)^2 / (2x) for x ≠ 0 supplied by the upstream Jcost_eq_sq lemma in the Cost module. The module proves local_cache_benefit under assumptions A1-A3 and shows that the optimal partition recurrence forces the golden ratio φ as the self-similar fixed point.
proof idea
The term-mode proof first invokes the upstream lemma Jcost_eq_sq (ne_of_gt hr) to obtain the squared-ratio expression for Jcost r. It then applies div_pos, reduces the numerator via sub_ne_zero.mpr hr_ne together with positivity, and confirms the denominator is positive by the hypothesis 0 < r.
why it matters
The result is invoked by more than forty downstream theorems, among them srCost_pos_off_threshold in speech intelligibility, aestheticCost_pos_off_optimum in cultural aesthetics, above_threshold_positive in the Maillard reaction, oxidative_stress for reactive oxygen species, and resonance_increases_stability in coherence technology. It supplies the basic positivity step that supports the Recognition Composition Law and the forcing chain from J-uniqueness to the eight-tick octave and D = 3. It touches the open question of how J-cost positivity propagates across the phi-ladder in higher-dimensional applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.