Path D to totality: the operation is total because the carrier is exact — arithmetic with no rounding, Op(a,b) defined and lossless up to the carrier's out-of-memory tripwire. The archetypes are the exact number fields (Rational = ℚ, QuadraticReal = ℚ(√D)) under + and *. Distinct from the three machine-finite paths, which are total by staying in a bounded range (wrap / stabilise / saturate); an exact carrier is total because its arithmetic is closed and exact.
More...
Detailed Description
struct dedekind::category::is_exact_total< T, Op >
Path D to totality: the operation is total because the carrier is exact — arithmetic with no rounding, Op(a,b) defined and lossless up to the carrier's out-of-memory tripwire. The archetypes are the exact number fields (Rational = ℚ, QuadraticReal = ℚ(√D)) under + and *. Distinct from the three machine-finite paths, which are total by staying in a bounded range (wrap / stabilise / saturate); an exact carrier is total because its arithmetic is closed and exact.
- Note
- Total for all practical purposes. ℕ, ℤ, ℚ (and the reals built on ℚ) are designed so the boundary on a computation is physical — the deployer's chosen carrier precision, exhausted only when the machine runs out of memory — and explicit in the data type, not a silent arithmetic wraparound. That finite scope is one reading of Eqn 2 (a carrier models \(\le\beth_1\) but materialises \(<\aleph_0\)): responsibility for the boundary rests with whoever deploys, and it is clear from the type. So this trait certifies exactness-and-totality in that regime; keeping it a distinct EXACT path (rather than folding ℚ into "saturating") records that ℚ is an exact field bounded by physics, not a designed saturating semiring. Opt-in (default false).
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/total.cppm
