debye_kernel
The debye_kernel supplies the explicit single-timescale exponential memory kernel Γ(t) = (Δ/τ) exp(-t/τ) used in the causal response chain. Frequency-domain analysts working on transfer-function limits cite it when passing from time-domain kernels to closed-form expressions for K(ω). The definition is a direct one-line algebraic expression that extracts the Δ and τ fields from the TransferFunction record and multiplies by the standard exponential.
claimThe Debye kernel is the function Γ(t) = (Δ/τ) exp(-t/τ) for t ∈ ℝ, where Δ and τ are the strength and timescale parameters of the transfer function H.
background
The CausalKernelChain module formalizes the passage from a time-domain exponential memory kernel to its frequency response and the associated steady-state and high-frequency limits. The upstream CaldeiraLeggett.TransferFunction record supplies the two real parameters Δ and τ that appear in the kernel. Related cost-algebra definitions reparametrize the underlying functional equation as H(x) = J(x) + 1, which satisfies the d'Alembert identity H(xy) + H(x/y) = 2 H(x) H(y); the BIT kernel family already lists the exponential case Real.exp(-z/z0) as one of its constructors.
proof idea
One-line definition that directly assembles the product (H.Δ / H.τ) * Real.exp(-t / H.τ) using the record fields of the supplied TransferFunction and the standard real exponential.
why it matters in Recognition Science
This definition supplies the concrete Debye kernel that is integrated in kernel_response_trunc and whose infinite-horizon limit is proved in kernel_response_limit. It realizes the single-pole case required by the causal-kernel chain, enabling the closed-form response Δ / (1 + iωτ) that appears in the Newtonian and steady-state limits. The construction sits inside the Recognition Science framework by matching the exponential member of the BIT kernel family and supporting the transition from memory kernels to the D = 3 spatial structure.
scope and limits
- Does not treat multi-pole or continuous spectral densities.
- Does not extend the kernel to negative times.
- Does not compute the full transfer function 1 + K(ω).
- Does not address discretization or numerical quadrature.
Lean usage
kernel_response_trunc H ω Bformal statement (Lean)
136def debye_kernel (H : CaldeiraLeggett.TransferFunction) (t : ℝ) : ℝ :=
proof body
Definition body.
137 (H.Δ / H.τ) * Real.exp (-t / H.τ)
138
139
140/-- Truncated (finite-horizon) frequency response contribution from the Debye kernel:
141\[
142K_B(\omega)=\int_0^B \Gamma(t)\,e^{-i\omega t}\,dt.
143\]
144The full transfer function is `1 + K_∞(ω)`. -/