SpectralDensity
plain-language theorem explainer
SpectralDensity packages a real-valued function J with the single constraint that J remains non-negative for all positive frequencies. Workers adapting the Caldeira-Leggett bath model to gravitational actions cite it to guarantee passivity of the oscillator modes. The declaration is a bare structure definition carrying no computational reduction or lemma applications.
Claim. A spectral density is a function $J : ℝ → ℝ$ such that $J(ω) ≥ 0$ for every $ω > 0$.
background
The Caldeira-Leggett module formalizes an action for dissipative gravitational dynamics by coupling a baryon potential to a continuum of harmonic oscillators. The action integral contains the bath term ∫ dΩ ½(ẋ_Ω² − Ω² x_Ω²) together with the interaction X ∫ c(Ω) x_Ω dΩ. The spectral density is introduced via the standard relation J(Ω) = (π/2) c(Ω)² / Ω and is required to be non-negative for Ω > 0 to enforce passivity.
proof idea
Direct structure definition. The two fields are declared explicitly; the nonneg field records the inequality ∀ ω, 0 < ω → 0 ≤ J ω with no further reduction or tactic steps.
why it matters
The structure supplies the carrier type instantiated by debye_density to produce a concrete non-negative J. It therefore anchors the transfer-function constructions that realize causal response in the gravitational Caldeira-Leggett setting. The module status records that full proofs of the integrated transfer function remain pending.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.