Constructive mathematics and mathlib

Bishop-style real numbers

Axeyum's CReal is a Bishop-style setoid of regular rational sequences. A setoid retains the sequences and defines when they denote the same real number. Its equality relation is CReal.Equiv; arithmetic must be proved to respect that relation. The construction avoids quotient soundness and extensionality axioms in the native results discussed here.

A continuity modulus supplies the input precision needed for a requested output accuracy. Axeyum carries this modulus as data in UniformlyContinuousOn. Its derivative structure, HasDerivativeOn, also carries a modulus for its uniform remainder estimate. These are stronger inputs than a bare assertion of continuity or pointwise differentiability.

The resulting library includes general approximation theorems, exact identities, and implications that expose the assumptions needed for stronger conclusions. The tables distinguish those forms from exact computer algebra system (CAS) computations and imported classical proofs. These forms are not a ranking: a stronger conclusion may require stronger hypotheses or additional axioms.

Lean and mathlib can also express constructive mathematics. Bishop's construction is established mathematics. Axeyum's contribution here is its own development of the carriers and their laws, connected to the system's computation routes and fact ledger. mathlib has much broader mathematical coverage and an established interactive proof environment.

Real-number construction · Derivative definition · Measured library and axiom comparison

Intermediate value theorem

Assume a ≤ b and F(a) ≤ 0 ≤ F(b). The distinction is between making the residual small and obtaining an exact zero.

Statement family and evidence
Form	Hypotheses	Conclusion	Proof route
General constructive form	Uniform continuity on [a,b], with an explicit modulus.	For each n, there exists x ∈ [a,b] with \|F(x)\| ≤ 1/(n+1). This bounds the residual, not the distance to an exact root.	Native kernel proof; empty axiom footprint. Evidence record
Logical boundary	An exact root in [0,1] of Fᵥ(t) = min(t, max(t − 1, v)). The library proves continuity and the endpoint signs.	The root implies v ≤ 0 ∨ 0 ≤ v for the real parameter v. A general exact-root principle would supply this real-order principle.	Native kernel proof of an implication; empty axiom footprint. Evidence record
Exact polynomial computation	A rational polynomial and rational endpoints with a strict sign change; within the procedure's resource limits.	The CAS names an algebraic root. The certificate checker re-derives the root and interval conditions using exact arithmetic.	CAS certificate. The full root claim is not reconstructed in the kernel. Evidence record
Classical mathlib form	Continuity on an ordered interval and a target value between the endpoint values; more general ordered spaces are supported.	intermediate_value_Icc establishes an exact preimage. Axeyum also retains a labeled import of this theorem.	Imported proof; classical source dependencies and import assumptions remain recorded. Evidence record

Follow the IVT dependency graph

There is also a native exact-root theorem under stronger analytic hypotheses. CReal.ivt_exact_root assumes the derivative structure, uniform continuity, the endpoint signs, and a supplied positive lower bound on the derivative throughout the interval. Its proof has an empty axiom footprint. Exact constructive roots are therefore available beyond the polynomial case when the hypotheses provide enough information.

Extreme value theorem

The value of a supremum and a point attaining it are different mathematical objects. Constructing the former need not locate the latter.

Statement family and evidence
Form	Hypotheses	Conclusion	Proof route
General constructive form	Uniform continuity on [a,b], with an explicit modulus, and a ≤ b.	For each n, there exists x ∈ [a,b] such that F(y) ≤ F(x) + 1/(n+1) for every y ∈ [a,b]. The proof uses the constructed supremum and its approximation law.	Native kernel proof; empty axiom footprint. Evidence record
Logical boundary	An attained maximum of t ↦ t·v on [0,1]. The library also proves the family's continuity and boundedness hypotheses.	The maximizing point implies v ≤ 0 ∨ 0 ≤ v. General attainment would supply the same real-order principle as exact IVT.	Native kernel proof of an implication; empty axiom footprint. Evidence record
Exact polynomial computation	A rational polynomial on a closed rational interval; within the procedure's resource limits.	The CAS compares endpoints and algebraic critical points to name an exact maximizing point and value. Its checker re-derives the certificate.	CAS certificate. Completeness of the candidate set remains in the CAS trust record. Evidence record
Classical mathlib form	A nonempty compact set and a continuous function, in the theorem's more general topological and ordered setting.	IsCompact.exists_isMaxOn establishes a point attaining the maximum. Axeyum retains a labeled import.	Imported proof; classical source dependencies and import assumptions remain recorded. Evidence record

Follow the EVT dependency graph

Fundamental theorem of calculus

Constructive analysis also proves exact identities. Axeyum constructs the integral and proves both directions of the fundamental theorem of calculus. For these statements, let a ≤ b and let F have a supplied uniform continuity modulus and an explicit bound on [a,b].

The integral is constructed from finite left-endpoint Riemann sums. The continuity modulus controls their approximation error as the partitions become finer. The development proves that different continuity witnesses give equivalent integral values, and that an interval can be split at any point inside it. Those proofs must compare sums built on different partitions, including cases where a subinterval has zero width.

FTC I then proves that the constructed antiderivative has derivative F. FTC II applies to any antiderivative G satisfying the stated derivative structure. Its proof compares G with the constructed antiderivative: their difference has zero derivative and is therefore constant. Evaluating at the endpoints gives the exact identity ∫ₐᵇ F = G(b) − G(a). The integral construction and proofs expose this chain of estimates and equalities.

Exact constructive calculus and mathlib counterparts
Form	Additional inputs	Conclusion	Evidence
Constructive FTC I	The integral construction uses the interval and continuity data.	The constructed antiderivative has derivative F in the sense of HasDerivativeOn, including its modulus.	CReal.hasDerivative_antiderivative. Native kernel proof; empty axiom footprint.
Constructive FTC II	An antiderivative G, with HasDerivativeOn G F a b.	The integral of F from a to b is equivalent to G(b) − G(a). This is exact equality of represented real numbers under CReal.Equiv.	CReal.integral_eq_antideriv_diff. Native kernel proof; empty axiom footprint.
mathlib FTC I	Interval integrability, strong measurability at the endpoint neighborhood filter, and continuity at that endpoint.	A derivative of the interval integral at that endpoint. mathlib also provides one-sided and more general derivative forms.	intervalIntegral.integral_hasDerivAt_right. Source statement comparison.
mathlib FTC II	HasDerivAt for G with derivative F on the unordered interval, and interval integrability of F.	The interval integral of F equals G(b) − G(a). Its hypotheses do not require Axeyum's explicit uniform derivative modulus.	intervalIntegral.integral_eq_sub_of_hasDerivAt. Source statement comparison.

FTC has no corresponding obstruction row here: these exact constructive identities are already proved under their stated hypotheses. The mathlib FTC links compare statements; the recorded IVT/EVT axiom measurements do not establish footprints for these FTC declarations.

Constructed from definitions, with no added axioms

Axeyum constructs its real numbers and proves the native results on this page without added axioms. The named mathlib IVT and EVT proofs depend on propositional extensionality, classical choice, and quotient soundness. Axeyum instead carries the required constructions and quantitative hypotheses explicitly, and proves what follows from them.

An axiom footprint lists the axioms reached by a proof's dependencies. An empty footprint means that traversal reaches no axiom declarations. The result still depends on the kernel's inference rules and implementation, and a theorem can still have hypotheses.

Measurement and import evidence

At mathlib commit c5ea00351c28e24afc9f0f84379aa41082b1188f, under Lean 4.30.0, the recorded source-kernel measurements for the named IVT and EVT counterparts report propext, Classical.choice, Quot.sound. Axeyum's imported evidence records also list the translation and import assumptions used to admit those proofs. The source-kernel measurement and the import record describe different parts of that checking process.

The boundary results prove conditional implications to the real-order principle ∀v, v ≤ 0 ∨ 0 ≤ v, often called analytic LLPO, the lesser limited principle of omniscience. They do not prove classical mathematics inconsistent, nor do they refute exact roots or maxima in individual cases. Their role is to identify what a general exact-existence principle would entail.

A constructive existential theorem also differs from an executable function returning a witness. In this kernel, Exists lives in Prop; its proof cannot generally be eliminated into data. The approximate IVT statement alone therefore does not provide an executable root selector. Computed constructions and CAS certificates require their own definitions and correctness evidence.

Choosing a theorem for the next proof

For an automated reasoner, a theorem's hypotheses, available constructions, and proof dependencies determine where it can be used. A goal that mentions a root leaves several questions open: how accurate must it be, must the result supply a value that a computation can use, and which assumptions are available?

Mathematical choices when a later step needs a root
Need	Applicable result	What must be supplied or accepted
A small residual	Approximate IVT establishes \|F(x)\| at the requested accuracy.	The interval, endpoint signs, and uniform continuity modulus. Its existential conclusion alone does not supply an executable selector.
An exact zero with derivative separation	Constructive exact IVT establishes F(x) ≈ 0.	The derivative structure, uniform continuity, endpoint signs, and an explicit positive lower bound on the derivative.
An exact algebraic root for computation	Polynomial IVT in the CAS returns a named algebraic root and a certificate.	A rational polynomial and rational bracket with a strict sign change. The procedure has resource limits and its own certificate-checking trust requirements.
General classical exact existence	The labeled mathlib import establishes an exact preimage.	The imported theorem's carriers and hypotheses, together with its recorded axioms and import assumptions. It does not directly produce a native CReal value.

Here ≈ denotes exact equality under CReal.Equiv. The choices above describe mathematical applicability. An automated planner must still match the formal types and discharge every hypothesis before it can use a result.

Axeyum already records facts with their formal statements, proof routes, axiom footprints, and dependencies. Its frontier selector checks dependency readiness and whether a registered operation or producer contract can act under the route and gate policies. The table describes the richer theorem-selection behavior sought in the research vision; it is not a report that the selector currently makes all of these analytic choices automatically.

The IVT decay bound also supports a geometric-series estimate. The EVT proof composes the supremum laws. A planner that recognizes these shared requirements can seek an intermediate result that serves several proofs. Checked results then expand the set of choices available for later work.

IMPS and Ωmega provide earlier examples of theorem reuse and mathematical proof planning. The system comparisons examine how their designs can inform this work.

Native evidence snapshot: 03ae4a3c9, 2026-10-05. IVT/EVT audit (ADR-0875) · FTC construction · Existence and data discussion (diary, 2026-08-26).