response_at_zero
plain-language theorem explainer
The theorem states that the response function at zero frequency equals one plus the DC enhancement parameter for any valid TransferFunction. Gravitational modelers adapting Caldeira-Leggett baths to dissipative dynamics would cite this to fix the static limit. The proof is a one-line wrapper that unfolds the response_function definition and simplifies the resulting expression.
Claim. For a transfer function with DC enhancement parameter $Δ$, the real part of the response satisfies $C(0) = 1 + Δ$.
background
The Caldeira-Leggett module adapts the standard bath-of-oscillators construction to gravity by coupling a baryon potential to a continuum of harmonic modes whose spectral density yields a causal response. The TransferFunction structure encodes the single-pole form $H(iω) = 1 + Δ/(1 + iωτ)$ with $Δ = w - 1$ the DC enhancement and $τ > 0$ the memory time. Its real part is extracted by the response_function definition $C(ω) = 1 + Δ / (1 + (ωτ)^2)$. Upstream, the algebra CostAlgebra.H supplies the shifted cost $H(x) = J(x) + 1$ that converts the Recognition Composition Law into the d'Alembert equation used to motivate the functional form.
proof idea
The proof is a one-line wrapper: it unfolds the response_function definition and applies simp, which substitutes ω = 0 to obtain the constant 1 + Δ directly.
why it matters
The result fixes the zero-frequency anchor of the gravitational Caldeira-Leggett response, confirming that the static limit recovers the enhanced Newtonian value w = 1 + Δ. It supplies one of the concrete evaluation points required by the module's structure definitions before the pending integration-out-of-the-bath theorems can be stated. The module doc-comment notes that full proofs of the transfer-function derivation from the action remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.