The ordered-pair Cauchy bound for the general-ratio geometric series

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

Recorded description

CReal.geomCauchyOfLtOrdered is the a<=b-ordered leaf lemma geomCauchyOfLt's case split consumes: it bounds the partial-sum gap between indices a<=b of sumRange (x^n) via the reciprocal-of-(1-x) bound witness -- the general-ratio analogue of geomCauchyOrderedHalf (the fixed-ratio-1/2 leaf).

Formal statement

theorem CReal.geomCauchyOfLtOrdered : ((x0 : CReal) -> ((x1 : CReal.le CReal.zero x0) -> ((x2 : AxNat) -> ((x3 : CReal.PosBound (CReal.add CReal.one (CReal.neg x0)) x2) -> ((x4 : AxNat) -> ((x5 : ((x5 : AxNat) -> CReal.le (CReal.mul (CReal.inv (CReal.add CReal.one (CReal.neg x0)) x2 x3) (CReal.pow x0 x5)) (CReal.ofRat (Rat.natDivSucc x4 x5)))) -> ((x6 : AxNat) -> ((x7 : AxNat) -> ((x8 : AxNat.le x6 x7) -> CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x9 : AxNat) => CReal.pow x0 x9) x7) x7) (CReal.seq (CReal.sumRange (fun (x9 : AxNat) => CReal.pow x0 x9) x6) x6)) (Rat.add (Rat.natDivSucc (AxNat.add (AxNat.add x4 (AxNat.succ AxNat.zero)) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))))))) x7) (Rat.natDivSucc (AxNat.add (AxNat.add x4 (AxNat.succ AxNat.zero)) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))))))) x6)))))))))))

Dependencies

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

13 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.geomCauchyOfLtOrdered

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits CReal.geomCauchyOfLtOrdered through the trusted Kernel::add_declaration gate, which re-checks the proof term against the stated type. theorem_dependency_inventory exits non-zero for a named filter matching nothing (a deleted theorem cannot read as a re-derived one), and grep -c (never -q) both consumes the pipe and asserts the exact tab-anchored line is present. Verified on this tree: the command prints exactly one matching line for CReal.geomCauchyOfLtOrdered. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.geomCauchyOfLtOrdered

Kind: exhaustive-enumeration
Status: checked

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

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.geomCauchyOfLtOrdered, 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 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/geometric.rs, declare_geom_cauchy_of_lt_ordered)",
  "source": "canonical type read via kernel_declaration_projection's own UNFILTERED emit mode (cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection, no --require-declaration flag), which prints, per constructed prelude, one TSV row per declaration whose last field is kernel.render_lean(declaration.ty()) -- the same Kernel::render_lean canonical form nat_theorem_inventory prints, just not filtered to Declaration::Theorem. That output was piped to a scratchpad file and the exact row for this declaration's own prelude label was extracted and injected here programmatically (a Python script reading the TSV, never hand-transcribed); direct dependency edges (where applicable) were cross-read from the same run's direct_theorems column and independently confirmed against theorem_dependency_inventory's own output on this tree. No new probe binary was written for this batch, since the in-tree tool already emits the canonical type; crates/ source was not touched to produce this batch."
}