quadratic.cppm File Reference

\(\mathbb{Q}(\sqrt D)\) — a genuine, decidable quadratic real field. More...

#include <compare>
#include <concepts>
#include <functional>
#include <stdexcept>
#include <type_traits>
import dedekind.numbers:rational;
import dedekind.sets;
import dedekind.order;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for quadratic.cppm:

Classes
class	dedekind::numbers::QuadraticReal< D, Q >
	A real of \(\mathbb{Q}(\sqrt D)\): \(a+b\sqrt D\). More...
struct	dedekind::category::SpeciesTraits< dedekind::numbers::QuadraticReal< D, Q > >
	Atlas registration: QuadraticReal<D,Q> is a first-class species. More...
struct	dedekind::category::is_exact_total< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::is_exact_total< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::is_associative< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::is_associative< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::is_commutative< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::is_commutative< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::unit_trait< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::unit_trait< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::category::inverse_trait< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
struct	dedekind::algebra::is_translation_invariant_ordered< dedekind::numbers::QuadraticReal< D, Q > >
	Carrier-promise: QuadraticReal<D,Q> is an ORDERED FIELD. The template gate (D>1) ∧ IsRational<Q> makes this unconditional — every instantiation is a REAL quadratic field ℚ(√D) with D>1 (no imaginary ℚ(√−n) case exists), hence formally real (−1 not a sum of squares), with a genuine total order (strong_ordering <=>, by comparing squares). So both order-compatibility axiom markers hold: O1 (translation) and O2 (scaling), closing IsOrderedMultiplicativeGroup<QuadraticReal<D,Q>> — which in turn certifies Complex<QuadraticReal<D,Q>> as a field (#818). More...
struct	dedekind::algebra::is_scaling_invariant_ordered< dedekind::numbers::QuadraticReal< D, Q > >

Namespaces
namespace	dedekind::numbers
namespace	dedekind::category

Functions
consteval bool	dedekind::numbers::detail_quadratic::is_perfect_square (long n)
	Is n a perfect square? Guards QuadraticReal against a square radicand (where \(\sqrt D\) is rational, the a/b representation is not unique, and the "extension" degenerates to \(\mathbb{Q}\)).

Variables
template<long D, typename Q>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::numbers::QuadraticReal< D, Q >, std::less_equal<> >
template<long D, typename Q>
constexpr bool	dedekind::category::is_transitive_v< dedekind::numbers::QuadraticReal< D, Q >, std::less_equal<> >
template<long D, typename Q>
constexpr bool	dedekind::category::is_antisymmetric_v< dedekind::numbers::QuadraticReal< D, Q >, std::less_equal<> > = true
template<long D, typename Q>
constexpr bool	dedekind::category::is_connex_v< dedekind::numbers::QuadraticReal< D, Q >, std::less_equal<> >
template<long D, typename Q>
constexpr bool	dedekind::category::is_distributive_v< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > > = true
template<long D, typename Q>
constexpr bool	dedekind::category::is_invertible_v< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > > = true
template<long D, typename Q>
constexpr bool	dedekind::category::is_invertible_v< dedekind::numbers::QuadraticReal< D, Q >, std::multiplies< dedekind::numbers::QuadraticReal< D, Q > > >

Detailed Description

\(\mathbb{Q}(\sqrt D)\) — a genuine, decidable quadratic real field.

@partition :quadratic

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

quadratic__A_Real_Field_You_Can_Compute

Cut<Q> (see :cut) reifies the order of the reals decidably but stops at the leaf: it cannot add two irrationals (the sum of two cuts is a Minkowski sum whose membership is \(\exists\)-over- \(\mathbb{Q}\), and the order of general sums forces the undecidable equality of reals). QuadraticReal steps just far enough to keep everything decidable: it fixes one radical extension \(\mathbb{Q}(\sqrt D)\) ( \(D\) a non-square positive integer) and represents a real as \(a+b\sqrt D,\ a,b\in\mathbb{Q}\). On this carrier the field operations \(+,-,\times,\div\) close exactly (conjugation gives the inverse: \(1/(a+b\sqrt D)=(a-b\sqrt D)/(a^2-b^2D)\)), and the order stays total and decidable (compare \(a+b\sqrt D\) to 0 by comparing \(a^2\) to \(b^2D\)). So the field laws are witnessed by computation — \((1+\sqrt2)(1-\sqrt2)=-1\) is a static_assert — not postulated on an uninhabited carrier. It models \(\mathbb{Q}(\sqrt D)\subset\mathbb{R}\), one extension, not all of \(\mathbb{R}\): the honest price of decidability.

Note

"Wir müssen wissen. Wir werden wissen." — David Hilbert (1930).