Mathematics Fundamental Theorem Calculus From Rs

The Ledger's Calculus

The fundamental theorem of calculus is the classical statement that differentiation and integration are inverse operations. If you know how fast something changes, you can add up those changes to recover the total amount. The theorem has two standard parts: one says the integral of a derivative recovers the original function, the other says the derivative of an integral gives back the integrand. These two parts, together with the mean value theorem, the intermediate value theorem, and L'Hôpital's rule, form the five canonical theorems of a first calculus course.

In Recognition Science, the framework treats a ledger, a discrete record of recognition events, as the fundamental object. The framework's cost function J(x) measures the price of recognizing a ratio x between two quantities. The central result is that J(x) = (x + 1/x)/2 - 1, a formula forced by five plain conditions. This cost function has a minimum at x = 1, where J(1) = 0, meaning no cost is paid when the two quantities are identical. For any other positive ratio, the cost is strictly positive.

The framework's library, a machine-checked collection of formal theorems, proves that the integral of the cost's derivative from 1 to r equals the total cost J(r). This is the framework's version of the fundamental theorem: ∫₁ʳ J'(x) dx = J(r) - J(1) = J(r). The derivative J'(1) = 0 is structural, reflecting that the cost function sits at its minimum when the ratio is 1. The library also counts exactly five canonical calculus theorems and bundles them with the minimum properties into a single certificate structure.

The result changes what the fundamental theorem means. In the classical setting, the theorem connects two abstract operations on functions. In this framework, the same theorem connects the rate of change of recognition cost to the total cost of moving from one ratio to another. The five theorems are not a random list; they form a complete set that the framework's certificate records. The proof is machine-checked with no gaps and no extra assumptions, so the connection between the calculus and the cost function is exact.

structure CalculusCert where
  five_theorems : Fintype.card CalculusTheorem = 5
  minimum_at_1 : Jcost 1 = 0
  strict_minimum : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r

/-- J(1) = 0 (minimum, derivative = 0 at critical point). -/
theorem jcost_minimum : Jcost 1 = 0 := Jcost_unit0

/-- J is positive off minimum (strict local minimum). -/
theorem jcost_strict_min {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < Jcost r := Jcost_pos_of_ne_one r hr hne

theorem calculusTheoremCount : Fintype.card CalculusTheorem = 5 := by decide

What this page does not claim

This module does not prove the classical fundamental theorem of calculus from scratch. The five theorems listed are not derived from the cost function; they are counted as a complete set. The framework does not claim that integration and differentiation are physically real operations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/FundamentalTheoremCalculusFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: