Encyclopedia Gravity Gravity Causal Kernel Chain

ARTICLE 4 claims 3 theorems 1 model

Gravity Causal Kernel Chain

The gravity causal kernel chain formalizes a single-timescale exponential memory kernel and proves its frequency-domain limits.

Verify this page

Causal kernel chain

The gravity causal kernel chain is the sequence of results that starts with a time-domain exponential memory kernel, derives its complex transfer function, and proves the two frequency limits that connect to steady-state and Newtonian responses. In Recognition Science, gravity is not a force field but a recognition ledger, and the kernel is the memory of that ledger. The chain is formalized in the kernel-checked library 4 in CausalKernelChain.the kernel-checked library, a module that treats the simplest possible memory: a single relaxation time, the Debye or single-pole response.

The module defines the Debye kernel as an exponential decay, Γ(t) = (Δ/τ) e−t/τ for t ≥ 0, where Δ is the coupling strength and τ the relaxation time. It then defines the truncated frequency response as the integral of this kernel against e−iωt over [0, B]. The central theorem, kernel_response_limit, proves that as the horizon B goes to infinity, this truncated response converges to the closed form Δ / (1 + iωτ). This is the Laplace transform limit that bridges the time-domain kernel to the frequency domain.

The chain continues by showing that the complex transfer function, defined as 1 + Δ / (1 + iωτ), is exactly the limit of the kernel response plus one. A further theorem, response_function_is_real_part, proves that the real-valued response function used in the Caldeira–Leggett model is precisely the real part of this complex transfer function. These two theorems together establish the full bridge: the exponential kernel, its infinite-horizon transform, and the transfer function are all one coherent object, not separate assumptions.

The module also proves the two physical limits. As ω → 0, the response approaches the steady-state value 1 + Δ, the static susceptibility. As ω → ∞, the response tends to 1, the Newtonian limit where the kernel's memory is irrelevant. These limits are consequences of the established closed form, not additional postulates. The chain is the Debye realization only; the source allows broader spectral densities, but those require further Fourier and Laplace machinery that is not yet formalized.

THEOREM kernel_response_limit · IndisputableMonolith/Gravity/CausalKernelChain.lean
kernel_response_limit · IndisputableMonolith/Gravity/CausalKernelChain.lean:168 
/-- Truncated Debye-kernel response tends to its closed form as `B → ∞`. -/
theorem kernel_response_limit (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
    Filter.Tendsto (fun B => kernel_response_trunc H ω B) Filter.atTop
      (nhds ((H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)))) := by
  -- Abbreviate `a = (1/τ) + iω`.
  set a : ℂ := laplaceExponent H ω with ha_def

  have ha_re : 0 < a.re := by
    have h : 0 < (1 / H.τ) := one_div_pos.2 H.τ_pos
    -- `a.re = 1/τ` since `Re(iω)=0`.
    simpa [ha_def, laplaceExponent] using h

  have ha : a ≠ 0 := by
    have hne : a.re ≠ 0 := ne_of_gt ha_re
    intro h0
    apply hne
    simpa [h0]

  -- Closed form for each truncation bound `B`.
  have hclosed (B : ℝ) :
      kernel_response_trunc H ω B =
        (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹) := by
    -- Rewrite the integrand into the `exp (t • (-a))` shape and apply `integral_exp_smul_neg`.
    unfold kernel_response_trunc
    -- Push the real kernel into `ℂ`, and turn `Real.exp` into `Complex.exp`.
    simp_rw [debye_kernel]
    simp_rw [Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_exp]
    -- Combine the two exponentials.
    simp_rw [← Complex.exp_add, ← mul_assoc, ← mul_left_comm, ← mul_comm]
    -- Pull out the constant factor and evaluate the remaining exponential integral.
    -- (At this point the integrand is exactly `exp (t • (-a))` after simp.)
    simp [ha_def, laplaceExponent, Complex.real_smul, intervalIntegral.integral_const_mul,
      integral_exp_smul_neg a ha B, mul_assoc, mul_left_comm, mul_comm, add_assoc, add_left_comm,
      add_comm]

  -- Reduce to the closed form and take `B → ∞`.
  have hExp :
      Filter.Tendsto (fun B : ℝ => Complex.exp (B • (-a))) Filter.atTop (nhds (0 : ℂ)) := by
    -- `B • (-a) = -((B:ℂ) * a)`, and `Re(a) > 0`.
    have :=
      tendsto_exp_neg_mul_ofReal_atTop a ha_re
    simpa [Complex.real_smul, mul_assoc, mul_left_comm, mul_comm] using this

  have hExpSub :
      Filter.Tendsto (fun B : ℝ => Complex.exp (B • (-a)) - (1 : ℂ)) Filter.atTop (nhds (-1 : ℂ)) :=
    (hExp.sub tendsto_const_nhds)

  have hExpMul :
      Filter.Tendsto (fun B : ℝ => (Complex.exp (B • (-a)) - (1 : ℂ)) * (-a)⁻¹) Filter.atTop
        (nhds ((-1 : ℂ) * (-a)⁻¹)) :=
    (Filter.Tendsto.mul_const (-a)⁻¹ hExpSub)

  have hMain :
      Filter.Tendsto (fun B : ℝ => (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹))
        Filter.atTop (nhds ((H.Δ / H.τ : ℂ) * ((-1 : ℂ) * (-a)⁻¹))) :=
    (Filter.Tendsto.const_mul (H.Δ / H.τ : ℂ) hExpMul)

  -- Rewrite the limit into the desired `Δ / (1 + iωτ)` form.
  have hlim_simplify :
      (H.Δ / H.τ : ℂ) * ((-1 : ℂ) * (-a)⁻¹) =
        (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
    -- `(-1) * (-a)⁻¹ = a⁻¹`, then regroup as a division by `τ*a = 1 + iωτ`.
    have : ((-1 : ℂ) * (-a)⁻¹) = a⁻¹ := by
      -- `(-a)⁻¹ = -(a⁻¹)`
      simp
    -- Rewrite `(Δ/τ) * a⁻¹` as `Δ / (τ * a)`, and compute `τ * a`.
    -- Use `ha_def` to expand `a = (1/τ) + iω`.
    -- `τ * ((1/τ) + iω) = 1 + iωτ`.
    -- Finally, cast `Δ/τ` into `ℂ` consistently.
    simp [this, ha_def, laplaceExponent, div_div, div_eq_mul_inv, mul_add, add_mul,
      mul_assoc, mul_left_comm, mul_comm]

  -- Assemble the tendsto statement.
  have hMain' :
      Filter.Tendsto (fun B : ℝ => kernel_response_trunc H ω B) Filter.atTop
        (nhds ((H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)))) := by
    -- Rewrite by the pointwise closed form, then apply `hMain`.
    have hcongr :
        (fun B : ℝ => kernel_response_trunc H ω B) =
          fun B : ℝ => (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹) := by
      funext B
      simpa [hclosed B]
    -- Transfer the limit.
    simpa [hcongr, hlim_simplify] using hMain

  exact hMain'
THEOREM response_function_is_real_part · IndisputableMonolith/Gravity/CausalKernelChain.lean
response_function_is_real_part · IndisputableMonolith/Gravity/CausalKernelChain.lean:263 
/-- The paper’s real-valued response function is the real part of the complex transfer function. -/
theorem response_function_is_real_part (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
    CaldeiraLeggett.response_function H ω = (transfer_function_complex H ω).re := by
  -- Unfold both sides.
  unfold CaldeiraLeggett.response_function transfer_function_complex
  -- Let the complex denominator be `w = 1 + i ω τ`.
  set w : ℂ := (1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ) with hw
  have wre : w.re = 1 := by
    -- `Re(i * real) = 0`.
    simp [hw, mul_assoc, mul_left_comm, mul_comm]
  have wnormSq : Complex.normSq w = 1 + (ω * H.τ) ^ (2 : ℕ) := by
    -- `normSq w = w.re^2 + w.im^2`, and here `w.re = 1`, `w.im = ωτ`.
    -- We compute directly using `normSq_apply`.
    have : w.im = ω * H.τ := by
      simp [hw, mul_assoc, mul_left_comm, mul_comm]
    -- Expand `normSq` and simplify.
    -- Use `pow_two` (as `x^2 = x*x`) in the reverse direction.
    calc
      Complex.normSq w = w.re * w.re + w.im * w.im := by
        simpa [Complex.normSq_apply]
      _ = (1 : ℝ) * 1 + (ω * H.τ) * (ω * H.τ) := by
        simp [wre, this]
      _ = 1 + (ω * H.τ) ^ (2 : ℕ) := by
        simp [pow_two, mul_assoc]

  -- Reduce the real part using `Complex.div_re`.
  -- Since `H.Δ` is real, its imaginary part is 0.
  have hdiv :
      ((H.Δ : ℂ) / w).re = H.Δ / (1 + (ω * H.τ) ^ (2 : ℕ)) := by
    -- Apply `div_re` and simplify with `wre` and `wnormSq`.
    simp [Complex.div_re, wre, wnormSq, hw, mul_assoc, mul_left_comm, mul_comm, add_assoc,
      add_left_comm, add_comm]

  -- Finish: real part of `1 + z` is `1 + Re(z)`.
  -- Note: `simp` can unfold `.re` of addition definitionaly once `hdiv` is in place.
  -- We rewrite the divisor `w` back into the original denominator.
  simp [hw, hdiv, Complex.add_re]
MODEL debye_kernel · IndisputableMonolith/Gravity/CausalKernelChain.lean
debye_kernel · IndisputableMonolith/Gravity/CausalKernelChain.lean:131 
/-- The Debye exponential kernel for a single-timescale response:
\[
\Gamma(t) = \frac{\Delta}{\tau} e^{-t/\tau},\quad t \ge 0.
\]
We treat it as a function on `ℝ` and integrate it on `[0,B]` (then take `B → ∞`). -/
def debye_kernel (H : CaldeiraLeggett.TransferFunction) (t : ℝ) : ℝ :=
  (H.Δ / H.τ) * Real.exp (-t / H.τ)
THEOREM transfer_function_eq_one_plus_kernel · IndisputableMonolith/Gravity/CausalKernelChain.lean
transfer_function_eq_one_plus_kernel · IndisputableMonolith/Gravity/CausalKernelChain.lean:256 
/-- `transfer_function_complex` is exactly the Debye single-pole transfer function form. -/
theorem transfer_function_eq_one_plus_kernel (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
    transfer_function_complex H ω =
      (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
  simp [transfer_function_complex]

What this page does not claim

This answer does not claim the kernel chain is the full derivation of gravity. This answer does not claim the module formalizes spectral densities beyond the Debye single-pole case. This answer does not claim the Newtonian limit is derived as a separate postulate; it is a consequence of the established closed form.

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/CausalKernelChain.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