debye_kernel
plain-language theorem explainer
The Debye kernel supplies the explicit single-timescale exponential memory response Γ(t) = (Δ/τ) exp(-t/τ) for t ≥ 0, with Δ and τ drawn from the TransferFunction record. Modelers of causal relaxation in gravity or dissipation contexts cite this as the base time-domain object. It is realized by a direct one-line algebraic expression.
Claim. The Debye kernel is the function Γ(t) = (Δ/τ) exp(-t/τ) for t ≥ 0, where Δ and τ are the parameters of the transfer function H.
background
The module formalizes the single-timescale exponential memory kernel (Debye/single-pole response) and its frequency-domain properties. The TransferFunction record supplies the two real parameters Δ and τ that scale the amplitude and set the relaxation time. Upstream, the BITKernelFamilies.kernel definition already enumerates an exponential case of the form exp(-z/z0), and the CostAlgebra.H reparametrization converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
Direct definition that inserts the two fields of the TransferFunction record into the standard exponential expression.
why it matters
This definition is the time-domain starting point for kernel_response_trunc and kernel_response_limit, which compute the truncated and limiting frequency responses. It fills the Debye case inside the causal-kernel chain whose goal is to move from the exponential kernel through the transfer function to the steady-state and Newtonian limits. The module explicitly restricts scope to this single-pole realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.