CReal.ivt_bisect_invariant: the computable bisection bracket satisfies the same six-part invariant as the existential one

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

Recorded description

CReal.ivt_bisect_lo/CReal.ivt_bisect_hi compute a bracket as actual DATA -- a Bool-selected pair of CReal values that can be evaluated -- rather than an Exists-wrapped witness the way CReal.ivt_step/CReal.ivt_iter produce theirs. CReal.ivt_bisect_invariant proves that this computed bracket, after k steps at a fixed slack index n, satisfies the identical six-part invariant (nesting inside [P0, Q0], the weak sign condition at both endpoints, and geometric width (Q0-P0)*(1/2)^k) that the existential construction satisfies. The point of doing this at all: a sequence of CReal.ivt_approx's existential witnesses cannot be formed, because Exists does not eliminate into a Type, so no Nat -> CReal function of approximate roots exists from ivt_approx alone. This fact is what makes CReal.ivt_bisect_hi usable as one term of an actual sequence, and it underlies CReal.ivt_exact_root's construction of an EXACT root -- it is not itself a statement about roots or about IVT's conclusion.

Formal statement

theorem CReal.ivt_bisect_invariant : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : AxNat) -> ((x4 : CReal.le x1 x2) -> ((x5 : CReal.le (x0 x1) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x3))) -> ((x6 : CReal.le (CReal.neg (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x3))) (x0 x2)) -> ((x7 : AxNat) -> And (CReal.le x1 (CReal.ivt_bisect_lo x0 x1 x2 x3 x7)) (And (CReal.le (CReal.ivt_bisect_lo x0 x1 x2 x3 x7) (CReal.ivt_bisect_hi x0 x1 x2 x3 x7)) (And (CReal.le (CReal.ivt_bisect_hi x0 x1 x2 x3 x7) x2) (And (CReal.le (x0 (CReal.ivt_bisect_lo x0 x1 x2 x3 x7)) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x3))) (And (CReal.le (CReal.neg (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x3))) (x0 (CReal.ivt_bisect_hi x0 x1 x2 x3 x7))) (CReal.Equiv (CReal.add (CReal.ivt_bisect_hi x0 x1 x2 x3 x7) (CReal.neg (CReal.ivt_bisect_lo x0 x1 x2 x3 x7))) (CReal.mul (CReal.add x2 (CReal.neg x1)) (CReal.pow (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ AxNat.zero))) x7)))))))))))))))

Dependencies

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

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

Evidence

kernel-CReal.ivt_bisect_invariant

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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