IndisputableMonolith.Gravity.CaldeiraLeggett
The CaldeiraLeggett module introduces the spectral density J(Ω) for an oscillator bath in the Recognition Science gravity setting. It requires J(Ω) ≥ 0 for all Ω > 0 to enforce passivity. Researchers deriving causal kernels or transfer functions cite this module as the spectral starting point. The module consists entirely of definitions and elementary non-negativity lemmas.
claimA spectral density function \(J(\Omega)\) for the oscillator bath satisfying \(J(\Omega) \geq 0\) for all \(\Omega > 0\) (passivity condition).
background
The module resides in the Gravity domain and imports the RS time quantum τ₀ = 1 tick from Constants. It defines SpectralDensity together with supporting objects such as debye_spectral, coupling_from_spectral, TransferFunction, response_function, and quadrature_function. These objects prepare the frequency-domain description of dissipation that the downstream CausalKernelChain module converts into time-domain exponential kernels.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Supplies the spectral-density object required by CausalKernelChain to formalize the single-timescale exponential memory kernel and its frequency-domain limits. The module therefore occupies the spectral half of the causal-kernel chain that connects the RS time quantum to response functions.
scope and limits
- Does not derive any explicit form of J from the J-uniqueness or phi-ladder constructions.
- Does not prove theorems; all content is definitional or elementary lemmas.
- Does not address spatial dimension D = 3 or the alpha band.
- Does not connect the bath to mass formulas or Berry creation thresholds.
used by (1)
depends on (1)
declarations in this module (12)
-
structure
SpectralDensity -
def
coupling_from_spectral -
def
debye_spectral -
lemma
debye_spectral_nonneg -
def
debye_density -
structure
TransferFunction -
def
response_function -
def
quadrature_function -
theorem
response_at_zero -
theorem
response_limit_high_freq -
theorem
response_enhancement -
theorem
cl_action_gives_transfer_function