Gravity Caldeira Leggett Cl Action Gives Transfer Function

A placeholder for a future proof

The Caldeira-Leggett model describes a quantum system that loses energy by coupling it to a bath of many harmonic oscillators. When the bath is traced out, the system feels damping and random fluctuations whose sizes are linked by the fluctuation-dissipation theorem. This is a standard construction in open quantum systems, used for decades to model friction and noise at the quantum scale.

The framework's library contains a file that adapts this construction to gravity. It defines an action with a Newtonian potential, an auxiliary field, and an oscillator bath, along with a spectral density J(Ω) that must be non-negative for all frequencies. It also defines a Debye spectral density with a single-pole form, and from that a transfer function H(iω) = 1 + Δ/(1 + iωτ), where Δ is a DC enhancement and τ is a memory timescale.

The library proves several properties of this transfer function: at zero frequency the response equals 1 + Δ, at high frequency it approaches 1 (the Newtonian limit), and for positive Δ the response is always greater than 1, meaning the bath enhances rather than suppresses the response. These are real theorems about the defined objects.

The declaration cl_action_gives_transfer_function, however, is a placeholder. Its statement is simply True, and its proof is trivial. The docstring says clearly that the full derivation, showing that integrating out the bath and the auxiliary field yields the claimed transfer function, is left for future formalization. The declaration establishes only that the framework intends to prove this connection, not that the connection has been proved.

What this means in practice: the framework has set up the vocabulary of a gravitational Caldeira-Leggett model and proved facts about the transfer function it defines, but it has not yet shown that this transfer function actually follows from the action. The bridge between the action and the response remains open.

/-- The Caldeira-Leggett action gives rise to the causal transfer function. -/
theorem cl_action_gives_transfer_function :
    True := by  -- Placeholder for the full derivation
  trivial

/-- 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 gives rise to the transfer function. The framework does not claim that this gravitational adaptation has been derived from the forcing chain. No claim is made about the empirical validity of the Debye spectral density for gravity.

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: