transfer_function_eq_one_plus_kernel
plain-language theorem explainer
The theorem states that the complex transfer function for a Debye kernel equals one plus the single-pole term involving strength Δ and relaxation time τ. Modelers of causal response in gravity or dissipative systems cite this when moving between time-domain kernels and frequency responses. The proof is a one-line simplification that unfolds the definition of the complex transfer function.
Claim. Let $H$ be a transfer function with real parameters $Δ$ (strength) and $τ$ (relaxation time). For real frequency $ω$, the complex transfer function satisfies $H(iω) = 1 + Δ / (1 + i ω τ)$.
background
The module formalizes the single-timescale exponential memory kernel (Debye/single-pole response) and its frequency-domain properties: the time-domain causal kernel for $t ≥ 0$, the transfer function $H(iω)$, and the steady-state and Newtonian limits of the real part $C(ω) = Re H(iω)$. The TransferFunction structure supplies the two parameters $Δ$ and $τ$ that define this kernel. Upstream, CostAlgebra.H reparametrizes the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$, which converts the Recognition Composition Law into the d'Alembert equation used in the ledger factorization.
proof idea
One-line wrapper that applies the definition of transfer_function_complex via the simp tactic.
why it matters
This identity supplies the explicit Debye form inside the causal-kernel chain, enabling the subsequent real-part extraction that yields the paper's response function. It occupies the frequency-domain step of the single-timescale kernel formalization and sits downstream of the J-cost and ledger structures that originate in the forcing chain (T5–T8). No downstream uses are yet recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.