jcost_strict_min
plain-language theorem explainer
The declaration establishes that the J-cost function is strictly positive for any positive real r not equal to 1. Researchers deriving the fundamental theorem of calculus from Recognition Science principles would cite it to confirm the strict local minimum property of the cost function at the identity scaling. The proof is a direct one-line application of the upstream positivity lemma for J-cost away from unity.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$, where $J$ is the recognition cost function with $J(1) = 0$.
background
In Recognition Science the J-cost function quantifies the recognition cost of a scaling factor r, satisfying J(1) = 0 and achieving its global minimum there. The module FundamentalTheoremCalculusFromRS derives the fundamental theorem of calculus from RS by showing that the integral of J' from 1 to r recovers J(r) exactly, with five canonical calculus theorems corresponding to configDim D = 5. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1; its proof rewrites Jcost via the square identity Jcost_eq_sq and invokes positivity of squares for the numerator (x-1)^2 together with positivity of the denominator.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one (from the Cost module) to the supplied hypotheses 0 < r and r ≠ 1.
why it matters
The result is bundled into the calculusCert definition alongside the minimum_at_1 property and the count of five theorems, completing the RS-native statement of the fundamental theorem of calculus. It directly supports the module claim that J(r) = (r-1)^2/(2r) near r=1 has derivative zero at the minimum, aligning with the framework's T5 J-uniqueness and the strict positivity off the fixed point. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.