CReal.ivt_bisect_cauchy_bound: the named bisection points at any two accuracies are close, as a real-valued bound

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

Recorded description

Under a STRONGER hypothesis than the rest of the ivt_approx family -- a uniformly positive derivative on [a, b], bounded away from zero by 1/(k+1), not merely uniform continuity -- CReal.ivt_bisect_cauchy_bound bounds abs (X m - X n) by 1/(m+1) + 1/(n+1) for the named bisection points X at any two accuracy indices m, n. This is a genuine Cauchy-type estimate, but it is a REAL-VALUED (CReal) inequality, not yet CReal.Cauchy's canonical rational-sample form -- the bridge to that form is a separate, IVT-independent lemma (CReal.cauchy_of_abs_diff_le). The derivative hypothesis is what this fact needs to even be true: without it, two bisection runs at different accuracies are not comparable at all, since the underlying brackets need not be nested -- recorded as a verified negative result for the alternative diagonal-bisection construction in creal/ivt.rs's own documentation of CReal.ivt_bisect_diag.

Formal statement

theorem CReal.ivt_bisect_cauchy_bound : ((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))))) -> ((x11 : AxNat) -> ((x12 : AxNat) -> CReal.le (CReal.abs (CReal.add (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))))) (CReal.neg (CReal.ivt_bisect_hi x0 x2 x3 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x12)) (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)) x12)))) (CReal.bound (CReal.add x3 (CReal.neg x2)))))))) (CReal.ofRat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x9))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x9))) x12))))))))))))))))

Dependencies

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

11 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.ivt_bisect_cauchy_bound

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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_bound. 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."
}