jcost_off_minimum
plain-language theorem explainer
J-cost is strictly positive for any positive real ratio r different from one. Workers on the variational formulation of Recognition Science cite this to confirm that the equilibrium at r equals one is a strict minimum of the recognition functional. The proof is a direct one-line application of the core positivity lemma for the squared deviation expression of J-cost.
Claim. If $r > 0$ and $r ≠ 1$, then $0 < Jcost(r)$.
background
The J-cost functional quantifies deviation from equilibrium in the Recognition Science calculus of variations. Upstream lemmas establish that Jcost r rewrites as a quotient whose numerator is a square and whose denominator is positive for r > 0, yielding strict positivity away from r = 1. The module develops the Euler-Lagrange equation for the J-cost integral, with the equilibrium condition r = 1 yielding J = 0 as the global minimum.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (and its duplicates in JcostCore and LocalCache). The lemma substitutes the squared form Jcost_eq_sq and invokes div_pos together with sq_pos_of_ne_zero on the factor (r - 1).
why it matters
It supplies the off_minimum_positive field inside the VariationsCert definition, which certifies the five canonical variational problems and the strict minimum at r = 1. This step closes the local analysis of the recognition functional required for the RS forcing chain, linking the J-uniqueness property to the variational foundation that supports the phi-ladder and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.