jcost_minimum
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 in Recognition Science
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.
scope and limits
- Does not prove that the minimum is global without further analysis.
- Does not compute the derivative at any point other than 1.
- Does not extend the result to the phi-ladder or to spatial dimensions beyond the base case.
Lean usage
def cert : CalculusCert := { five_theorems := calculusTheoremCount, minimum_at_1 := jcost_minimum, strict_minimum := jcost_strict_min }formal statement (Lean)
32theorem jcost_minimum : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
33
34/-- J is positive off minimum (strict local minimum). -/