minimum_at_one
plain-language theorem explainer
The J-cost function attains its global minimum of zero at argument one over the positive reals. Modelers in hydrodynamics, medicine, or cognitive science cite the result to justify deviation penalties in each domain. The argument introduces the variable, rewrites the unit case, splits on equality to one, and invokes the strict positivity lemma for the remaining case.
Claim. For every real number $r$ with $0 < r$, the J-cost satisfies $J(1) = 0$ and $J(1) < J(r)$ whenever $r > 0$ and $r ≠ 1$, where $J(r) = (r-1)^2/(2r)$.
background
The J-cost is the squared-ratio function $J(r) = (r-1)^2/(2r)$ for $r > 0$. Direct substitution yields $J(1) = 0$, while the core positivity lemma shows $J(r) > 0$ for all other positive $r$. This module treats the same inequality as the source of non-equilibrium cost in every Recognition Science domain.
proof idea
The proof introduces $r$ and the hypothesis $0 < r$. It rewrites the left-hand side with the unit lemma Jcost_unit0. Case analysis on equality to one reduces the equal case to the same unit value and the unequal case to the strict inequality supplied by Jcost_pos_of_ne_one, which immediately gives the required comparison.
why it matters
The theorem supplies the minimum property required by the downstream certificate jPositivityUniversalityCert, which assembles the domain-specific costs for turbulence, disease, off-target CRISPR effects, and market gaps. It realizes the universal lemma of module C16, confirming that a single positivity source governs deviation costs across all listed domains and aligns with the J-uniqueness fixed point of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.