Eq. (49) solves Eq. (44):
ProvedAKR2008.hybrid_modeF_solves_eq44Throughout, 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 every real and every time with , the mode coefficient of Eq. (49) satisfies the mode form of Eq. (44),
Eq. (44), , is the Riccati equation for the kernel of the classical Hamilton–Jacobi functional ; it is independent of and therefore also holds in the interacting solution of Sec. IV B.
Formalization Note The time derivative is taken with deriv; the hypothesis excludes the poles of .
import Mathlib import Definitions.Def_AKR2008_HybridDefs
namespace AKR2008
theorem hybrid_modeF_solves_eq44 (k t : ℝ) (hcos : Real.cos (k * t) ≠ 0) :
deriv (fun s => hybridModeF k s) t + hybridModeF k t ^ 2 + k ^ 2 = 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 numbers and such that :
No other hypotheses; is allowed (then and every term is ).