Use of Axeyum
Axeyum's constructed-real library combines bisection, a quantitative decay bound, and an explicit continuity modulus. Its proof kernel checks the resulting general theorem.
- Components
- Axeyum KernelAxeyum Library
Recorded result
For every requested accuracy, the theorem establishes a point in the interval where the absolute value of the function is at most that tolerance.
How the proof uses the library
The approximate Intermediate Value Theorem (IVT) combines repeated bisection, a bound on how fast the interval shrinks, and a continuity bound. Together they establish a point where the function is as close to zero as requested.
The dependencies form a directed acyclic graph: each arrow runs from a prerequisite to a result that uses it, with no circular chain of justification. The diagram selects direct links from the ledger; each node opens its formal statement and evidence.
Bisection halves an interval while preserving the conditions needed for a root approximation. A separate proof repeats that step. It establishes how the interval's width changes, but still needs a connection between width and the desired error in the function's value.
A decay bound supplies that connection alongside the continuity modulus. The modulus is an explicit rule: given an allowed error in the output, it says how close the inputs must be. The proof combines these ingredients to establish the requested bound on the function's value.
The graph exposes different jobs within one proof. Interval refinement, quantitative estimates, and continuity each supply a prerequisite. The final theorem uses their conclusions together, with their hypotheses preserved.
The same decay bound also supports a geometric-series estimate. Its usefulness extends beyond the theorem that motivated this use.
The continuity bound also helps prove that function values lie below the supremum, the least upper bound of those values. Follow the Extreme Value Theorem (EVT) development to see another use of the shared library.
What the constructive foundation changes
Axeyum builds these proofs over Bishop-style constructive reals. A real number carries a sequence of rational approximations with a proved error bound. A setoid equips these sequences with a defined equivalence relation: different sequences can denote the same real number without being the same object.
The library proves that arithmetic respects this equivalence. It also carries the continuity modulus needed to choose the approximation precision. The proof therefore has to account for the data each later construction needs.
The comparison uses named proofs from Lean's library of formal mathematics, called mathlib.
| Property | Axeyum construction | Named mathlib counterpart |
|---|---|---|
| Proof | Constructed-real proof | intermediate_value_Icc |
| Inputs | Uniform continuity on an ordered closed interval, with an explicit modulus. | Continuity on an interval; the theorem covers a more general ordered topological setting. |
| Conclusion | A point where the function is within the requested error of zero, given endpoint values bracketing zero. | Every value between the endpoint values is attained exactly. |
| Axioms reported by the source kernel | Empty footprint for this proof. | propextClassical.choiceQuot.sound |
Classical.choice permits selection from an existence claim without
supplying a construction;
propext identifies logically equivalent propositions;
Quot.sound identifies equivalent representatives in a quotient. The Axeyum
proof uses none of these. Its kernel rules and the theorem's stated hypotheses still
govern the result.
Lean and mathlib also support constructive mathematics. These are specific proofs with different hypotheses and conclusions. Bishop's construction is established mathematics; Axeyum develops it within its own kernel and library, carrying explicit approximation information through the dependency graph.
Axeyum ledger at 03ae4a3c9. Mathlib at c5ea00351, Lean 4.30.0; the mathlib axiom list is Lean's own report. Recorded comparison (ADR-0875) . Imported proof and its separate trust record .
Supporting artifacts
Artifact pages contain the formal statement, proof route, evidence, provenance, and direct dependency graph recorded in the ledger.
- CReal.ivt_approx: the constructive approximate Intermediate Value Theorem -- roots to any requested accuracy kernel-lean · F:creal-ivt-approx
- CReal.ivt_iter: n-fold bisection, bracket width shrinking geometrically as (1/2)^n kernel-lean · F:creal-ivt-iter
- [generated] kernel theorem CReal.pow_half_le_natDivSucc (creal prelude, axiom-free, prose not curated) kernel-lean · F:creal-pow-half-le-natdivsucc