CReal.ivt_bisect_cauchy: the named bisection points, under a uniformly positive derivative, form a genuine Cauchy sequence

Identifier: F:creal-ivt-bisect-cauchy
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

Under the same hypotheses as CReal.ivt_bisect_cauchy_bound -- uniform continuity AND a uniformly positive derivative bounded away from zero by 1/(k+1) -- CReal.ivt_bisect_cauchy concludes CReal.Cauchy of the sequence `e |-> CReal.ivt_bisect_hi F a b (Nat.succ (Nat.mul 2 e)) K`. This is the point at which the bisection sequence becomes something CReal's convergence machinery (CReal.converges_of_cauchy and its neighbours) can act on directly, which a sequence of CReal.ivt_approx's existential witnesses never could -- `forall e, exists x, ...` does not eliminate into a Type. It states nothing about the sequence's limit being a root of F -- that is CReal.ivt_exact_root, built on top of this fact together with CReal.converges_comp_eventually and CReal.equiv_zero_of_small.

Formal statement

theorem CReal.ivt_bisect_cauchy : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : ((x1 : CReal) -> CReal)) -> ((x2 : CReal) -> ((x3 : CReal) -> ((x4 : CReal.HasDerivativeOn x0 x1 x2 x3) -> ((x5 : CReal.UniformlyContinuousOn x0 x2 x3) -> ((x6 : CReal.le x2 x3) -> ((x7 : CReal.le (x0 x2) CReal.zero) -> ((x8 : CReal.le CReal.zero (x0 x3)) -> ((x9 : AxNat) -> ((x10 : ((x10 : CReal) -> ((x11 : CReal.le x2 x10) -> ((x12 : CReal.le x10 x3) -> CReal.le (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x9)) (x1 x10))))) -> CReal.Cauchy (fun (x11 : AxNat) => CReal.ivt_bisect_hi x0 x2 x3 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x11)) (AxNat.add (AxNat.mul (AxNat.succ (CReal.bound (CReal.add x3 (CReal.neg x2)))) (CReal.UniformlyContinuousOn.modulus x0 x2 x3 x5 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x11)))) (CReal.bound (CReal.add x3 (CReal.neg x2))))))))))))))))

Dependencies

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

2 direct dependencies 1 direct dependents

Evidence

kernel-CReal.ivt_bisect_cauchy

Kind: kernel-term
Status: checked

Supports: CReal.ivt_bisect_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.ivt_bisect_cauchy 2>/dev/null | grep -cE '^CReal\.ivt_bisect_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.ivt_bisect_cauchy

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.ivt_bisect_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.ivt_bisect_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": "curated",
  "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."
}