Jcost_strictMono_on_Ici_one
plain-language theorem explainer
J-cost is strictly increasing on [1, ∞). Researchers proving cache hierarchy from cost minimization on graphs cite it to guarantee that larger scale separation raises total cost. The proof rewrites both sides via the squared-ratio identity, clears the positive denominators with div_lt_div_iff₀, and finishes with nlinarith on four non-negative squares.
Claim. For all real numbers $a,b$ with $1≤a<b$, $J(a)<J(b)$ where $J(x)=(x-1)^2/(2x)$.
background
The LocalCacheForcing module shows that J-cost minimization on connected graphs forces hierarchical local caching and thereby closes Gap G1 in the brain holography argument. J-cost is the Recognition Science cost function $J(x)=(x+x^{-1})/2-1$, equivalently written $(x-1)^2/(2x)$ for $x≠0$. The present theorem supplies the strict increase needed for the monotone and phi-power corollaries that follow in the same file.
proof idea
Positivity of $a$ and $b$ is obtained by linarith from the hypotheses. Two applications of the upstream lemma Jcost_eq_sq convert both sides to squared ratios. The comparison is rewritten with div_lt_div_iff₀ on the positive terms $2a$ and $2b$, after which nlinarith dispatches the resulting inequality by non-negativity of $(a-1)^2$, $(b-1)^2$, $(ab-1)^2$ and $(a-b)^2$.
why it matters
It is invoked directly by Jcost_mono_on_Ici_one and Jcost_phi_pow_strictMono, which in turn feed collocation_minimizes_cost and caching_is_forced. The result therefore forms part of the local-cache-forcing certificate that closes Gap G1. In the broader Recognition framework it underwrites the phi-ladder cost growth that forces the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.