kernel_response_trunc
kernel_response_trunc supplies the truncated frequency response integral for the Debye kernel in the causal chain. Gravity and fluid modelers cite it when bounding finite-time memory effects before taking the steady-state limit. The definition directly encodes the integral of the kernel times the complex exponential factor over the interval from zero to B.
claimFor transfer function $H$, frequency $ω$, and bound $B$, define the truncated response by $K_B(ω) = ∫_0^B Γ(t) e^{-i ω t} dt$, where $Γ(t)$ is the Debye kernel associated with $H$. The complete transfer function recovers as $1 + lim_{B→∞} K_B(ω)$.
background
This module develops the causal-kernel chain from the time-domain exponential memory kernel to its frequency-domain transfer function. The Debye kernel realizes the single-pole response with relaxation time $τ$ drawn from the TransferFunction record. It connects to the Recognition Science cost algebra where the shifted cost H satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The exponential kernel case appears in the BITKernelFamilies definition, while the CPM2D bridge packages the underlying model for defect and energy interpretations.
proof idea
The definition is the explicit integral over the finite interval [0, B] of the Debye kernel evaluated at t, multiplied by the complex exponential exp(-i ω t). It prepares the ground for the limit theorem by providing the finite-B approximant, with closed-form evaluation deferred to integral_exp_smul_neg and the atTop tendsto lemma.
why it matters in Recognition Science
This definition anchors the finite-horizon response that kernel_response_limit lifts to the closed-form limit (H.Δ) / (1 + i ω H.τ). It completes the time-to-frequency step in the causal kernel chain, linking the exponential memory to the real-part response function used in gravity calculations. The module notes that this covers only the single-pole Debye case.
scope and limits
- Does not derive the closed-form expression for the integral.
- Does not treat kernels with multiple relaxation times.
- Does not incorporate the full Recognition Composition Law directly.
- Does not address numerical stability of the truncation.
formal statement (Lean)
145def kernel_response_trunc (H : CaldeiraLeggett.TransferFunction) (ω B : ℝ) : ℂ :=
proof body
Definition body.
146 ∫ t in (0 : ℝ)..B,
147 ((debye_kernel H t : ℝ) : ℂ) * Complex.exp (-(Complex.I * (ω : ℂ) * (t : ℂ)))
148
149
150/-!
151### Bridge lemma (frequency-domain closed form)
152
153For τ>0, define `a = (1/τ) + i ω`. Then
154
155 exp(-t/τ) * exp(-i ω t) = exp(-(a * t)).
156
157The truncated integral can be evaluated in closed form using `integral_exp_smul_neg`,
158then the `B → ∞` limit is obtained from `tendsto_exp_neg_mul_ofReal_atTop`.
159-/
160
161/-! ### Laplace transform limit and transfer-function bridge -/
162
163/-- The complex exponent `a = (1/τ) + i ω` appearing in the Debye kernel transform. -/