dual.cppm File Reference

Dual numbers 𝔻 = a + bε with ε² = 0 — forward-mode AD carrier. More...

#include <concepts>
#include <functional>
#include <limits>
#include <type_traits>
import dedekind.sets;
import dedekind.numbers;
import dedekind.geometry;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for dual.cppm:

Classes
class	dedekind::analysis::Dual< F >
	Represents f(x) + f'(x)ε. More...
struct	dedekind::category::quotient_algebra_base< dedekind::analysis::Dual< F > >
struct	dedekind::category::is_linear_action< dedekind::analysis::Dual< F >, F, std::plus< dedekind::analysis::Dual< F > >, std::plus< F >, std::multiplies< F >, std::multiplies<> >
struct	dedekind::category::is_exact_total< dedekind::analysis::Dual< F >, std::plus< dedekind::analysis::Dual< F > > >
struct	dedekind::category::is_exact_total< dedekind::analysis::Dual< F >, std::multiplies< dedekind::analysis::Dual< F > > >
struct	dedekind::category::unit_trait< dedekind::analysis::Dual< F >, std::plus< dedekind::analysis::Dual< F > > >
struct	dedekind::category::unit_trait< dedekind::analysis::Dual< F >, std::multiplies< dedekind::analysis::Dual< F > > >
struct	dedekind::category::inverse_trait< dedekind::analysis::Dual< F >, std::plus< dedekind::analysis::Dual< F > > >
struct	dedekind::category::is_homomorphism< std::decay_t< decltype(dedekind::analysis::embed_ℝ_𝔻)>, dedekind::numbers::QuadraticReal< 2 >, std::plus< dedekind::numbers::QuadraticReal< 2 > >, std::plus< dedekind::analysis::Dual< dedekind::numbers::QuadraticReal< 2 > > > >
struct	dedekind::category::is_homomorphism< std::decay_t< decltype(dedekind::analysis::embed_ℝ_𝔻)>, dedekind::numbers::QuadraticReal< 2 >, std::multiplies< dedekind::numbers::QuadraticReal< 2 > >, std::multiplies< dedekind::analysis::Dual< dedekind::numbers::QuadraticReal< 2 > > > >

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::analysis::dual_admits

Typedefs
using	dedekind::analysis::𝔻_ℚ = Dual<dedekind::numbers::Rational<>>
using	dedekind::analysis::ℚ_ = dedekind::numbers::Rational<>

Functions
template<typename F>
constexpr F	dedekind::analysis::component (const Dual< F > &d, dedekind::category::At< 1 >)
	Canonical product projections for Dual (the ADL component hook of dedekind::category::π_1 / π_2): 𝔻's storage is val / der, not the pair-like .first / .second the default projection reads, so we provide the overload here. This is what makes Dual satisfy IsProduct uniformly with Complex (P-leg), while value() / derivative() stay as the domain-specific aliases that agree with π_1 / π_2.
template<typename F>
constexpr F	dedekind::analysis::component (const Dual< F > &d, dedekind::category::At< 2 >)

Variables
constexpr 𝔻_ℚ	dedekind::analysis::eps {ℚ_{0}, ℚ_{1}}
constexpr 𝔻_ℚ	dedekind::analysis::x_seed {ℚ_{3}, ℚ_{1}}
constexpr Dual< int >	dedekind::analysis::eps_int {0, 1}
constexpr auto	dedekind::analysis::𝔻
	The canonical dual-number universe 𝔻 = 𝔸<Dual<QuadraticReal<2>>, Boole, ℶ_1> — the coat-hanger 𝔻 = Dual(ℝ) over the genuine ℝ = ℚ(√2) (mirroring ℝ and ℂ).
constexpr auto	dedekind::analysis::embed_ℝ_𝔻
	The Birkhoff S leg \(\mathbb{R}\hookrightarrow\mathbb{D}\) over the coat-hanger: QuadraticReal<2> → Dual<QuadraticReal<2>>, \(r\mapsto r+0\varepsilon\) (primal r, tangent 0).
template<typename F>
constexpr bool	dedekind::category::is_invertible_v< dedekind::analysis::Dual< F >, std::plus< dedekind::analysis::Dual< F > > >
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< std::decay_t< decltype(dedekind::analysis::embed_ℝ_𝔻)> >

Detailed Description

Dual numbers 𝔻 = a + bε with ε² = 0 — forward-mode AD carrier.

@partition :dual

dual__Partition_Move

This file relocated from dedekind.numbers:dual to dedekind.analysis:dual at PR #513: the construction is algebraically a quotient ring, but its structural meaning is differential — dual numbers are forward-mode automatic differentiation, and the partition's natural neighbours are :ftc (numerical derivative bridge), :forms (differential one-forms), and :hamilton (Hamiltonian flow on Dual-carrier symplectic state). The :analysis layer is downstream of :numbers in the build graph, so all numeric-carrier consumers (Rational<Z>, Complex<R>, IEEE<F>) remain reachable.

Copyright

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

dual__The_Nilpotent_Basis

Reifies Dual Numbers a + bε where ε² = 0. This provides the algebraic foundation for Forward-Mode Automatic Differentiation (AD).

dual__Carrier_Generality

The construction Dual(R) = R[ε]/(ε²) is well-defined over any commutative ring R. The Dual<F> constraint is std::semiregular<F> and not std::floating_point<F> (IEEE floats are not a ring): integer carriers (Dual<int>, Dual<SignedExtensionalCardinal<>>) and the modular ring (Dual<unsigned int>) instantiate cleanly and close the ring-operator surface.

Note on division semantics: Dual<F>::operator/ and inverse() delegate to F's division (F{1}/val plus -der/(val*val)), so the operator surface syntactically compiles for any F that supplies a / operator — including F=int, where the integer-division semantics give truncating, non-field results. The syntactic predicate algebra::HasFieldOperators<Dual<F>> is therefore NOT a guarantee that Dual<F> is field-shaped at the axiomatic level; it merely reports that the operator surface is closed. The field-axiomatic distinction is a job for the strict category::IsField concept (which is intentionally not specialised on Dual<int>); this file pins HasFieldOperators<Dual <ℚ>> as a positive witness and the ring-shape concepts (HasRingOperators, IsAlgebra) as the load-bearing claims for the integer-carrier extensions.

The algebraic-geometric reading of dual numbers over an arbitrary base ring — Spec(R[ε]/(ε²)) as the scheme of tangent vectors at a point — is the textbook anchor for this generality (Hartshorne, Algebraic Geometry, Exercise II.2.8; Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, §16.5).

dual__Coherence_With_Numerical_FTC_Bridge

Forward-mode AD on Dual<F> is the symbolic / exact route from a function to its derivative: f(x + ε) yields the primal in the value component and the derivative in the tangent component, mechanically, without any numerical approximation. The numerical counterpart is dedekind::analysis::ftc::derivative_at (central difference) in dedekind.analysis:ftc, which uses a small step h on a std::floating_point carrier. The two routes agree on smooth functions. Their structural divergence: :ftc currently gates on IsNumericalBridgeScalar = HasFieldOperators<R> && std::floating_point<resolved_value_t<R>>, so the analytic side is floating-point-only by design; Dual<F> generalises to discrete carriers without that restriction (the witnesses below pin one rung per supported carrier). An open architectural question is whether a downstream partition (e.g. dedekind.analysis:dual_ad) should host the AD-meaning of dual numbers and cross-link both :dual and :ftc as parallel implementations of "compute the derivative of f at x" — tracked separately, not in scope for the carrier-witness slice this file currently lands.

Note

"Musica est exercitium arithmeticae occultum nescientis se numerare animi." ("Music is the pleasure the human mind experiences from counting without being aware that it is counting.") – Gottfried Wilhelm Leibniz, letter to Christian Goldbach (1712)

See also

#272 Denotational Automatic Differentiation (work in progress): DualVector<F,N> with a directional seed, and Jacobians computed from Dual.

#286 undergraduate calculus (work in progress): a differentiability concept.

Typedef Documentation

𝔻_ℚ

using dedekind::analysis::𝔻_ℚ = Dual<dedekind::numbers::Rational<>>

dual__Formal_Verification

Variable Documentation

𝔻

auto dedekind::analysis::𝔻

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<Dual<dedekind::numbers::QuadraticReal<2>>, Boole, ℶ_1>{}

The canonical dual-number universe 𝔻 = 𝔸<Dual<QuadraticReal<2>>, Boole, ℶ_1> — the coat-hanger 𝔻 = Dual(ℝ) over the genuine ℝ = ℚ(√2) (mirroring ℝ and ℂ).

Per #559's chosen direction (option A): the named species symbols denote universe values (constexpr instances of 𝔸 over the carrier), not classifier-alias types. All seven species symbols (𝔹, ℕ, ℤ, ℚ, ℝ, ℂ, 𝔻) carry the canonical element <𝔻> scout spelling.

Post-HSP retarget: the carrier of 𝔻 is Dual<QuadraticReal<2>> — the 2nd-order quotient ℝ[ε]/(ε²) over the coat-hanger ℝ.

Cardinality is set explicitly to ℶ_1 (continuum) — 𝔻 is in bijection with ℝ × ℝ via the (a, b) coefficient pair (the same shape that gives ℂ its ℶ_1) — overriding 𝔸's ℵ_0 default. It is the cardinality of the 𝔻 modelled, not a logic: equality on ℚ(√2)[ε] is decidable, so 𝔻 answers in Boole.

Textbook construction: 𝔻 = ℝ[ε]/(ε²), a polynomial quotient: the H leg of the construction taxonomy, registered as quotient_algebra_base<Dual<F>>::type = F (below), which forwards the base's laws to 𝔻.

embed_ℝ_𝔻

auto dedekind::analysis::embed_ℝ_𝔻

inlineconstexprexport

Initial value:

=
    dedekind::category::arrow<dedekind::numbers::QuadraticReal<2>,
                              Dual<dedekind::numbers::QuadraticReal<2>>>(
        [](const dedekind::numbers::QuadraticReal<2>& r) noexcept {
          return Dual<dedekind::numbers::QuadraticReal<2>>{
              r, dedekind::numbers::QuadraticReal<2>{}};
        })

The Birkhoff S leg \(\mathbb{R}\hookrightarrow\mathbb{D}\) over the coat-hanger: QuadraticReal<2> → Dual<QuadraticReal<2>>, \(r\mapsto r+0\varepsilon\) (primal r, tangent 0).

A genuine monic ring embedding (an EmbedsAsSubalgebra S-leg, the 𝔻 sibling of embed_ℝ_ℂ / embed_ℚ_ℝ): ℝ is the constant subring \(\{\,\varepsilon\text{-part}=0\,\}\subset\mathbb{D}\) (the value-0-tangent duals). Witnessed by computation below.