response_function_is_real_part
plain-language theorem explainer
Physicists modeling dissipative kernels or frequency responses in Recognition Science gravity cite this result to equate the real response function with the real part of the complex transfer function. It confirms that the paper-defined real-valued C(ω) matches Re of the transfer function at real ω for any Caldeira-Leggett H. The tactic proof unfolds both sides, introduces the denominator w = 1 + iωτ, verifies its real part and squared norm by direct expansion, then reduces the real part of the quotient via div_re and add_re.
Claim. Let $H$ be a Caldeira-Leggett transfer function with real parameters $Δ$ and $τ$. For any real frequency $ω$, the paper's real-valued response function $C(ω)$ equals the real part of the complex transfer function: $C(ω) = Re[transfer_function_complex(H, ω)]$.
background
This module formalizes the causal-kernel chain from the time-domain exponential memory kernel (causal for $t ≥ 0$) through its frequency response to the steady-state and Newtonian limits of the real response. The local setting is the Debye single-pole realization only; broader spectral densities require additional Fourier or Laplace machinery not yet present. The module goal is to establish the transfer function $H(iω)$ and the identification $C(ω) = Re H(iω)$ as the foundation for those limits.
proof idea
The tactic proof unfolds response_function and transfer_function_complex, then sets $w := 1 + i ω τ$. It proves $w.re = 1$ by simplification of the imaginary term. A calculation block expands Complex.normSq w to obtain $1 + (ω τ)^2$ after substituting the real and imaginary parts. It next shows that the real part of $Δ / w$ equals $Δ / (1 + (ω τ)^2)$ using div_re together with the prior facts on $w$. The final simp step applies add_re to finish the identification.
why it matters
The declaration secures the paper's identification of the real-valued response function as the real part of the complex transfer function, a required step before the module can derive the ω → 0 and ω → ∞ limits. It sits inside the gravity domain of the Recognition Science framework and supports consistency between time-domain kernels and frequency-domain analysis. No downstream uses are recorded yet, so its integration into higher gravitational models remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.