Euler's number e is constructed as a total, axiom-free CReal value

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

Recorded description

Euler's number is built as CReal.mk (speedup (diagonal expSeriesPartial) K) (...) -- via CReal.mk on an EXPLICIT, concrete regular sequence, never an Exists-elimination into data. expSeriesPartial n := sumRange expTerm n is the partial sum of 1/k! for k < n. The concrete Cauchy witness K for the dominating geometric series (sumRange expDominant, expDominant n := 2*(1/2)^n) is built by hand through CReal.mul's own index-shift bookkeeping (exp_dominant_cauchy_body_concrete) rather than reused from the existential form CReal.expDominantCauchy, precisely because an Exists-eliminated witness cannot be extracted as DATA for CReal.mk to consume -- Exists.rec targets only Prop. Admitted by the trusted kernel gate with an empty axiom footprint. This is Spivak Ch.18's e.

Formal statement

def CReal.e : 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.e

Kind: kernel-term
Status: checked

Supports: CReal.e is admitted by the trusted kernel gate as a definition with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration CReal.e --require-kind definition 2>/dev/null | grep -cE '^found[[:space:]]creal[[:space:]]definition[[:space:]]CReal\.e[[:space:]]'

Evidence notes

DIRECT presence check, built this session (Task 1 of this batch): no in-tree example previously inventoried Declaration::Definition by name with fail-on-absence semantics (theorem_dependency_inventory / nat_theorem_inventory / prelude_theorem_inventory all filter to Declaration::Theorem and explicitly exclude Definitions -- 'Definitions, inductives and axioms are excluded' is theorem_dependency_inventory's own stated contract). Added '--require-declaration <name> [--require-kind <kind>]' to kernel_declaration_projection: it searches every constructed prelude's environment for an EXACT display-name match and exits non-zero when none is found, or when --require-kind is given and no match has that kind. 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 (run against CReal.integral) 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 the intended declaration'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.e

Kind: exhaustive-enumeration
Status: checked

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

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. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY here.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/exponential.rs, declare_e)",
  "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 theorem-inventory example prints a Definition's own type, since every such 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."
}