The Birkhoff S leg \(\mathbb{Q}\hookrightarrow\mathbb{R}\): a genuine monic homomorphism into the \(\mathbb{Q}(\sqrt2)\) coat-hanger, with computed witnesses, plus its graph \(\Gamma=\operatorname{graph}(\text{embed})\subseteq\mathbb{Q}\times \mathbb{R}\) reifying the arrow relationally. More...

#include <concepts>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.numbers:quadratic;
import dedekind.relational;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for real_bridge.cppm:

Classes
class	dedekind::numbers::EmbedRationalToReal< I >
	The field embedding \(\mathbb{Q}\hookrightarrow\mathbb{R} =\mathbb{Q}(\sqrt2)\), \(q\mapsto q+0\sqrt2\). More...
struct	dedekind::category::is_homomorphism< dedekind::numbers::EmbedRationalToReal< I >, dedekind::numbers::Rational< I >, std::plus< dedekind::numbers::Rational< I > >, std::plus< dedekind::numbers::QuadraticReal< 2, dedekind::numbers::Rational< I > > > >
	S-leg is structure-preserving (witness: preserves + and ×; 0 and 1 are computed). More...
struct	dedekind::category::is_homomorphism< dedekind::numbers::EmbedRationalToReal< I >, dedekind::numbers::Rational< I >, std::multiplies< dedekind::numbers::Rational< I > >, std::multiplies< dedekind::numbers::QuadraticReal< 2, dedekind::numbers::Rational< I > > > >

Namespaces
namespace	dedekind::numbers
namespace	dedekind::category

Variables
constexpr EmbedRationalToReal	dedekind::numbers::embed_ℚ_ℝ {}
	The canonical S-leg instance \(\mathbb{Q}\hookrightarrow\mathbb{R}\).
template<typename I>
constexpr bool	dedekind::category::is_monic_arrow_v< dedekind::numbers::EmbedRationalToReal< I > > = true
	S-leg is monic (witness: \(a\neq b\Rightarrow embed(a)\neq embed(b)\)).

Detailed Description

The Birkhoff S leg \(\mathbb{Q}\hookrightarrow\mathbb{R}\): a genuine monic homomorphism into the \(\mathbb{Q}(\sqrt2)\) coat-hanger, with computed witnesses, plus its graph \(\Gamma=\operatorname{graph}(\text{embed})\subseteq\mathbb{Q}\times \mathbb{R}\) reifying the arrow relationally.

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

real_bridge__The_S_Leg

\(\mathbb{R}=\mathbb{A}\langle\mathbb{Q}(\sqrt2)\rangle\) is the algebraic coat-hanger (a first-class IsField value; see :quadratic). This partition hangs the first HSP leg off it: \(\mathbb{Q}\hookrightarrow \mathbb{R}\), \(q\mapsto q+0\sqrt2\), as an EmbedsAsSubalgebra arrow.

The contrast with the retired PlatonicReal is the whole point. There the subalgebra legs were postulated on an uninhabited stub; here the arrow lands in a genuine, inhabited field, so the homomorphism and injectivity laws are run at compile time (embed(a+b)==embed(a)+embed(b), embed injective) rather than declared on faith. The opt-in is_homomorphism / is_monic_arrow_v registrations below are backed, one-for-one, by the static_asserts in real_bridge__Formal_Verification.

Classes

Namespaces

Variables

Detailed Description

real_bridge__The_S_Leg