response_limit_high_freq
The real part of a single-pole Caldeira-Leggett transfer function tends to 1 as frequency tends to infinity. Gravitational modelers using frequency-dependent potentials cite the result to recover the Newtonian ultraviolet limit. The tactic proof chains standard Filter.Tendsto facts on polynomial growth, monotonicity, and inversion to show the correction term vanishes.
claimLet $H$ be a transfer function with nonzero DC enhancement $Δ$. Then the real response $C(ω) = 1 + Δ / (1 + (ω τ)^2)$ satisfies $lim_{ω→+∞} C(ω) = 1$.
background
The Caldeira-Leggett module adapts the bath-of-oscillators construction to gravity, producing a frequency-dependent response after the bath is traced out. A TransferFunction is the structure carrying real parameters Δ (DC enhancement, w-1) and τ > 0 (memory timescale), with response_function defined as the real part 1 + Δ / (1 + (ω τ)^2). The module supplies the action integral that couples the baryon potential to the bath via spectral density J(Ω) ≥ 0 and states that the single-pole form arises from exponential memory. Upstream results from CostAlgebra supply the shifted cost H(x) = J(x) + 1 that converts the Recognition Composition Law into the d'Alembert equation, although the present argument uses only real-analysis limit lemmas.
proof idea
The tactic proof unfolds response_function and builds a chain of Filter.Tendsto statements. It shows ω τ tends to infinity, raises the result to the second power, adds 1 while preserving the limit via eventual monotonicity, takes the reciprocal to reach zero, multiplies by the constant Δ, and finally adds the constant 1. Each step applies simpa, tendsto_atTop_mono', or tendsto_const_nhds together with linarith.
why it matters in Recognition Science
This theorem verifies the high-frequency Newtonian limit inside the gravitational Caldeira-Leggett realization, confirming that the effective response recovers the constant 1 at short distances. It fills the ultraviolet end of the single-pole transfer function described in the module documentation and supports the broader program of obtaining classical gravity from the Recognition functional equation. No downstream theorems are recorded yet.
scope and limits
- Does not derive the single-pole form of the transfer function from the action integral.
- Does not treat the imaginary part or full complex response.
- Does not connect to the phi-ladder, mass formulas, or T0-T8 chain of the core framework.
- Does not address stability, positivity, or fluctuation-dissipation constraints beyond the given hypotheses.
formal statement (Lean)
116theorem response_limit_high_freq (H : TransferFunction) (hΔ : H.Δ ≠ 0) :
117 Filter.Tendsto (response_function H) Filter.atTop (nhds 1) := by
proof body
Tactic-mode proof.
118 -- As ω → ∞, Δ/(1 + (ωτ)²) → 0
119 unfold response_function
120 -- Show the denominator tends to `+∞` as ω → +∞.
121 have hmul : Filter.Tendsto (fun ω : ℝ => ω * H.τ) Filter.atTop Filter.atTop := by
122 simpa using ((Filter.tendsto_id).atTop_mul_const H.τ_pos)
123 have hsq : Filter.Tendsto (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ)) Filter.atTop Filter.atTop :=
124 (Filter.tendsto_pow_atTop (α := ℝ) (n := 2) (by decide)).comp hmul
125 have hmono :
126 (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ))
127 ≤ᶠ[Filter.atTop] (fun ω : ℝ => 1 + (ω * H.τ) ^ (2 : ℕ)) :=
128 Filter.Eventually.of_forall (fun _ω => by linarith)
129 have hden :
130 Filter.Tendsto (fun ω : ℝ => 1 + (ω * H.τ) ^ (2 : ℕ)) Filter.atTop Filter.atTop :=
131 Filter.tendsto_atTop_mono' Filter.atTop hmono hsq
132
133 have hinv :
134 Filter.Tendsto (fun ω : ℝ => (1 + (ω * H.τ) ^ (2 : ℕ))⁻¹) Filter.atTop (nhds 0) :=
135 (tendsto_inv_atTop_zero).comp hden
136
137 have hfrac_mul :
138 Filter.Tendsto (fun ω : ℝ => H.Δ * (1 + (ω * H.τ) ^ (2 : ℕ))⁻¹) Filter.atTop (nhds 0) := by
139 have hΔconst : Filter.Tendsto (fun _ω : ℝ => H.Δ) Filter.atTop (nhds H.Δ) := by
140 simpa using (tendsto_const_nhds : Filter.Tendsto (fun _ω : ℝ => H.Δ) Filter.atTop (nhds H.Δ))
141 -- H.Δ * (denom)⁻¹ → H.Δ * 0 = 0
142 simpa using (hΔconst.mul hinv)
143
144 have hfrac :
145 Filter.Tendsto (fun ω : ℝ => H.Δ / (1 + (ω * H.τ) ^ (2 : ℕ))) Filter.atTop (nhds 0) := by
146 simpa [div_eq_mul_inv] using hfrac_mul
147
148 -- Add back the constant `1`.
149 have hone : Filter.Tendsto (fun _ω : ℝ => (1 : ℝ)) Filter.atTop (nhds 1) := by
150 simpa using (tendsto_const_nhds : Filter.Tendsto (fun _ω : ℝ => (1 : ℝ)) Filter.atTop (nhds 1))
151 simpa using hone.add hfrac
152
153/-- Passivity (enhancement, not suppression): if \(\Delta > 0\), then \(C(\omega) > 1\). -/