calculusTheoremCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the individual statements of the five theorems.
- Does not relate the count to the explicit J-cost formula near unity.
- Does not prove that these are the only possible calculus theorems in the framework.
- Does not address higher-dimensional or generalized versions.
Lean usage
def cert : CalculusCert := { five_theorems := calculusTheoremCount, minimum_at_1 := jcost_minimum, strict_minimum := jcost_strict_min }formal statement (Lean)
29theorem calculusTheoremCount : Fintype.card CalculusTheorem = 5 := by decide
proof body
Term-mode proof.
30
31/-- J(1) = 0 (minimum, derivative = 0 at critical point). -/