Expand description
The real closure of the hyperreals: real algebraic Puiseux series in dt, exactly.
The hyperreals a program builds with the field operations are the rational functions of dt over
the real algebraic numbers (Hyperreal); the real closure of that ordered field adds a root to
every polynomial that changes sign. Its elements are the real Puiseux series algebraic over it —
√dt = dt^(1/2), √(1 + dt) = 1 + dt/2 − dt²/8 + … — and every one is held exactly, as a
Puiseux: a squarefree polynomial it is a root of, with coefficients rational functions of
s = dt^(1/q), and the branch of that polynomial’s real roots it is.
Branches. The real roots of a polynomial over K_s are found by Newton’s polygon: an edge of
the lower convex hull of the points (i, v(p_i)) of slope −γ holds the roots of valuation γ,
and the real roots c of the edge’s characteristic polynomial their leading coefficients. A
fractional γ refines s to a root of itself; a simple c separates its root from every other,
and a repeated one is followed into the polynomial s^(-v)·P(s^γ·(c + z)) until its roots
separate. A separated branch has one root of positive valuation left, so each further term is
−lc(p₀)/lc(p₁)·s^(v₀ − v₁), computed only as far as a comparison, a selection or a printed digit
asks.
Operations. α + β is a root of Res_z(P(z), Q(y − z)), α·β of Res_z(P(z), z^n·Q(y/z)),
α^k of Res_z(P(z), y − z^k) and ⁿ√α of P(y^n), each resultant interpolated in y at
integer points from resultants over K_s. The result is the one root whose expansion agrees with
the operation applied to the operands’ expansions through the order at which that polynomial’s
roots all differ — so every decision is exact, and two values are equal exactly when their
difference is the zero root of its polynomial.
One form for a value. A value that is a rational function of a root of dt is held as that
function (Closed::Field when it is one of dt itself), found by Padé reconstruction from its
expansion with the degree bounds Gauss’s lemma gives and checked exactly. It prints as that
function; a value with a power that is one prints as a radical, √(1 + dt), 2·∛(1 + dt); any
other prints by its two leading terms and the order of the rest, 2√2 - (√2/16)·dt^2 + O(dt^3).
Structs§
- Power
Refusal - Why a power of a value of the real closure is refused: the hyperreal’s own refusal, its degree
counted in the root
dt^(1/q)the value is a rational function of. - Puiseux
- A real algebraic Puiseux series in
dt: a root ofpoly(squarefree, overK_s,s^q = dt), picked by its branch. See the module documentation.
Enums§
- Closed
- A value of the real closure in its one form: a hyperreal when it is a rational function of
dt, otherwise a Puiseux series that is no such function.