debye_density
plain-language theorem explainer
The definition constructs a SpectralDensity instance for the Debye oscillator bath in the Caldeira-Leggett model, taking positive real parameters lambda and gamma to set the spectral function J. Gravitational modelers adapting dissipative dynamics would cite this when specifying the bath spectrum for damping calculations. It is realized as a direct structure constructor that supplies the spectral function and invokes the nonnegativity property.
Claim. Let $0 < lambda$ and $0 < gamma$. The Debye density is the spectral density structure whose frequency response $J(Omega)$ is the Debye form for these parameters and satisfies $J(Omega) >= 0$ for all $Omega > 0$.
background
The Caldeira-Leggett module formalizes an action for a system coordinate coupled to a bath of harmonic oscillators, with the spectral density $J(Omega)$ encoding coupling strengths via $J(Omega) = pi/2 c(Omega)^2 / Omega$. The SpectralDensity structure requires a function $J : R to R$ together with a proof that $J(omega) >= 0$ for $omega > 0$, enforcing bath passivity. The module adapts this construction to gravity by inserting the bath term into the action integral alongside the gravitational potential gradient.
proof idea
The definition is a one-line wrapper that applies the Debye spectral function to populate the J field and invokes the nonnegativity lemma to discharge the structure obligation.
why it matters
This supplies the concrete bath spectrum for the gravitational Caldeira-Leggett action, supporting later transfer-function derivations with single-pole response. It fills the spectral-density slot in the module's conservative realization of causal dynamics, linking to the Recognition Science J-cost functional equation and forcing chain. The module status notes that full proofs of bath integration remain pending, so the definition closes the structure requirement while leaving dynamical equivalence open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.