Use of Axeyum
Axeyum constructs the supremum value and proves its upper-bound and approximation laws. The final proof chains the inequalities supplied by those laws.
- Components
- Axeyum KernelAxeyum Library
Recorded result
For every requested accuracy, the theorem establishes a point such that every function value on the interval is at most the selected value plus that tolerance.
How the proof uses the library
The approximate Extreme Value Theorem (EVT) builds on a supremum: the least upper bound of the function's values. Its earlier proofs supply both an upper bound and points close to it. Chaining these bounds gives an approximate maximum.
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.
The supremum is the least upper bound of the function's values. Its construction starts with maxima over finite samples of the interval. The continuity modulus controls the error between samples. Refining the samples produces a convergent sequence of values, from which Axeyum constructs the supremum.
The next proofs establish what that value means. The upper-bound law says that every function value on the interval is at most the supremum. The approximation law supplies a point whose value is within the requested error of the supremum.
The final EVT proof chains these inequalities: every function value is at most the supremum, and the supremum is at most the selected value plus the allowed error. The selected point is therefore an approximate maximum. This step reuses the existing laws and the transitivity of the ordering: inequalities can be chained.
The continuity bound also helps prove that function values lie below the supremum, the least upper bound of those values. Follow the Intermediate Value Theorem (IVT) 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 | IsCompact.exists_isMaxOn |
| Inputs | Uniform continuity on an ordered closed interval, with an explicit modulus. | Continuity on a nonempty compact set; the theorem covers spaces beyond real intervals. |
| Conclusion | A point whose value is within the requested error of every value on the interval. | A point that attains the maximum 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.evt_approx_max: the Extreme Value Theorem's honest row 1 -- an approximate maximum kernel-lean · F:creal-evt-approx-max
- CReal.supOn exists as a total, axiom-free CReal function -- the supremum value of a uniformly continuous function on [a, b] kernel-lean · F:creal-supon
- CReal.supOn_ub: the upper-bound law -- supOn dominates F at every point of [a, b] kernel-lean · F:creal-supon-ub
- CReal.supOn_approx_lub: the approximate least-upper-bound law -- supOn is approached to any requested accuracy kernel-lean · F:creal-supon-approx-lub