transfer_function_eq_one_plus_kernel
The equality shows that the complex transfer function for a Caldeira-Leggett system equipped with the Debye exponential kernel equals one plus the single-pole term involving damping Delta and relaxation time tau. Researchers working on frequency-domain responses in dissipative models would cite this when converting between time-domain kernels and steady-state limits. The proof reduces immediately by simplification on the definition of the complex transfer function.
claimLet $H$ be a Caldeira-Leggett transfer function with damping parameter $Delta$ and relaxation time $tau$. For real frequency $omega$, the complex transfer function satisfies $H(i omega) = 1 + Delta / (1 + i omega tau)$.
background
The module develops the causal-kernel chain that begins with a time-domain exponential memory kernel and passes to its frequency response. The Debye realization is the single-timescale case whose Laplace transform produces one pole; the module goal is to obtain the transfer function, its real part, and the omega to 0 and omega to infinity limits. Upstream, the cost algebra supplies the shifted function H(x) = J(x) + 1 that converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The proof is a one-line wrapper that applies the simp tactic to unfold the definition of transfer_function_complex.
why it matters in Recognition Science
The identity supplies the explicit frequency-domain form of the Debye kernel inside the causal-kernel chain, directly enabling the subsequent real-part response function. It realizes the single-pole case required by the Recognition Science treatment of memory kernels, consistent with the phi-ladder and eight-tick octave structures. No downstream theorems are yet recorded, leaving the Newtonian and steady-state limits as immediate next steps.
scope and limits
- Does not treat continuous spectral densities or multi-pole kernels.
- Does not derive Delta or tau from the phi-forcing chain.
- Does not address non-causal or acausal response functions.
formal statement (Lean)
257theorem transfer_function_eq_one_plus_kernel (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
258 transfer_function_complex H ω =
259 (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
proof body
Term-mode proof.
260 simp [transfer_function_complex]
261
262
263/-- The paper’s real-valued response function is the real part of the complex transfer function. -/