REAL NUMBERS

-type represents the real numbers at an axiomatic level, focusing on limit-based properties for functional analysis. It balances classical completeness with computational efficiency, tailored to Schwartz’s framework.

This approach uses , , and axiomatically, with Z3 enforcing arithmetic and order properties, while leaving room for future refinements like Dedekind cuts via quotient types.

Formation

(-Formation). The real numbers are a type , equipped with constants (,), casting functions , , order (, , , , ) and arithmetic (, , , , , , , , , , ), satisfying completeness via limits.

type real_ineq = Lt | Gt | Lte | Gte | Eq | Neq
type real_op = Plus | Minus | Times | Div | Neg | Pow | Abs | Ln | Sin | Cos | Exp

type exp =
  | Real (* ℝ *)
  | RealIneq of real_ineq * exp * exp (* <, <=, >, >=, = *)
  | RealOps of real_op * exp * exp (* +, -, /, *, ^, exp, sin, cos, abs, neg, ln *)
  | NatToReal of exp (* casting *)

Axiomatic Limit Level

is defined axiomatically with completeness: every bounded sequence has a limit if Cauchy, and every non-empty bounded set has a supremum and infimum. Limits are handled via , avoiding explicit construction.

let real_complete (a : exp) : exp =
  Limit (a, Infinity, Var "l", True)

Advantages

: The limit-based approach simplifies analysis by assuming completeness axiomatically, enabling integration and without constructing from scratch.

: Z3 integration verifies real arithmetic and inequalities (e.g., ), aligning with classical analysis and Schwartz’s needs.

Limitations

: Lacking a constructive definition (e.g., Cauchy sequences or Dedekind cuts), relies on external solvers (Z3) for decidability, limiting proof-theoretic introspection.

: Fine-grained properties (e.g., distinguishing irrationality) are not natively supported, as the focus is on functional limits over structural detail.

let real_order (x : exp) : exp =
  RealIneq (Gte, RealOps (Times, x, x), Zero)

Future Support: Dedekind Cuts

Future extensions could introduce a type, as in Lean, to define via Dedekind cuts: pairs of subsets of where and . This would enable constructive reals if needed.

Such detalisation is deferred, as current axiomatic suffices for and in Schwartz’s analysis, with Z3 handling precision.

Theorems

(Completeness). Every non-empty, bounded above subset has a supremum, axiomatized via .

(Bolzano-Weierstrass). Every bounded sequence in has a convergent subsequence, implicit in our limit axioms.

let bolzano_weierstrass (a : exp) : exp =
  Exists ("b", Seq Real, Limit (b, Infinity, Var "l", True))