response_function
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ωτ).
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the transfer function from the underlying action integral.
- Does not enforce the fluctuation-dissipation theorem.
- Does not specify the bath spectral density J(Ω).
- Does not treat multi-pole or non-exponential memory kernels.
Lean usage
theorem response_at_zero (H : TransferFunction) : response_function H 0 = 1 + H.Δ := by unfold response_function; simpformal statement (Lean)
99def response_function (H : TransferFunction) (ω : ℝ) : ℝ :=
proof body
Definition body.
100 1 + H.Δ / (1 + (ω * H.τ)^2)
101
102/-- The imaginary part of the transfer function (quadrature function).
103 \(S(\omega) = \text{Im}[H(i\omega)] = -\frac{\Delta \cdot \omega\tau}{1 + (\omega\tau)^2}\) -/