pi <= 4, from the same geometric domination the construction already needed

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

Recorded description

le pi four, four := mul two two. Every partial sum of the series is at most two: termwise piHalfTerm k <= (1/2)^k (CReal.piHalfTermLePowHalf, a short induction on the definitional ratio (k+1)/(2k+3) <= 1/2), summed by CReal.sumRange_le, then CReal.sumRange_pow_half_closed_form reads the geometric partial sum as 2*(1 - (1/2)^n) <= 2. That holds at EVERY index including 0, so CReal.converges_upper_bound applies with no shift, giving CReal.piHalfLeTwo : le piHalf two; pi IS mul two piHalf, so one CReal.mul_le_mul_of_nonneg_left finishes. Looser than the classical 3.15 for the same structural reason CReal.e_le_four is looser than e <= 3: sharpening needs the tail dominated from index 4 rather than from index 0, a re-indexed domination rather than a corollary of what is here.

Formal statement

theorem CReal.piLeFour : CReal.le CReal.pi (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.

4 direct dependencies 0 direct dependents

Evidence

kernel-CReal.piLeFour

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits this theorem 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. ONE NAME PER INVOCATION: this tool silently discards every name argument after the first. --release is MANDATORY.

footprint-CReal.piLeFour

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds this declaration

Checker command

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

Evidence notes

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 this one. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack. Independently re-measured this session by kernel_declaration_projection, whose footprint-size column reads 0 for all fourteen CReal.pi* declarations.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/pi.rs, declare_pi_family)",
  "source": "canonical type and axiom-footprint size read from kernel_declaration_projection --release on this tree (the creal-prelude row), not from source text or a doc comment."
}