CalculusTheorem
plain-language theorem explainer
Recognition Science obtains five calculus theorems from the J-cost: the first and second fundamental theorems of calculus, the mean value theorem, the intermediate value theorem, and L'Hôpital's rule. Analysts deriving differentiation and integration as inverses under the Recognition Composition Law cite this list when fixing the configuration dimension at five. The inductive definition lists the five cases and equips the type with decidable equality and finite cardinality.
Claim. Inductive type enumerating the five calculus theorems: first fundamental theorem of calculus, second fundamental theorem of calculus, mean value theorem, intermediate value theorem, L'Hôpital's rule.
background
The J-cost function quantifies recognition cost between scales, satisfying the Recognition Composition Law. Its integral from 1 to r recovers the total cost, with the explicit local form J(r)=(r-1)^2/(2r) near r=1 yielding derivative zero at the minimum. The module states that differentiation and integration are inverses under this cost, and that the five theorems equal the configuration dimension D=5.
proof idea
The declaration is the inductive definition itself, introducing five distinct constructors for the listed theorems and deriving the instances DecidableEq, Repr, BEq, and Fintype.
why it matters
This supplies the finite set whose cardinality is certified to be five in the downstream CalculusCert structure, which also records the J-cost minimum at 1. It realizes the step where the five analytic results fix the configuration dimension in the Recognition Science framework, closing the analytic foundation for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.