transfer_function_complex
transfer_function_complex defines the complex frequency response for a single-pole Debye kernel as 1 plus Delta over 1 plus i omega tau. Gravity modelers formalizing causal memory effects cite it to obtain the real response function from the complex form. The definition is a direct algebraic casting of the real parameters Delta and tau into complex arithmetic.
claimFor a transfer function structure with DC enhancement $Delta$ and positive memory timescale $tau$, the complex response at real frequency $omega$ equals $1 + frac{Delta}{1 + i omega tau}$.
background
The CausalKernelChain module formalizes the single-timescale exponential memory kernel and its frequency-domain properties. The upstream TransferFunction structure supplies Delta as the DC enhancement (w minus 1) and tau as the memory timescale with the axiom 0 less than tau. The exponential kernel itself appears in BITKernelFamilies as exp of minus z over z0, while the shifted cost H from CostAlgebra satisfies the d'Alembert form of the recognition composition law.
proof idea
Direct definition that expands to the single-pole expression by casting the real fields Delta and tau into complex numbers and performing the indicated division.
why it matters in Recognition Science
This definition supplies the complex transfer function used by the three downstream results in the same module: kernel_response_limit, response_function_is_real_part, and transfer_function_eq_one_plus_kernel. It completes the frequency-domain step of the causal-kernel chain for the Debye case, linking the time-domain exponential kernel to its steady-state and Newtonian limits. The module notes that broader spectral densities remain outside the current formalization.
scope and limits
- Does not treat multi-pole or continuous spectral densities.
- Does not establish convergence of the truncated integral to the closed form.
- Does not impose numerical bounds on Delta or tau beyond positivity of tau.
- Does not embed the transfer function into the forcing chain or phi-ladder.
Lean usage
theorem response_is_real (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : CaldeiraLeggett.response_function H ω = (transfer_function_complex H ω).re := by exact response_function_is_real_part H ωformal statement (Lean)
127def transfer_function_complex (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : ℂ :=
proof body
Definition body.
128 (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ))
129
130
131/-- The Debye exponential kernel for a single-timescale response:
132\[
133\Gamma(t) = \frac{\Delta}{\tau} e^{-t/\tau},\quad t \ge 0.
134\]
135We treat it as a function on `ℝ` and integrate it on `[0,B]` (then take `B → ∞`). -/