TransferFunction
plain-language theorem explainer
TransferFunction encodes the parameters of a single-pole causal response in the Caldeira-Leggett gravitational model: a DC enhancement factor Δ and positive memory timescale τ. Gravity and dissipative-dynamics researchers cite it when computing frequency-dependent kernels from bath integration. The declaration is a direct structure definition with three fields and zero proof obligations.
Claim. A structure consisting of a real DC enhancement factor $Δ$ (equal to $w-1$), a positive real memory timescale $τ$, and the condition $0<τ$. It realizes the complex response $H(iω)=1+Δ/(1+iωτ)$.
background
The Caldeira-Leggett module adapts the standard bath-of-oscillators construction to gravity, producing an action whose bath integration yields a frequency-dependent response. The single-pole form corresponds to exponential memory, with spectral density $J(Ω)≥0$ and transfer function $H(iω)$ obtained after tracing out the oscillators. Upstream, CostAlgebra.H supplies the shifted cost $H(x)=J(x)+1$ satisfying the d'Alembert identity $H(xy)+H(x/y)=2H(x)H(y)$, while PhiForcingDerived.of and SpectralEmergence.of supply the J-cost and gauge-content structures that fix the underlying forcing chain.
proof idea
This is a structure definition that directly assembles the three fields Δ, τ, and τ_pos. No lemmas are applied and no tactics are used.
why it matters
The structure supplies the input type for response_function, quadrature_function, response_at_zero, response_enhancement, and response_limit_high_freq in the same module, and for debye_kernel in CausalKernelChain. It realizes the concrete single-pole $H(iω)$ required by the gravitational Caldeira-Leggett action, linking the spectral density to the eight-tick octave and D=3 forcing steps. Module status notes that full proofs of bath integration remain pending.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.