jcost_minimum
plain-language theorem explainer
J(1) equals zero, establishing the minimum of the recognition cost function at the unit scale. Researchers deriving the fundamental theorem of calculus within Recognition Science would cite this result to anchor the integration properties of J-cost. The proof is a direct one-line application of the unit lemma from the Cost module.
Claim. $J(1) = 0$ where $J$ denotes the recognition cost function.
background
In Recognition Science the J-cost function takes the explicit form $J(x) = (x-1)^2/(2x)$. This squared-ratio expression encodes the defect cost between a scale $x$ and the unit scale. The module FundamentalTheoremCalculusFromRS derives the fundamental theorem of calculus from this cost: the integral of the derivative from 1 to $r$ recovers $J(r)$ precisely because $J(1)$ vanishes.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0, which itself reduces the definition of Jcost by simplification to obtain the value zero at argument 1.
why it matters
This theorem supplies the minimum_at_1 field inside the calculusCert definition that certifies the five canonical calculus theorems (FTC-1, FTC-2, mean-value, intermediate-value, L'Hôpital) required for configDim D = 5. It directly confirms the critical-point condition J'(1) = 0 that lets differentiation and integration invert in the RS setting. The result sits at the base of the chain that converts the J-cost minimum into the structural FTC statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.