kernel_response_trunc
plain-language theorem explainer
Defines the truncated frequency response integral K_B(ω) from the Debye kernel as the finite-horizon integral of Γ(t) exp(-i ω t) dt from 0 to B. Researchers constructing causal transfer functions in gravity or dissipative models cite this as the approximant to the full response 1 + K_∞(ω). The declaration is realized directly as an integral expression over the real interval (0, B).
Claim. Let $H$ be a transfer function. For real frequencies $ω$ and cutoffs $B$, the truncated kernel response is $K_B(ω) = ∫_0^B Γ(t) e^{-i ω t} dt$, where $Γ(t)$ is the Debye kernel associated to $H$. The full transfer function is then $1 + K_∞(ω)$.
background
The module formalizes the single-timescale exponential memory kernel (Debye/single-pole response) and its frequency-domain properties. The Debye kernel is the causal exponential decay for $t ≥ 0$, drawn from the exponential case of the BIT kernel family. TransferFunction encodes the amplitude and timescale parameters that enter the kernel and the resulting response. This sits inside the causal-kernel chain whose goal is to connect the time-domain kernel through its Fourier transform to the steady-state and Newtonian limits of the real part of the transfer function.
proof idea
This is a definition whose body is the integral expression itself: the debye_kernel evaluated at $t$, lifted to ℂ, multiplied by the complex exponential, and integrated from 0 to B. No lemmas are applied inside the definition; the surrounding comments note that the closed form follows from integral_exp_smul_neg once the Laplace exponent is introduced.
why it matters
The definition supplies the finite-horizon object whose limit as $B → ∞$ is proved in the downstream theorem kernel_response_limit, which recovers the closed-form response $(H.Δ) / (1 + i ω H.τ)$. It therefore completes the time-to-frequency bridge inside the CausalKernelChain module and supports the steady-state and high-frequency limits required for the response function $C(ω) = Re H(iω)$. The construction remains within the Debye (single-pole) case; broader spectral densities are noted as future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.