laplaceExponent
plain-language theorem explainer
laplaceExponent supplies the complex exponent a = 1/τ + iω that locates the pole of the single-pole Debye response. Researchers deriving frequency-domain limits for causal memory kernels in gravitational models cite it when passing from the time-domain exponential kernel to its transfer function. The definition is realized by direct coercion of the real reciprocal timescale and frequency into the complex plane.
Claim. For a transfer function with memory timescale τ > 0, the Laplace exponent is the complex number a(ω) := 1/τ + iω.
background
The module develops the causal-kernel chain for the single-timescale exponential (Debye) memory kernel. Its TransferFunction structure packages a DC enhancement Δ together with a positive memory timescale τ; the associated frequency response takes the form 1 + Δ/(1 + iωτ). Upstream, CostAlgebra.H reparametrizes the Recognition cost J into H(x) = J(x) + 1, converting the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2H(x)H(y). The present definition isolates the complex quantity whose real part is the inverse timescale and whose imaginary part is the driving frequency.
proof idea
The definition is a one-line algebraic construction that coerces 1/τ into ℂ and adds iω.
why it matters
kernel_response_limit invokes laplaceExponent to abbreviate the pole location when proving that the truncated Debye response converges to its closed form Δ/(1 + iωτ) as the cutoff B tends to infinity. The definition therefore completes the frequency-domain half of the causal-kernel chain in the gravity module, connecting the time-domain exponential kernel to the steady-state and Newtonian limits required by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.