A carrier's construction: D is built from a base algebra and computes with the base's operations. ::type is the base; ::times_mixes_plus says whether D's × multiplies out (a quotient of a polynomial ring, the Cauchy product: the base's × and +) or stays componentwise (a product, a subalgebra: the base's × alone). Declared once per construction leg in dedekind.algebra (H / P / S / F), never per carrier; a carrier declaring two legs is ambiguous here, honestly. More...

Detailed Description

template<typename D>
struct dedekind::category::construction_base< D >

A carrier's construction: D is built from a base algebra and computes with the base's operations. ::type is the base; ::times_mixes_plus says whether D's × multiplies out (a quotient of a polynomial ring, the Cauchy product: the base's × and +) or stays componentwise (a product, a subalgebra: the base's × alone). Declared once per construction leg in dedekind.algebra (H / P / S / F), never per carrier; a carrier declaring two legs is ambiguous here, honestly.

total__totality

The totality certificate: a carrier's operation is defined on every pair (it is a magma). Five sufficient paths, each a pragmatic certificate and none a canonical taxonomy boundary. Four are declared by the carrier in :species: periodicity (modular wrap), idempotence (globally stable), saturation (escalation to an extended-range sentinel), exactness (exact arithmetic with no rounding, bounded only by the out-of-memory tripwire). The fifth is read off the construction here: a carrier built from a base algebra computes with the base's operations, so it is total exactly when those are, by whatever path certified them.

The first three are machine-finite (totality by staying in a bounded range); the fourth lets a genuinely exact number field be a Magma — and hence reach IsField — rather than being excluded as "non-machine-total". It is registered for Rational = ℚ and QuadraticReal = ℚ(√D). SignedCardinality = ℤ and Cardinality = ℕ are total via is_saturating (they escalate to \(\pm\aleph_0\)), so IsRing <ℤ> / IsSemiring <ℕ> hold through the saturating path, witnessed at :integer / :natural. (The two postures are distinct and a carrier picks exactly one.) The named concept IsSaturating that wraps is_saturating_v lives in dedekind.category:mereology; here we reach for the underlying trait variables directly so this upstream-foundational layer does not depend on that partition.

Template Parameters

D	the constructed carrier.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/total.cppm