quadrature_function
plain-language theorem explainer
The quadrature_function extracts the imaginary part of the single-pole transfer function for a dissipative gravitational response. Physicists adapting the Caldeira-Leggett bath model to gravity would cite it when isolating the quadrature component of the frequency-dependent response. The definition follows by direct substitution of the complex form H(iω) = 1 + Δ/(1 + iωτ) into the imaginary-part operator and algebraic simplification of the resulting expression.
Claim. For a transfer function with DC enhancement parameter Δ and memory timescale τ > 0, the quadrature function at angular frequency ω is S(ω) = -Δ ω τ / (1 + (ω τ)^2).
background
The Caldeira-Leggett module supplies structure and definitions for an action-based realization of causal-response dynamics in gravity. A system coordinate couples to a bath of harmonic oscillators; tracing out the bath produces a frequency-dependent response whose single-pole form is encoded by the TransferFunction structure: H(iω) = 1 + Δ/(1 + iωτ), where Δ = w - 1 is the DC enhancement and τ is the memory timescale satisfying τ > 0.
proof idea
One-line definition that substitutes the fields Δ and τ of the TransferFunction into the closed-form imaginary part of the single-pole response and performs the algebraic simplification of the complex division.
why it matters
This definition supplies the explicit quadrature component required by the key-properties section of the same module, including response_at_zero and response_limit_high_freq. It contributes the dissipative part of the transfer function in the gravitational adaptation of the Caldeira-Leggett construction, which sits downstream of the cost-algebra H that converts the Recognition Composition Law into the d'Alembert equation. The module status records that the full bath-integration proof remains pending.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.