Encyclopedia Gravity Gravity Caldeira Leggett Response Limit High Freq

ARTICLE 4 claims 3 theorems 1 open

Gravity Caldeira Leggett Response Limit High Freq

A machine-checked theorem confirms that a dissipative gravitational response fades to the Newtonian value at high frequencies, but only for a specific model, not for gravity itself.

Verify this page

The high-frequency limit

The Caldeira-Leggett model describes how a system loses energy by coupling to a bath of harmonic oscillators, a standard tool in quantum physics for treating friction and fluctuations. The Recognition Science framework adapts this construction to gravity by treating the gravitational potential as the system coordinate and a spectrum of oscillators as the bath. In this adaptation, the response of the gravitational field to a disturbance is encoded in a transfer function H(iω), a complex-valued function of frequency ω whose real part C(ω) measures how strongly the field responds at that frequency.

The theorem response_limit_high_freq states that as the frequency ω grows without bound, the response function C(ω) approaches 1. The response function has the single-pole form C(ω) = 1 + Δ / (1 + (ωτ)²), where Δ is a constant called the DC enhancement and τ is the memory timescale, the characteristic time over which the bath remembers its past. At zero frequency, C(0) = 1 + Δ, so the parameter Δ measures how much the response is enhanced at low frequencies relative to the Newtonian value. At high frequencies, the denominator (1 + (ωτ)²) grows without bound, so the enhancement term Δ / (1 + (ωτ)²) shrinks to zero, leaving C(ω) → 1. The theorem requires only that Δ ≠ 0, which excludes the trivial case where the response is already identically 1 at all frequencies.

The limit C(ω) → 1 is the Newtonian limit: at high frequencies, the dissipative enhancement vanishes and the response returns to the bare Newtonian value. This is a consistency check on the model, confirming that the memory effects encoded in the bath do not alter the response at asymptotically high frequencies. The theorem is proved in the machine-checked library of formal theorems, meaning the argument is verified by a computer to be logically valid from the stated definitions.

What the theorem does not claim is broader. It does not establish that the Caldeira-Leggett model correctly describes gravity in any regime; the formalization provides the structure and definitions, but the full derivation showing that integrating out the bath gives the claimed transfer function is left pending. The theorem also does not apply to any other response function beyond the specific single-pole form defined in the module. It is a statement about a particular mathematical model, not about the physical world.

THEOREM response_limit_high_freq · IndisputableMonolith/Gravity/CaldeiraLeggett.lean
response_limit_high_freq · IndisputableMonolith/Gravity/CaldeiraLeggett.lean:115 
/-- 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
THEOREM response_at_zero · IndisputableMonolith/Gravity/CaldeiraLeggett.lean
response_at_zero · IndisputableMonolith/Gravity/CaldeiraLeggett.lean:109 
/-- 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
THEOREM response_limit_high_freq · IndisputableMonolith/Gravity/CaldeiraLeggett.lean
response_limit_high_freq · IndisputableMonolith/Gravity/CaldeiraLeggett.lean:115 
/-- 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

What this page does not claim

The theorem does not prove that the Caldeira-Leggett model correctly describes gravity in any regime. The theorem does not apply to response functions other than the specific single-pole form defined in the module. The theorem does not establish the transfer function derivation from the action, which remains a placeholder.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND