numeric.cppm File Reference

The Numeric Landing (IEEE 754 and Lipschitz Boundaries). More...

#include <cmath>
#include <concepts>
#include <functional>
#include <limits>
#include <optional>
import dedekind.category:topoi;

Include dependency graph for numeric.cppm:

Classes
struct	dedekind::category::NumericWitness< T >
	A typed witness of numeric classification in Ω_K3. More...
struct	dedekind::category::IntervalBoundaryPolicy< T >
	Closed interval policy [lower, upper] for integral species. More...
struct	dedekind::category::FullMachineBoundaryPolicy< T >
	Full-machine boundary policy (no clipping). More...
struct	dedekind::category::NaNHolePolicy< T >
	IEEE-754 NaN-hole classifier policy for floating species. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsNumericSpecies
concept	dedekind::category::IsLipschitzBoundaryPolicy
	User-provided Lipschitz boundary policy over a numeric species.
concept	dedekind::category::IsNumericHoleClassifier
	A characteristic morphism χ: T -> Ω_K3 for numeric support.

Macros
#define	DEDEKIND_NOINLINE
#define	DEDEKIND_BRIDGE_CONSTEXPR   constexpr
#define	DEDEKIND_BRIDGE_NOINLINE

Functions
template<std::signed_integral T>
constexpr std::optional< T >	dedekind::category::detail::checked_add_signed (T a, T b)
template<std::signed_integral T>
constexpr std::optional< T >	dedekind::category::detail::checked_mul_signed (T a, T b)
template<typename T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr Ternary	dedekind::category::classify_numeric (T x, Policy policy)
	Classify a numeric value under a user policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_add (T a, T b, Policy policy)
	Certified integer addition with an explicit support policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_add (T a, T b, Policy policy={})
	Certified floating addition with NaN-hole policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_mul (T a, T b, Policy policy)
	Certified integer multiplication with an explicit support policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_mul (T a, T b, Policy policy={})
	Certified floating multiplication with NaN-hole policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_div (T a, T b, Policy policy)
	Certified integer division with explicit policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_div (T a, T b, Policy policy={})
	Certified floating division with NaN-hole policy.
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_add_int_interval (int a, int b, IntervalBoundaryPolicy< int > policy)
	Non-template bridge functions for profiler-friendly attribution.
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< unsigned int >	dedekind::category::certify_add_uint_full (unsigned int a, unsigned int b, FullMachineBoundaryPolicy< unsigned int > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_mul_int_interval (int a, int b, IntervalBoundaryPolicy< int > policy)
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_div_int_full (int a, int b, FullMachineBoundaryPolicy< int > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_add_double_nan (double a, double b, NaNHolePolicy< double > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_mul_double_nan (double a, double b, NaNHolePolicy< double > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_div_double_nan (double a, double b, NaNHolePolicy< double > policy={})

Variables
constexpr bool	dedekind::category::numeric_uses_builtin_overflow_checks = false
	Compile-time diagnostic: portable fallback overflow path enabled.

Detailed Description

The Numeric Landing (IEEE 754 and Lipschitz Boundaries).

@partition :numeric

This partition defines first-pass, honest APIs for machine-numeric hazards:

• NaN holes (floating-point truth holes)
• Lipschitz boundaries (bounded-support certificates)

The boundary may not always be inferable from the type alone. For such cases, users can provide a boundary policy explicitly.

Copyright

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

Note

"If one proves the equality of two numbers a and b by showing first that a <= b and then that a >= b, it is unfair; one should instead show that they are really equal by disclosing the inner ground for their equality." – Emmy Noether, as quoted by Hermann Weyl (1935)