Gravity Caldeira Leggett Transfer Function

The response function

A transfer function is the ratio of a system's output to its input, expressed in the frequency domain. For a linear system, it completely characterizes the response: feed in a sinusoidal input at frequency ω and the output is that same frequency, scaled and shifted in phase by the transfer function's magnitude and argument. The classical Caldeira-Leggett formalism builds such functions for dissipative quantum systems by coupling a coordinate to a bath of harmonic oscillators; tracing out the bath leaves damping and fluctuations linked by the fluctuation-dissipation theorem.

In the Recognition Science framework's machine-checked library of formal theorems, the declaration TransferFunction models a specific single-pole response. The structure carries two parameters: Δ, the DC enhancement, and τ, the memory timescale, with the constraint that τ is positive. From these it defines a real response function C(ω) = 1 + Δ/(1 + (ωτ)²) and a quadrature function S(ω) = −Δ·ωτ/(1 + (ωτ)²), which are the real and imaginary parts of the complex transfer function H(iω) = 1 + Δ/(1 + iωτ).

Three theorems about this structure are proved in the library. At zero frequency, the response equals 1 + Δ, the DC enhancement. At high frequency, the response tends to 1, the Newtonian limit. And when Δ is positive, the response is everywhere greater than 1, a passivity property meaning the system enhances rather than suppresses. The library also defines a Debye spectral density J(Ω) = (2λγ/π)·Ω/(γ² + Ω²) with a proved nonnegativity lemma, and a coupling function derived from it.

What the declaration does not claim is as important as what it proves. The docstring states plainly that full proofs that integrating out the bath yields this transfer function are pending; the theorem named cl_action_gives_transfer_function is a placeholder whose proof is `trivial`, not a derivation. The structure establishes the form and the properties that follow from that form, not the physical mechanism that produces it. The framework models the response as single-pole with exponential memory, but the action-based derivation connecting the Caldeira-Leggett action to this H(iω) remains open formalization work.

/-- The complex transfer function \(H(i\omega)\) for a single-pole response.
    \(H(i\omega) = 1 + \frac{\Delta}{1 + i\omega\tau_\star}\)

    where \(\Delta = w - 1\) is the DC enhancement. -/
structure TransferFunction where
  Δ : ℝ  -- DC enhancement (w - 1)
  τ : ℝ  -- Memory timescale
  τ_pos : 0 < τ

/-- At zero frequency, the response equals \(1 + \Delta = w\). -/
theorem response_at_zero (H : TransferFunction) :
    response_function H 0 = 1 + H.Δ := by
  unfold response_function
  simp

/-- At infinite frequency, the response approaches 1 (Newtonian limit). -/
theorem response_limit_high_freq (H : TransferFunction) (hΔ : H.Δ ≠ 0) :
    Filter.Tendsto (response_function H) Filter.atTop (nhds 1) := by
  -- As ω → ∞, Δ/(1 + (ωτ)²) → 0
  unfold response_function
  -- Show the denominator tends to `+∞` as ω → +∞.
  have hmul : Filter.Tendsto (fun ω : ℝ => ω * H.τ) Filter.atTop Filter.atTop := by
    simpa using ((Filter.tendsto_id).atTop_mul_const H.τ_pos)
  have hsq : Filter.Tendsto (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ)) Filter.atTop Filter.atTop :=
    (Filter.tendsto_pow_atTop (α := ℝ) (n := 2) (by decide)).comp hmul
  have hmono :
      (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ))
        ≤ᶠ[Filter.atTop] (fun ω : ℝ => 1 + (ω * H.τ) ^ (2 : ℕ)) :=
    Filter.Eventually.of_forall (fun _ω => by linarith)
  have hden :
      Filter.Tendsto (fun ω : ℝ => 1 + (ω * H.τ) ^ (2 : ℕ)) Filter.atTop Filter.atTop :=
    Filter.tendsto_atTop_mono' Filter.atTop hmono hsq

  have hinv :
      Filter.Tendsto (fun ω : ℝ => (1 + (ω * H.τ) ^ (2 : ℕ))⁻¹) Filter.atTop (nhds 0) :=
    (tendsto_inv_atTop_zero).comp hden

  have hfrac_mul :
      Filter.Tendsto (fun ω : ℝ => H.Δ * (1 + (ω * H.τ) ^ (2 : ℕ))⁻¹) Filter.atTop (nhds 0) := by
    have hΔconst : Filter.Tendsto (fun _ω : ℝ => H.Δ) Filter.atTop (nhds H.Δ) := by
      simpa using (tendsto_const_nhds : Filter.Tendsto (fun _ω : ℝ => H.Δ) Filter.atTop (nhds H.Δ))
    -- H.Δ * (denom)⁻¹ → H.Δ * 0 = 0
    simpa using (hΔconst.mul hinv)

  have hfrac :
      Filter.Tendsto (fun ω : ℝ => H.Δ / (1 + (ω * H.τ) ^ (2 : ℕ))) Filter.atTop (nhds 0) := by
    simpa [div_eq_mul_inv] using hfrac_mul

  -- Add back the constant `1`.
  have hone : Filter.Tendsto (fun _ω : ℝ => (1 : ℝ)) Filter.atTop (nhds 1) := by
    simpa using (tendsto_const_nhds : Filter.Tendsto (fun _ω : ℝ => (1 : ℝ)) Filter.atTop (nhds 1))
  simpa using hone.add hfrac

/-- Passivity (enhancement, not suppression): if \(\Delta > 0\), then \(C(\omega) > 1\). -/
theorem response_enhancement (H : TransferFunction) (hΔ : 0 < H.Δ) (ω : ℝ) :
    1 < response_function H ω := by
  unfold response_function
  have h : 0 < H.Δ / (1 + (ω * H.τ)^2) := by
    apply div_pos hΔ
    have : 0 ≤ (ω * H.τ)^2 := sq_nonneg _
    linarith
  linarith

What this page does not claim

The transfer function is not derived from the Caldeira-Leggett action; that derivation is explicitly pending. The framework does not claim this single-pole form is the only possible response for gravitational memory. No claim is made that the parameters Δ and τ are determined by the forcing chain rather than chosen.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/CaldeiraLeggett.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: