mathlib and the Axeyum fact ledger

Axeyum's CReal uses Bishop-style regular sequences of rational numbers. Each sequence carries a proved error bound. A setoid keeps those sequences as separate objects and supplies an equivalence relation saying when they denote the same real number. Real-number equality is the defined relation CReal.Equiv.

This choice creates proof obligations throughout the library. Arithmetic must preserve the equivalence relation. Approximation bounds must survive composition. A continuity modulus must supply the input precision needed for a requested output accuracy. The IVT and EVT dependency graphs show how the resulting facts support further analysis.

Axeyum's approximate Intermediate Value Theorem establishes points where a function is as close to zero as requested. Its approximate Extreme Value Theorem establishes points whose values are within the requested error of every value on the interval. Both assume uniform continuity with an explicit modulus. Their recorded proofs have empty axiom footprints.

The named mathlib counterparts establish exact existence in more general settings, with the axiom dependencies listed below. Axeyum's results preserve explicit approximation information under constructive foundations. They do not identify CReal with mathlib's real-number type or recover the classical conclusions unchanged.

Constructed-real implementation · Bishop-setoid design. Lean and mathlib also support constructive mathematics; the comparison concerns these specific developments.

mathlib supports both constructive and classical mathematics. Its axiom footprint therefore belongs to each declaration, not to the library as a whole. Lean can report that footprint.