e <= 4, one uniform bound holding at every index

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

Recorded description

le e four, four := mul two two. From the SAME domination expTerm n <= expDominant n (expDominant n := 2*(1/2)^n) the file builds for the Cauchy argument, summed via sumRange_le and the closed form sumRange_pow_half_closed_form: sum expDominant n = 2*sum(1/2)^i = 2*(2*(1-(1/2)^n)) <= 4. UNLIKE two_le_e, no shift is needed -- this bound holds at every n including n = 0. It is looser than the classical e <= 3 by exactly the factor of 2 the domination is uniform (rather than index-2-split) about; see F:creal-e-le-three for the sharpened bound and why it costs a genuine case split.

Formal statement

theorem CReal.e_le_four : CReal.le CReal.e (CReal.mul (CReal.ofRat (Rat.normalize (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ AxNat.zero) (AxNat.le.refl (AxNat.succ AxNat.zero)))) (CReal.ofRat (Rat.normalize (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ AxNat.zero) (AxNat.le.refl (AxNat.succ AxNat.zero)))))

Dependencies

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

30 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.e_le_four

Kind: kernel-term
Status: checked

Supports: CReal.e_le_four 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 -- e_le_four 2>/dev/null | grep -cE '^CReal\.e_le_four[[:space:]]'

Evidence notes

build_creal_prelude admits CReal.e_le_four through the trusted Kernel::add_declaration gate. theorem_dependency_inventory exits non-zero for a named filter matching nothing; grep -c (never -q) both consumes the pipe and asserts the exact tab-anchored line is present. Verified on this tree: the command currently prints exactly one matching line for CReal.e_le_four. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.e_le_four

Kind: exhaustive-enumeration
Status: checked

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

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_le_four)",
  "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 this theorem's own type directly. 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."
}