Learn · Constructive analysis
Axeyum for constructive analysts
Axeyum builds real numbers from regular rational sequences and carries explicit approximation data through its analysis library.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to constructive analysis.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What analysis remains computational when choice is not assumed?
The constructed-real library includes arithmetic, limits, uniform continuity with explicit moduli, derivatives, Riemann integration, exponential and trigonometric functions, pi, interval suprema, and constructive forms of the intermediate and extreme value theorems.
The intermediate value development can return roots to a requested accuracy. Under a uniformly positive derivative it constructs an exact root. The extreme value development currently supplies approximate maxima and a constructive supremum value rather than a general choice of an exact maximizing point.
Why it matters
What the current work makes possible
- Regular sequences form a real-number setoid without a Cauchy quotient or Quot.sound.
- Uniform continuity includes the modulus needed to run approximation procedures.
- Riemann sums converge to a total constructed-real integral.
- The kernel reports empty footprints for the constructed-real development.
Results to inspect
Open the evidence
What comes next
Extend the present base
The main next result is a complete fundamental theorem of calculus that connects the derivative and integral developments at their present level of generality.
Further work can make execution costs and modulus requirements easier to inspect, then extend integration and convergence results without losing their computational content.
Where to begin