transfer_function_complex
plain-language theorem explainer
The definition supplies the complex frequency response H(iω) = 1 + Δ/(1 + iωτ) for the single-pole Debye kernel in causal gravity models. Researchers working on memory kernels or response functions in cosmology cite it to move from time-domain exponentials to frequency space. It is implemented as a direct algebraic expression using the DC enhancement and timescale parameters from the TransferFunction record.
Claim. Let $H$ be a transfer function structure with DC enhancement parameter $Δ$ and memory timescale $τ > 0$. The complex transfer function at real frequency $ω$ is $1 + Δ / (1 + i ω τ)$.
background
The module formalizes the causal-kernel chain from the time-domain exponential kernel Γ(t) = (Δ/τ) exp(−t/τ) for t ≥ 0 to its frequency-domain properties. The upstream TransferFunction structure supplies the parameters: Δ as DC enhancement (w − 1) and τ as memory timescale with the positivity hypothesis 0 < τ. The local setting restricts to the single-timescale Debye (single-pole) case; broader spectral densities are noted as future work.
proof idea
This is a direct definition that substitutes the fields Δ and τ from the TransferFunction record into the standard single-pole expression. No lemmas or tactics are invoked; the body is the literal algebraic formula given in the doc-comment.
why it matters
It supplies the core object used by kernel_response_limit, response_function_is_real_part, and transfer_function_eq_one_plus_kernel in the same module. The definition completes the frequency-domain half of the Debye-kernel formalization, linking the exponential memory kernel to its steady-state and Newtonian limits while remaining inside the Recognition Science causal structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.