Appendix A: $S_{\mathrm{osc}}$ solves the oscillator Hamilton–Jacobi equation

Proved

AKR2008.osc_HJ_solution

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-gravity

Let $\omega$ be a real frequency and $S_{\mathrm{osc}}(x,t)=-\dfrac{\omega x^2}{2}\tan(\omega t)$ . For every $x$ and every $t$ with $\cos(\omega t)\ne0$ ,

\dot S_{\mathrm{osc}} + \frac12\Bigl(\frac{\partial S_{\mathrm{osc}}}{\partial x}\Bigr)^2 + \frac12\,\omega^2x^2 = 0 .

This is the Hamilton–Jacobi equation of the unit-mass one-dimensional harmonic oscillator; its solution is the single-mode analogue of the classical functional $S^c[\phi,t]=-\sum_k\frac{ka_k^2}{2}\tan(kt)$ of Sec. IV.

Preamble

import Mathlib
import Definitions.Def_AKR2008_HybridDefs

Formal statement

namespace AKR2008

theorem osc_HJ_solution (ω x t : ℝ) (hcos : Real.cos (ω * t) ≠ 0) :
    deriv (fun s => oscS ω x s) t + (1 / 2) * (deriv (fun y => oscS ω y t) x) ^ 2
      + (1 / 2) * ω ^ 2 * x ^ 2 = 0 := by sorry

end AKR2008

Source

M. Albers, C. Kiefer, M. Reginatto, Measurement analysis and quantum gravity, Phys. Rev. D 78, 064051 (2008), https://doi.org/10.1103/PhysRevD.78.064051, p. 064051-14, Appendix A

Read-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 $\omega,x,t$ with $\cos(\omega t)\ne0$ , writing $S(x,t)=-(\omega x^2/2)\tan(\omega t)$ :

\frac{\partial S}{\partial t}(x,t) + \frac12\Bigl(\frac{\partial S}{\partial x}(x,t)\Bigr)^2 + \frac12\,\omega^2x^2 = 0,

where each partial derivative is the one-variable deriv of $S$ in that variable with the other held fixed. No other hypotheses ( $\omega=0$ allowed).

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Appendix A: SoscS_{\mathrm{osc}}Sosc​ solves the oscillator Hamilton–Jacobi equation

Appendix A: $S_{\mathrm{osc}}$ solves the oscillator Hamilton–Jacobi equation