Riemann sums over a fixed interval form a Cauchy sequence as the mesh refines

Identifier: F:creal-riemannsum-cauchy
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For a function F on [a,b], a witness that F is uniformly continuous on [a,b], and any accuracy index e: the finite left-endpoint Riemann sum riemannSum F a b m, taken at two sufficiently fine (Nat.succ-shaped) mesh counts built from e, agree to within the canonical CReal.Within bound at index e -- i.e. riemannSum is a Cauchy sequence of CReal values as the subinterval count grows, at the SAME shared accuracy index used to compare them (not yet the canonical per-own-index Cauchy shape; see CReal.sharedIndexToCanonical for that bridge). This is Spivak Ch.13's convergence-of-Riemann-sums estimate, and it is the theorem CReal.integral itself is built from.

Formal statement

theorem CReal.riemannSum_cauchy : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : CReal.le x1 x2) -> ((x7 : CReal.UniformlyContinuousOn x0 x1 x2) -> ((x8 : AxNat) -> CReal.Within (CReal.seq (CReal.add (CReal.riemannSum x0 x1 x2 (AxNat.add (AxNat.add (AxNat.mul (AxNat.succ (CReal.bound (CReal.add x2 (CReal.neg x1)))) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x7 x3)) (CReal.bound (CReal.add x2 (CReal.neg x1)))) x5)) (CReal.neg (CReal.riemannSum x0 x1 x2 (AxNat.add (AxNat.add (AxNat.mul (AxNat.succ (CReal.bound (CReal.add x2 (CReal.neg x1)))) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x7 x3)) (CReal.bound (CReal.add x2 (CReal.neg x1)))) x5)))) x8) (Rat.add (CReal.seq (CReal.mul (CReal.ofNat (AxNat.succ (AxNat.add (AxNat.add (AxNat.mul (AxNat.succ (CReal.bound (CReal.add x2 (CReal.neg x1)))) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x7 x3)) (CReal.bound (CReal.add x2 (CReal.neg x1)))) x5))) (CReal.mul (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x3)) (CReal.mul (CReal.add x2 (CReal.neg x1)) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.add (AxNat.add (AxNat.mul (AxNat.succ (CReal.bound (CReal.add x2 (CReal.neg x1)))) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x7 x3)) (CReal.bound (CReal.add x2 (CReal.neg x1)))) x5)))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ AxNat.zero)) x8)))))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

18 direct dependencies 6 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.riemannSum_cauchy

Kind: kernel-term
Status: checked

Supports: CReal.riemannSum_cauchy is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- riemannSum_cauchy 2>/dev/null | grep -cE '^CReal\.riemannSum_cauchy[[:space:]]'

Evidence notes

build_creal_prelude admits CReal.riemannSum_cauchy through the trusted Kernel::add_declaration gate. theorem_dependency_inventory exits non-zero for a named filter matching nothing; grep -c (never -q) both avoids a SIGPIPE-under-pipefail false negative and independently asserts the exact tab-anchored line is present. Mutation-tested on an isolated /data0 snapshot (scripts/lane-snapshot.sh, never the shared checkout): renaming the display string from "riemannSum_cauchy" to "riemannSum_cauchy_MUTATED" at crates/axeyum-lean-kernel/src/creal.rs:4379 makes this exact grep return 0 matches (exit 1), while an unrelated control name (CReal.integral_const) in the SAME rebuilt binary still matched -- confirming the pattern discriminates on the intended theorem and not on the build succeeding in general. --release is MANDATORY: this tool also builds creal/complex/cpoint, which recurse deep enough in a debug build to overflow the default thread stack.

footprint-CReal.riemannSum_cauchy

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.riemannSum_cauchy

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free creal

Evidence notes

Re-measured on this tree: creal: axiom=0 opaque=0 quotient=0 total_trusted=0, and the tool prints 'ok: creal trusted surface = 0' and exits 0. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY here per CLAUDE.md: --include-constructed builds creal/complex/cpoint and this example has no deep-stack worker, so a debug build SIGABRTs at 134 instead of reporting the honest measurement.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/integral.rs, declare_riemann_sum_cauchy)",
  "source": "theorem name and canonical type read via a standalone probe binary depending on axeyum-lean-kernel by path, calling only its public Kernel API (environment(), display_name(), render_lean(), axiom_footprint(), theorem_dependencies()) -- no in-tree example prints CReal.riemannSum_cauchy's own type. Direct dependency edges cross-checked against theorem_dependency_inventory's own output on the same tree. The probe was built and run in the session scratchpad and deleted after use; crates/ source was not touched to produce this batch."
}