debye_kernel
plain-language theorem explainer
The Debye kernel supplies the exponential memory function Γ(t) = (Δ/τ) exp(-t/τ) for a TransferFunction H. Modelers of single-pole causal responses in the gravity sector cite this definition. It is realized as a direct one-line expression using the exponential function on the scaled time argument.
Claim. Let $H$ be a transfer function with parameters $Δ$ and $τ$. The Debye kernel is the function $Γ:ℝ→ℝ$ defined by $Γ(t)= (Δ/τ) exp(-t/τ)$.
background
The module establishes the causal kernel chain starting from the time-domain exponential kernel. The Debye form is the single-timescale case of the memory kernel, with the integral over [0,B] yielding the truncated response $K_B(ω)$ whose limit as $B→∞$ gives the frequency-domain contribution. The TransferFunction record from the CaldeiraLeggett import provides the fields $Δ$ and $τ$. Upstream, the $H$ function from CostAlgebra reparametrizes the J-cost to $H(x)=J(x)+1$, satisfying $H(xy)+H(x/y)=2H(x)H(y)$. The BITKernelFamilies.kernel includes the exponential case as one of its families. This sits in the gravity domain, linking to the Recognition Science derivation of physics from the functional equation.
proof idea
The definition is a direct algebraic expression. It multiplies the ratio of the transfer function parameters by the real exponential of the negative scaled time.
why it matters
This definition is the concrete realization of the Debye kernel that feeds the truncated response kernel_response_trunc and the limit theorem kernel_response_limit. It fills the single-pole case in the causal-kernel chain module, whose goal is to formalize the time-to-frequency transition for the response function. The module scope notes that broader spectral densities are not yet covered. It connects to the cost algebra $H$ and the BIT kernel families upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.