CalculusCert
plain-language theorem explainer
The CalculusCert structure packages a certificate that exactly five canonical calculus theorems exist alongside the J-cost function attaining a strict global minimum of zero at unity. A researcher deriving the fundamental theorem of calculus from the recognition cost functional equation would cite this certificate when invoking the five theorems as a complete basis. It is realized as a structure definition whose fields are populated directly by the module's theorem-count lemma and the two J-cost extremum lemmas.
Claim. A certificate asserting that the set of five theorems (first and second fundamental theorems of calculus, mean value theorem, intermediate value theorem, L'Hôpital's rule) has cardinality 5, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module derives the fundamental theorem of calculus from Recognition Science by treating the J-cost integral from 1 to r as the total recognition cost, so that differentiation and integration become inverse operations. The J-cost function is the recognition cost obeying the composition law, with the explicit local form $J(r)=(r-1)^2/(2r)$ near $r=1$ implying a critical point at unity. The upstream inductive type enumerates precisely the five theorems whose cardinality is asserted by the first field of the certificate.
proof idea
The declaration is a structure definition with no proof body. Its three fields are instantiated downstream by the calculusCert definition, which supplies the theorem cardinality via the count lemma, the zero value at unity via the minimum lemma, and the strict inequality via the strict-minimum lemma.
why it matters
This certificate supplies the structural claim that the five theorems match the configuration dimension required for the fundamental theorem of calculus in the Recognition Science setting. It is consumed by the downstream calculusCert definition that packages the result for use in broader derivations. The construction closes the link between the J-cost minimum property and the completeness of the five theorems without introducing additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.