IndisputableMonolith.Gravity.CausalKernelChain
This module supplies lemmas for finite-interval exponential integrals and constructs causal kernels including the Debye kernel and Laplace exponent to support response functions. Researchers working on dissipative dynamics or Recognition Science gravity models cite it for exact handling of transfer functions in the Caldeira-Leggett setting. The results follow from direct antiderivative evaluation together with norm and limit arguments drawn from Mathlib.
claimThe central identity is $∫_0^B e^{-a t} dt = (1 - e^{-a B})/a$ for $a ∈ ℂ$ and $B > 0$, stated via the form $t • (-a)$. The module also defines the Debye kernel, Laplace exponent, transfer function, and real-part response function.
background
The module extends the Caldeira-Leggett construction, which supplies a conservative action-based realization of causal-response dynamics for dissipative quantum systems. It introduces the exponential integral lemma in the convenient $t • (-a)$ form, together with norm bounds on $e^{-a t}$, tendsto statements at infinity, and algebraic identities for kernels. Notation follows standard complex analysis with $a$ complex and time intervals finite.
proof idea
This is a collection of lemmas and definitions rather than a single theorem. The integral identity is obtained by direct evaluation of the antiderivative; kernel and transfer-function relations follow from algebraic rearrangement and application of limit lemmas on the exponential.
why it matters in Recognition Science
The module supplies the causal-kernel layer required by higher gravity constructions in Recognition Science. It feeds the response-function machinery that supports the forcing chain (T5–T8) and the phi-ladder mass formulas by providing exact expressions for dissipative kernels.
scope and limits
- Does not derive the full Caldeira-Leggett action functional.
- Does not treat quantum-field or many-body extensions beyond the single-kernel case.
- Does not compute numerical values for constants such as alpha or G.
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