response_function
plain-language theorem explainer
Definition supplying the real part C(ω) of the single-pole Caldeira-Leggett transfer function for gravitational bath models. Gravitational physicists cite it when extracting frequency-dependent response from the complex H(iω). The definition is the direct algebraic extraction of the real component from the pole expression 1 + Δ/(1 + iωτ).
Claim. For a transfer function structure with DC enhancement parameter Δ and memory timescale τ > 0, the response function is defined by C(ω) := 1 + Δ / (1 + (ω τ)^2).
background
The Caldeira-Leggett module adapts the harmonic-oscillator bath construction to gravity, yielding a conservative action whose bath integration produces a frequency-dependent response. The TransferFunction structure encodes the single-pole form H(iω) = 1 + Δ/(1 + iωτ) where Δ = w - 1 is the DC enhancement and τ > 0 is the memory timescale. This definition isolates the real part C(ω) = Re[H(iω)]. Upstream results on the shifted cost H(x) = J(x) + 1 and on spectral emergence supply the functional-equation and dimensional constraints that justify the single-pole ansatz.
proof idea
One-line definition that directly unfolds the real-part expression of the complex transfer function.
why it matters
The definition is the concrete object referenced by the response_at_zero, response_enhancement and response_limit_high_freq theorems in the same module and by the real-part identification theorem in CausalKernelChain. It supplies the explicit single-pole response required by the gravitational adaptation of the Caldeira-Leggett action. The module documentation records that full proofs of bath integration remain pending.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.