The constructed Riemann integral exists as a total, axiom-free CReal function

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

Recorded description

There is a total function CReal.integral taking a function F, endpoints a <= b, and a witness that F is uniformly continuous on [a,b], and returning a CReal -- built as speedup(diagonal(f_lambda), K) with a regularity proof, where f_lambda n := riemannSum F a b (deep F a b u n) is the sequence of Riemann sums at accuracy-driven mesh counts. Admitted by the trusted kernel gate with an empty axiom footprint. This is Spivak Ch.13/14's definite integral, constructed rather than assumed.

Formal statement

def CReal.integral : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal.le x1 x2) -> ((x4 : CReal.UniformlyContinuousOn x0 x1 x2) -> CReal)))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-CReal.integral

Kind: kernel-term
Status: checked

Supports: CReal.integral 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 kernel_declaration_projection -- --require-declaration CReal.integral --require-kind definition 2>/dev/null | grep -cE '^found[[:space:]]creal[[:space:]]definition[[:space:]]CReal\.integral[[:space:]]'

Evidence notes

UPGRADED from an indirect checker to a DIRECT one in the same batch that registered F:creal-e and the Ch.18/22-23 facts (see CLAUDE.md's brief for that batch). CReal.integral is a Declaration::Definition, not a Theorem, and theorem_dependency_inventory (like prelude_theorem_inventory and nat_theorem_inventory) deliberately excludes Definitions from its listing -- 'Definitions, inductives and axioms are excluded' is the tool's own stated contract -- so this fact previously checked CReal.integral's presence INDIRECTLY, via CReal.integral_const's own admission (declare_integral_const builds CReal.integral (fun _ => x0) x1 x2 x3 x4 as a 5-argument const_app, and the kernel can only admit that application by first resolving CReal.integral's own declared arrow type against it). That route worked but named the wrong subject in its own evidence id and forced a reader to know a second theorem's proof to trust this one. kernel_declaration_projection now takes '--require-declaration <name> [--require-kind <kind>]': it searches every constructed prelude's environment for an EXACT display-name match (of the given kind, when specified) and exits non-zero when none is found. Mutation-tested on an isolated /data0 snapshot (scripts/lane-snapshot.sh, never the shared checkout): renaming CReal.integral's display string to "integral_MUTATED" at crates/axeyum-lean-kernel/src/creal.rs:4389 made this exact check return count 0 / exit 1 in the rebuilt binary, while an unrelated control name (CReal.e) in the SAME rebuild still matched and exited 0 -- confirming the check discriminates on CReal.integral's own name, not on the build succeeding globally. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.integral

Kind: exhaustive-enumeration
Status: checked

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

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, exits 0 printing 'ok: creal trusted surface = 0'. That bounds every declaration in the creal environment, including CReal.integral, since a declaration cannot depend on a trusted declaration the environment does not contain. --require-axiom-free <name> errors for a prelude never built by this run. --release is MANDATORY here.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/integral.rs, declare_creal_integral)",
  "source": "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()) -- no in-tree example prints CReal.integral's own type, since every theorem-inventory example filters to Declaration::Theorem and excludes Definitions. The probe was built and run in the session scratchpad and deleted after use; crates/ source was not touched to produce this batch."
}