cl_action_gives_transfer_function
plain-language theorem explainer
The Caldeira-Leggett action yields the causal transfer function for dissipative dynamics in gravity. Researchers adapting quantum dissipation to gravitational systems would reference this when constructing response functions from the action integral. The proof proceeds via the trivial tactic as a temporary placeholder awaiting the explicit bath integration derivation.
Claim. The Caldeira-Leggett action $S$ gives rise to the causal transfer function $H(iω)$ obtained by integrating out the bath of harmonic oscillators.
background
The module formalizes the Caldeira-Leggett construction as a conservative action-based realization of causal-response dynamics in gravity. The action couples the baryon gravitational potential to a bath of oscillators with spectral density $J(Ω) = π c(Ω)^2 / (2 Ω) ≥ 0$, and the transfer function $H(iω)$ arises from tracing out the bath. The upstream structure for from UniversalForcingSelfReference supplies the meta-realization axioms that record structural properties required for self-reference in the forcing chain.
proof idea
The proof is a one-line wrapper that applies the trivial tactic to affirm the statement as a placeholder.
why it matters
This declaration establishes the connection between the Caldeira-Leggett action and the causal transfer function, filling a key step in the gravitational adaptation of dissipative quantum systems. It supports the Recognition Science framework by providing the structure for response functions in the context of the forcing chain (T0 to T8) and self-reference. The module notes that full proofs are pending, touching on the open question of completing the bath integration derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.