Fundamental Theorem of Calculus bridge hooks. More...

#include <cmath>
#include <concepts>
#include <cstddef>
#include <type_traits>
#include <utility>
import dedekind.algebra;

Include dependency graph for ftc.cppm:

Concepts
concept	dedekind::analysis::detail::IsNumericalBridgeScalar

Typedefs
template<typename R>
using	dedekind::analysis::detail::resolved_value_t

Functions
template<typename R>
constexpr auto	dedekind::analysis::detail::resolved_value (const R &x)
template<IsNumericalBridgeScalar R>
constexpr R	dedekind::analysis::detail::lift (resolved_value_t< R > value)
template<IsNumericalBridgeScalar R>
constexpr R	dedekind::analysis::detail::from_count (std::size_t value)
template<IsNumericalBridgeScalar R>
constexpr R	dedekind::analysis::detail::zero ()
template<IsNumericalBridgeScalar R>
constexpr R	dedekind::analysis::detail::two ()
template<IsNumericalBridgeScalar R>
constexpr bool	dedekind::analysis::detail::less_than (const R &a, const R &b)
template<IsNumericalBridgeScalar R>
constexpr bool	dedekind::analysis::detail::finite_value (const R &x)
template<IsNumericalBridgeScalar R>
constexpr auto	dedekind::analysis::detail::magnitude (const R &x)
template<IsNumericalBridgeScalar R>
constexpr bool	dedekind::analysis::detail::close_enough (const R &lhs, const R &rhs, const R &tolerance)
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr R	dedekind::analysis::derivative_at (F &&f, R x, R h=static_cast< R >(1e-5))
	Numerical derivative witness via central difference.
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr R	dedekind::analysis::integral_over (F &&f, R a, R b, std::size_t slices=4096)
	Numerical integral witness via trapezoidal rule (Riemann sum).
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr bool	dedekind::analysis::ftc_part_i_hypotheses (F &&f, R a, R b, std::size_t samples=32)
	FTC Part I bridge: d/dx integral_a^x f(t) dt ~= f(x).
template<detail::IsNumericalBridgeScalar R, typename F, typename Antiderivative> requires std::invocable<F, R> && std::invocable<Antiderivative, R>
constexpr bool	dedekind::analysis::ftc_part_ii_hypotheses (F &&f, Antiderivative &&antiderivative, R a, R b, std::size_t samples=32, R tolerance=static_cast< R >(1e-4))
	Numerical bridge for the sampled Part II hypothesis F' ~= f.
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr bool	dedekind::analysis::ftc_part_i_bridge (F &&f, R a, R x, R tolerance=static_cast< R >(1e-4))
	FTC Part I bridge: d/dx integral_a^x f(t) dt ~= f(x).
template<detail::IsNumericalBridgeScalar R, typename F, typename Antiderivative> requires std::invocable<F, R> && std::invocable<Antiderivative, R>
constexpr bool	dedekind::analysis::ftc_part_ii_bridge (F &&f, Antiderivative &&antiderivative, R a, R b, R tolerance=static_cast< R >(1e-4))
	FTC Part II bridge: integral_a^b f(x) dx ~= F(b)-F(a).
template<detail::IsNumericalBridgeScalar R, typename F, typename Antiderivative> requires std::invocable<F, R> && std::invocable<Antiderivative, R>
constexpr bool	dedekind::analysis::ftc_worked_theorem_chain (F &&f, Antiderivative &&antiderivative, R a, R x, R b, R tolerance=static_cast< R >(1e-4))
	Worked theorem chain combining both FTC directions.
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr std::pair< R, R >	dedekind::analysis::suggest_derivative_step_size (F &&f, R x, R tolerance=static_cast< R >(1e-6))
	Diagnostic: suggests optimal derivative step size via convergence testing.
template<detail::IsNumericalBridgeScalar R, typename F> requires std::invocable<F, R>
constexpr std::pair< std::size_t, R >	dedekind::analysis::diagnose_integral_convergence (F &&f, R a, R b, R convergence_threshold=static_cast< R >(1e-5))
	Diagnostic: validates integral convergence via Richardson extrapolation-style sampling.

Detailed Description

Fundamental Theorem of Calculus bridge hooks.

@partition :ftc

Provides small numerical bridge lemmas between derivative and integral interfaces so downstream formalization can target a stable API.

CURRENT LIMITATIONS (see backlog for actionable follow-ups):

Riemann Sum Only: integral_over() implements trapezoidal rule, a Riemann sum approximation. No Lebesgue measure, dominated convergence, or measure-theoretic abstraction. (See backlog: Integral Abstraction)
Finite Difference vs. Fréchet: derivative_at() uses raw central difference, decoupled from geometry::frechet_derivative_at(). No formal directional/Gâteaux derivatives or inverse theorems. (See backlog: Derivative Abstraction)
No Differential Forms Integration: OneForm and TwoForm exist in :forms and :exterior, but integral_over() does not support pullback, Stokes theorem, or exterior calculus. (See backlog: Forms Integration)
No Cauchy Derivative: Complex analysis and quaternion derivatives not yet formalized. (See backlog: Cauchy-Riemann Framework)
Sequence Loop Indexing: Both integral_over() and hypothesis functions use raw std::size_t loops. Should abstract via Path<R, Cardinality> monadic composition when mature. (See backlog: Sequence-Adapter Layer)

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

Note: "Hinc nostra differentialis methodus uno comprehendit calculo et inversa illa, quae olim vix unius problematis solutionem suppeditabat." — Gottfried Wilhelm Leibniz, De geometria recondita et analysi indivisibilium atque infinitorum (Acta Eruditorum, 1686). [Trans: "Hence our differential method comprehends in a single calculus also that inverse one, which formerly scarcely supplied the solution of a single problem."]

See also: #286 undergraduate calculus (work in progress): Riemann integrability and the fundamental theorem beyond numerical hypotheses.

Typedef Documentation

◆ resolved_value_t

template<typename R>

using dedekind::analysis::detail::resolved_value_t

Initial value:

std::remove_cvref_t<decltype(resolved_value(std::declval<R>()))>

Function Documentation

◆ derivative_at()

template<detail::IsNumericalBridgeScalar R, typename F>
requires std::invocable<F, R>

R dedekind::analysis::derivative_at	(	F &&	f,
		R	x,
		R	h = static_cast<R>(1e-5) )

constexprexport

Numerical derivative witness via central difference.

Implements a basic finite-difference approximation without formal connection to geometry::frechet_derivative_at(). For scalar functions, this is a Fréchet approximation in the classical sense, but should eventually bridge to the formal derivative abstraction. Consider mapping through OneForm/Covector for differential geometry.

See also: geometry::frechet_derivative_at() for formal Fréchet derivative.; backlog: Derivative Abstraction (linking code to geometry).

◆ diagnose_integral_convergence()

template<detail::IsNumericalBridgeScalar R, typename F>
requires std::invocable<F, R>

std::pair< std::size_t, R > dedekind::analysis::diagnose_integral_convergence	(	F &&	f,
		R	a,
		R	b,
		R	convergence_threshold = static_cast<R>(1e-5) )

constexprexport

Diagnostic: validates integral convergence via Richardson extrapolation-style sampling.

Computes integral_over() at increasing slice counts (100, 500, 2500, 4096) and monitors convergence drift. Returns the smallest slice count where drift ≤ convergence_threshold, plus the maximum drift observed across all refinement steps.

Parameters

f	The function to integrate.
a	Left endpoint.
b	Right endpoint.
convergence_threshold	Maximum acceptable drift between successive refinements.

Returns: Pair: (recommended_slices, max_drift_observed). If no convergence, returns (4096, max_drift).

Note: The default slices=4096 in integral_over() is a heuristic. This function helps confirm whether 4096 is sufficient for your integrand, or if a smaller slice count suffices (saving computation).

See also: backlog: Integral Abstraction, Maintenance Sweep (#123)

◆ ftc_worked_theorem_chain()

template<detail::IsNumericalBridgeScalar R, typename F, typename Antiderivative>
requires std::invocable<F, R> && std::invocable<Antiderivative, R>

bool dedekind::analysis::ftc_worked_theorem_chain	(	F &&	f,
		Antiderivative &&	antiderivative,
		R	a,
		R	x,
		R	b,
		R	tolerance = static_cast<R>(1e-4) )

constexprexport

Worked theorem chain combining both FTC directions.

Checks that a numerical accumulation differentiates back to the integrand at x, and that the same integrand integrates to the provided antiderivative delta over [a,b].

◆ integral_over()

template<detail::IsNumericalBridgeScalar R, typename F>
requires std::invocable<F, R>

R dedekind::analysis::integral_over	(	F &&	f,
		R	a,
		R	b,
		std::size_t	slices = 4096 )

constexprexport

Numerical integral witness via trapezoidal rule (Riemann sum).

Implements a Riemann sum using the trapezoidal rule, NOT a formal Lebesgue integral. Does not compose with differential forms (OneForm/TwoForm) or support Stokes' theorem. Limitations:

No measure-theoretic semantics (Lebesgue, Borel).
No form pullback or exterior calculus integration.
No dominated/monotone convergence theorems.
Raw std::size_t loop should eventually use Path monad (see backlog: Sequence-Adapter Layer).
No integration methods (by parts, substitution) or symbolic simplification (see Epic #286: Undergraduate Calculus Foundations).

See also: analysis::OneForm, TwoForm for differential forms (currently separate).; backlog: Integral Abstraction, Forms Integration, Epic #286.

◆ suggest_derivative_step_size()

template<detail::IsNumericalBridgeScalar R, typename F>
requires std::invocable<F, R>

std::pair< R, R > dedekind::analysis::suggest_derivative_step_size	(	F &&	f,
		R	x,
		R	tolerance = static_cast<R>(1e-6) )

constexprexport

Diagnostic: suggests optimal derivative step size via convergence testing.

Tests h values from 1e-8 to 1e-3 to find where derivative_at() stabilizes. Computes derivatives at decreasing step sizes and tracks the drift between successive estimates. Returns the smallest h where drift ≤ tolerance, plus the magnitude of last observed convergence drift.

Parameters

f	The function to differentiate.
x	The point at which to test the derivative.
tolerance	Convergence threshold for step size selection.

Returns: Pair: (suggested_h, last_drift_magnitude). If no convergence achieved at 1e-8, returns (1e-8, last_drift).

Note: This is a diagnostic tool. The default h=1e-5 in derivative_at() is a heuristic; this function helps validate its suitability for a specific function.

See also: backlog: Derivative Abstraction, Maintenance Sweep (#123)

Concepts

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ resolved_value_t

Function Documentation

◆ derivative_at()

◆ diagnose_integral_convergence()

◆ ftc_worked_theorem_chain()

◆ integral_over()

◆ suggest_derivative_step_size()