jcost_variational_minimum
plain-language theorem explainer
The J-cost functional reaches its global minimum of zero exactly when the recognition ratio equals one. Researchers deriving variational principles from Recognition Science cite this to anchor the equilibrium condition of the recognition functional. The proof is a direct term-mode application of the unit lemma for J-cost.
Claim. $J(1) = 0$, where $J(r) = (r-1)^2/(2r)$ is the J-cost function on positive ratios.
background
In this module the recognition functional is the integral of J-cost. The J-cost is given explicitly by $J(r) = (r-1)^2/(2r)$, which is nonnegative and vanishes only at $r=1$. The local setting is the calculus of variations applied to five canonical problems (brachistochrone, geodesic, minimal surface, Fermat, and J-cost minimisation), whose common equilibrium is $r=1$ and $J=0$ (MODULE_DOC).
proof idea
The proof is a one-line term-mode wrapper that applies the lemma Jcost_unit0, which itself reduces to simp on the definition $J(r) = (r-1)^2/(2r)$.
why it matters
This theorem supplies the minimum_at_1 field inside the VariationsCert definition, which certifies that the five variational problems share the equilibrium property at $r=1$. It closes the equilibrium step for the J-cost functional in the RS calculus of variations, consistent with the J-uniqueness property of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.