Eq. (54) solves Eq. (47):
ProvedAKR2008.hybrid_modeBeta_solves_eq47Throughout, kernels of Sec. IV A are written in the real orthonormal eigenbasis of (eigenvalue ): a kernel is represented by its mode coefficient , so , and .
For all real and every time with , the coefficients (Eq. (54)), (Eq. (51)) and (Eq. (49)) satisfy the mode form of Eq. (47),
Eq. (47) fixes the centre of the classical Gaussian ensemble ; the solution oscillates like the mean position of a classical oscillator.
import Mathlib import Definitions.Def_AKR2008_HybridDefs
namespace AKR2008
theorem hybrid_modeBeta_solves_eq47 (wk τk k t : ℝ) (hcos : Real.cos (k * t) ≠ 0) :
deriv (fun s => hybridModeBeta wk k s * hybridModeK τk k s) t
+ hybridModeBeta wk k t * hybridModeK τk k t * hybridModeF k t = 0 := by sorry
end AKR2008Read-back
What the Lean code literally says, in plain math · Aristotle (Harmonic)
Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, not by a blind auditor with a fresh context. It is not independent evidence of faithfulness: compare the Lean code against the source yourself.
For all real with :
No other hypotheses.