Gravity Caldeira Leggett Spectral Density

The spectral density

A spectral density is a function that tells you how strongly a system interacts with its environment at each frequency. In the Caldeira-Leggett model of dissipation, a quantum system is coupled to a bath of harmonic oscillators, and the spectral density J(Ω) measures the strength of that coupling as a function of oscillator frequency. The Recognition Science framework formalizes this as a structure: a function J from real numbers to real numbers, together with a proof that it is never negative for positive frequencies. That nonnegativity condition is called passivity, and it encodes the physical requirement that the bath can only absorb energy, not amplify it.

The framework's library also defines a particular choice of spectral density, the Debye or single-pole form, J(Ω) = (2λγ/π) · Ω/(γ² + Ω²), where γ is a cutoff frequency (the inverse memory time) and λ is the coupling strength. It proves that this Debye form is nonnegative whenever the coupling and cutoff are positive. From the spectral density, the library derives the coupling function c(Ω) = √(2J(Ω)Ω/π), which appears in the action coupling the system to the bath.

The library then defines a transfer function H(iω) = 1 + Δ/(1 + iωτ), where Δ is a DC enhancement and τ is the memory timescale. It proves three properties of this transfer function: at zero frequency the response equals 1 + Δ; at high frequency the response approaches 1, the Newtonian limit; and if Δ is positive, the response is always greater than 1, meaning the bath enhances rather than suppresses the response.

In Recognition Science, this formalization is a step toward a gravitational adaptation of Caldeira-Leggett: an action coupling a baryon potential to an auxiliary field and an oscillator bath, with the spectral density defined as above. The framework's library states that this action gives rise to the causal transfer function, but that statement is a placeholder, not a proved theorem. The full derivation, integrating out the bath and the auxiliary field to obtain the transfer function, is left for future formalization.

What the declaration establishes is precise but limited. It gives a machine-checked definition of a spectral density, a specific Debye form, and proved properties of the associated transfer function. It does not establish that the Caldeira-Leggett action actually produces that transfer function, nor that this model correctly describes gravitational dissipation in the physical world. Those remain open targets, not achievements.

/-- A spectral density function \(J(\Omega)\) for the oscillator bath.
    Must satisfy \(J(\Omega) \geq 0\) for all \(\Omega > 0\) (passivity). -/
structure SpectralDensity where
  J : ℝ → ℝ
  nonneg : ∀ ω, 0 < ω → 0 ≤ J ω

lemma debye_spectral_nonneg (lam γ ω : ℝ) (hlam : 0 < lam) (hγ : 0 < γ) (hω : 0 < ω) :
    0 ≤ debye_spectral lam γ ω := by
  unfold debye_spectral
  -- All factors are positive, so the product is positive
  positivity

/-- 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 declaration does not prove that the Caldeira-Leggett action produces the transfer function; that derivation is a placeholder. The declaration does not establish that this model describes actual gravitational dissipation. The declaration does not derive the spectral density from first principles; it defines it as a structure with a positivity condition.

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: