IndisputableMonolith.Gravity.CausalKernelChain
This module supplies the finite-interval complex exponential integral and derived causal kernels for response functions in dissipative dynamics. Gravity modelers cite it for explicit transfer functions and Debye kernels built on the Caldeira-Leggett action. The module consists of direct integral evaluations plus supporting limit and norm lemmas, each reduced via Mathlib exponential integral rules.
claimThe central identity is $\int_0^B e^{-a t}\,dt = \frac{1-e^{-aB}}{a}$ for real $t$ and complex $a$, together with the objects $\mathrm{debye\_kernel}$, $\mathrm{kernel\_response\_trunc}$, $\mathrm{laplaceExponent}$, and $\mathrm{transfer\_function\_complex}$.
background
The module extends the Caldeira-Leggett construction, which formalizes dissipative quantum systems via a conservative action-based realization of causal-response dynamics. It introduces the finite-interval integral in the $t\bullet(-a)$ form and defines the Laplace exponent, Debye kernel, truncated kernel response, and complex transfer function. These sit inside the Gravity domain and rely on the upstream Caldeira-Leggett module for the underlying action formalism.
proof idea
The module is a collection of lemmas and definitions. The integral identity is proved by direct evaluation of the exponential antiderivative; subsequent lemmas on norms, limits at infinity, and transfer-function identities apply standard Mathlib continuity and integral tactics to the same exponential form.
why it matters in Recognition Science
The module supplies the explicit causal-response kernels required by gravity models that descend from the Caldeira-Leggett action. It provides the concrete integral and truncation machinery that higher-level gravity theorems invoke for response functions, closing the chain from the action to observable kernels.
scope and limits
- Does not treat infinite-time kernels without explicit truncation.
- Does not incorporate non-Markovian memory kernels beyond the exponential form.
- Does not address quantization of the kernel itself.
depends on (1)
declarations in this module (10)
-
theorem
integral_exp_smul_neg -
lemma
norm_exp_neg_mul_ofReal -
theorem
tendsto_exp_neg_mul_ofReal_atTop -
def
transfer_function_complex -
def
debye_kernel -
def
kernel_response_trunc -
def
laplaceExponent -
theorem
kernel_response_limit -
theorem
transfer_function_eq_one_plus_kernel -
theorem
response_function_is_real_part