calculusTheoremCount
plain-language theorem explainer
Recognition Science identifies five canonical calculus theorems whose number equals the configuration dimension. A researcher verifying the derivation of calculus from the J-cost equation would cite this cardinality result. The proof is a decision procedure that directly counts the constructors of the inductive enumeration of those theorems.
Claim. The set of canonical calculus theorems has cardinality five, consisting of the fundamental theorem of calculus in two parts, the mean value theorem, the intermediate value theorem, and L'Hôpital's rule: $|C| = 5$ where $C$ denotes that set.
background
The module develops the fundamental theorem of calculus within Recognition Science by identifying differentiation and integration as inverse operations through the J-cost. The integral from 1 to r of J'(x) dx equals J(r), since J(1) equals zero at the minimum. Five theorems are singled out as canonical: FTC-1, FTC-2, the mean value theorem, the intermediate value theorem, and L'Hôpital's rule. Their count is asserted to equal the configuration dimension D equal to 5. The upstream inductive definition enumerates precisely these five cases.
proof idea
The proof applies the decide tactic, which computes the finite cardinality by inspecting the five constructors of the inductive type that lists the theorems.
why it matters
The result populates the five_theorems component of the calculusCert certificate that also records the J-cost minimum at unity. It confirms the module's claim that the five theorems correspond to configDim D = 5 in the Recognition Science framework. No open questions are attached to this enumeration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.