transfer_function_eq_one_plus_kernel
plain-language theorem explainer
The theorem equates the complex transfer function of a Caldeira-Leggett system to the explicit single-pole Debye form 1 plus Δ over 1 plus iωτ. Frequency-domain modelers of dissipative kernels in Recognition Science gravity contexts would cite the identity. The proof is a one-line simplification from the definition of transfer_function_complex.
Claim. Let $H$ be a Caldeira-Leggett transfer function with real parameters $Δ$ and $τ$. For real frequency $ω$, the complex transfer function satisfies $H(iω) = 1 + Δ / (1 + i ω τ)$.
background
The CausalKernelChain module formalizes the single-timescale exponential memory kernel and its frequency-domain properties under the Debye realization. The module goal is to derive the time-domain causal kernel, the transfer function, and the steady-state plus Newtonian limits for the real part of the response. Upstream, CostAlgebra.H reparametrizes the shifted cost as $H(x) = J(x) + 1$, converting the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$.
proof idea
The proof is a one-line wrapper that applies the definition of transfer_function_complex via the simp tactic.
why it matters
This identity supplies the explicit frequency-domain form of the Debye kernel inside the causal-kernel chain. It directly enables the subsequent real-part extraction for the response function. The result realizes the single-pole case before the module's stated scope limitation to broader spectral densities; it sits downstream of the J-cost algebra and phi-forcing structures but carries no used-by edges yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.