Module Beloch.Num

Exact real algebraic numbers. A value is an exact rational Rat q (fast path: axioms 1–4 never leave ℚ), an element of a single extension of degree ≤ field_degree_cap Field {gen; coords} = coords(α) with α the root of the monic irreducible gen.mu isolated in (gen.lo, gen.hi) (fast path for axiom-5/6/7 roots, bpr2006 §12.4), or a general real algebraic number Qq backed by FLINT's qqbar (canonical minimal polynomial + certified ball; cross-field arithmetic, composite extensions). Invariant: Qq is irrational — rationals collapse to Rat. to_float is the only float, output-only. See decisions/0013-flint-qqbar-backend.md.

type t =
  1. | Rat of Q.t
  2. | Qq of Qqbar.t
  3. | Field of {
    1. gen : gen;
    2. coords : Poly.t;
    }
and gen = {
  1. mu : Poly.t;
  2. lo : Q.t;
  3. hi : Q.t;
  4. alpha : Qqbar.t Stdlib.Lazy.t;
}
val zero : t
val one : t
val of_q : Q.t -> t
val of_int : int -> t
val two_q : Q.t
val same_gen : gen -> gen -> bool
val mk_field : gen -> Poly.t -> t
val of_qq : Qqbar.t -> t
val isolate_gen : Poly.t -> Q.t -> Q.t -> Qqbar.t
val mk_gen : mu:Poly.t -> lo:Q.t -> hi:Q.t -> gen
val qq_of_gen : gen -> Qqbar.t
val to_qq : t -> Qqbar.t
val refine_alg : Poly.t -> Q.t -> Q.t -> Q.t * Q.t
val simplest_in : Q.t -> Q.t -> Q.t
val rational_roots_in : Poly.t -> Q.t -> Q.t -> Q.t list
val minimal_poly_in : Poly.t -> Q.t -> Q.t -> Poly.t option
val make : Poly.t -> Q.t -> Q.t -> t
val field_degree_cap : int
val field_upgrade : t -> t
val poly_interval : Poly.t -> Q.t -> Q.t -> Q.t * Q.t
val sign : t -> int
val neg : t -> t
val enclosure_tight : t -> Q.t -> Q.t * Q.t
val to_float : t -> float
val to_rational_string : t -> string
val embed_cache : ((gen * gen) * Poly.t option) list Stdlib.ref
val embed_cache_max : int
val embedding : into:gen -> gen -> Poly.t option
val coords_over : gen -> t -> Poly.t option
val via_field : (gen -> Poly.t -> Poly.t -> Poly.t) -> t -> t -> t option
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val inv : t -> t
val div : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val real_roots : t array -> t list
val sqrt : t -> t