norm_exp_neg_mul_ofReal
plain-language theorem explainer
The lemma states that the modulus of exp(-(B a)) equals exp(-(B Re(a))) for complex a and real B. Analysts working on Debye kernels in causal gravity models cite this identity to reduce norm estimates in transfer-function limits. The proof computes the real part of the argument via direct expansion of complex multiplication and negation, then applies the standard modulus formula for complex exponentials.
Claim. For any complex number $a$ and real number $B$, $|e^{-B a}| = e^{-B Re(a)}$.
background
The declaration sits inside the CausalKernelChain module, which formalizes the single-timescale exponential memory kernel (Debye/single-pole response) together with its frequency-domain transfer function and the steady-state and Newtonian limits of the real part. The module works in the setting of causal kernels for gravity, restricting attention to the exponential case while leaving broader spectral densities for later Fourier machinery. It draws on the upstream identification in SimplicialLedger.ContinuumBridge.as, where the Laplacian action satisfies (1/2) Σ w_ij (ε_i - ε_j)^2 = (1/κ) Σ δ_h A_h with weights w_ij = A_ij / (κ vol_i).
proof idea
The tactic proof first obtains the auxiliary equality that the real part of -(B a) equals -(B Re(a)) by simp on the definitions of Complex.neg_re, Complex.mul_re, and the real/imaginary projections of ofReal. It then finishes with simpa using Complex.norm_exp together with the auxiliary real-part fact.
why it matters
The result supplies the norm identity required by the downstream theorem tendsto_exp_neg_mul_ofReal_atTop, which establishes that exp(-(B a)) tends to zero at infinity whenever Re(a) > 0. That limit in turn controls the decay properties of the exponential kernel inside the transfer-function chain. Within the Recognition framework the lemma therefore contributes the analytic step that lets the Debye response reach its Newtonian limit, consistent with the eight-tick octave structure and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.