[generated] kernel theorem CReal.converges_of_scaled_cauchy (creal prelude, axiom-free, prose not curated)

Identifier: F:creal-converges-of-scaled-cauchy
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

MECHANICALLY GENERATED, UNREVIEWED PROSE -- this sentence deliberately makes NO mathematical characterisation of the theorem. What is asserted, and all that is asserted, is this: the kernel declaration `CReal.converges_of_scaled_cauchy` is a `Declaration::Theorem` admitted into the environment by `build_creal_prelude` through the trusted `Kernel::add_declaration` gate, which re-derives its type from its proof term; its type is recorded verbatim in `formal.statement`; and its axiom footprint, as computed by `Kernel::axiom_footprint`, is empty. The authoritative content of this fact is `formal.statement`. A human-readable characterisation of what CReal.converges_of_scaled_cauchy SAYS has not been supplied, because a generator cannot supply one honestly -- see `notes`.

Formal statement

theorem CReal.converges_of_scaled_cauchy : ((x0 : ((x0 : AxNat) -> CReal)) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> ((x3 : AxNat) -> CReal.Within (Rat.sub (CReal.seq (x0 x2) x2) (CReal.seq (x0 x3) x3)) (Rat.add (Rat.natDivSucc x1 x2) (Rat.natDivSucc x1 x3))))) -> CReal.Converges x0 (CReal.mk (CReal.speedup (fun (x3 : AxNat) => CReal.seq (x0 x3) x3) x1) (CReal.regular_of_kregular (fun (x3 : AxNat) => CReal.seq (x0 x3) x3) x1 (fun (x3 : AxNat) => fun (x4 : AxNat) => And.intro (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc (AxNat.succ x1) x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) (Rat.le (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc (AxNat.succ x1) x4))) (Rat.le_trans (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc (AxNat.succ x1) x4))) (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.neg_le_neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4)) (Rat.add (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc (AxNat.succ x1) x4)) (Rat.add_le_add (Rat.natDivSucc x1 x3) (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc x1 x4) (Rat.natDivSucc (AxNat.succ x1) x4) (Rat.natDivSucc_le_add_left x1 (AxNat.succ AxNat.zero) x3) (Rat.natDivSucc_le_add_left x1 (AxNat.succ AxNat.zero) x4))) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) (Rat.le (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (fun (x5 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) (Rat.le (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x3) ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x4))) (fun (x5 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) => fun (x6 : Rat.le (Rat.sub ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x3) ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) => x5) (x2 x3 x4))) (Rat.le_trans (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4)) (Rat.add (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc (AxNat.succ x1) x4)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) (Rat.le (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (fun (x5 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) (Rat.le (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4)))) => Rat.le (Rat.sub ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x3) ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (fun (x5 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) (Rat.sub ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x3) ((fun (x5 : AxNat) => CReal.seq (x0 x5) x5) x4))) => fun (x6 : Rat.le (Rat.sub ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x3) ((fun (x6 : AxNat) => CReal.seq (x0 x6) x6) x4)) (Rat.add (Rat.natDivSucc x1 x3) (Rat.natDivSucc x1 x4))) => x6) (x2 x3 x4)) (Rat.add_le_add (Rat.natDivSucc x1 x3) (Rat.natDivSucc (AxNat.succ x1) x3) (Rat.natDivSucc x1 x4) (Rat.natDivSucc (AxNat.succ x1) x4) (Rat.natDivSucc_le_add_left x1 (AxNat.succ AxNat.zero) x3) (Rat.natDivSucc_le_add_left x1 (AxNat.succ AxNat.zero) x4)))))))))

Dependencies

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

7 direct dependencies 1 direct dependents

Evidence

kernel-CReal.converges_of_scaled_cauchy

Kind: kernel-term
Status: checked

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

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.converges_of_scaled_cauchy

Kind: exhaustive-enumeration
Status: checked

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

Checker command

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

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty creal surface bounds every declaration in it, including CReal.converges_of_scaled_cauchy. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

Provenance

{
  "date": "2026-08-27",
  "curation": "generated-unreviewed",
  "generated_by": "scripts/gen-kernel-facts.py",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/)",
  "source": "Derived mechanically from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, which prints one TSV row per declaration whose fields are (prelude, kind, display name, axiom-footprint size, direct type declarations, direct declarations, direct theorems, Kernel::render_lean(declaration.ty())). formal.statement is that last field verbatim; depends_on is the direct-theorem column intersected with this ledger's registered facts; axiom_footprint is the footprint-size column, cross-checked by the whole-prelude nat_axiom_inventory run recorded in the second evidence row. No field was hand-transcribed and no prose was authored."
}