Sec. IV A: the kernels (49)–(51), (54), (55) solve the non-interacting equations (44)–(48)

Proved

AKR2008.hybrid_noninteracting_mode_solution

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

mathematical-physicsquantum-gravity

Consider the non-interacting ( $g=0$ ) two-dimensional Nordström model with a quantized massive scalar field of mass $m$ , in the configuration-space-ensemble description of Sec. IV A, with the Gaussian ansatz for $S^c$ , $P^c$ , $P^q$ . Throughout, kernels of Sec. IV A are written in the real orthonormal eigenbasis $f^{(k)}$ of $-\partial_x^2$ (eigenvalue $k^2$ ): a kernel $A_{xy}=\sum_k A_k f^{(k)}_x f^{(k)}_y$ is represented by its mode coefficient $A_k$ , so $\int dx\,A_{yx}B_{xz}\mapsto A_kB_k$ , $\partial_z^2\delta(y-z)\mapsto -k^2$ and $\int dx\,A_{xx}\mapsto\sum_k A_k$ .

Let $\{k_i\}_{i\in\iota}$ be a finite family of mode wave numbers, $\tau_i, w_i$ arbitrary real constants, and $t$ a time with $\cos(k_it)\ne0$ for all $i$ . Put $F_i(t)=-k_i\tan(k_it)$ , $G_i=\sqrt{k_i^2+m^2}$ , $K_i(t)=\tau_i/\cos^2(k_it)$ , $\beta_i(t)=w_i\cos(k_it)$ and $N^c(t)=1/\prod_i\cos(k_it)$ . Then at time $t$ :

Eq. (44): $\dot F_i + F_i^2 + k_i^2 = 0$ for every $i$ ;
Eq. (45): $-G_i^2 + (k_i^2+m^2) = 0$ for every $i$ ;
Eq. (46):

\frac{\dot N^c}{N^c} - \frac12\,\frac{d}{dt}\Bigl(\sum_i \beta_i K_i \beta_i\Bigr) + \sum_i F_i = 0;

Eq. (47): $\dfrac{d}{dt}(\beta_iK_i) + \beta_iK_iF_i = 0$ for every $i$ ;
Eq. (48): $-\tfrac12\dot K_i - K_iF_i = 0$ for every $i$ .

This is the paper's explicit solution of the uncoupled classical-quantum system: the classical gravitational-wave sector is a field-theoretic analogue of a classical oscillator ensemble, and the quantum sector is a one-particle Schrödinger wave functional. It is the $g=0$ starting point of the first-order hybrid solution of Sec. IV B.

Formalization Note The kernel equations are stated mode by mode in the eigenbasis, and the family of modes is finite (a truncation). Eq. (43), which involves the divergent zero-point term $\int dx\,G_{xx}$ , and Eq. (53) are not part of this statement.

Preamble

import Mathlib
import Definitions.Def_AKR2008_HybridDefs

Formal statement

namespace AKR2008

theorem hybrid_noninteracting_mode_solution {ι : Type*} [Fintype ι] (k τ w : ι → ℝ) (m t : ℝ)
    (hcos : ∀ i, Real.cos (k i * t) ≠ 0) :
    (∀ i, deriv (fun s => hybridModeF (k i) s) t + hybridModeF (k i) t ^ 2 + k i ^ 2 = 0) ∧
    (∀ i, -hybridModeG m (k i) ^ 2 + (k i ^ 2 + m ^ 2) = 0) ∧
    (deriv (fun s => hybridNc k s) t / hybridNc k t
        - (1 / 2) * deriv (fun s => ∑ i, hybridModeBeta (w i) (k i) s *
            hybridModeK (τ i) (k i) s * hybridModeBeta (w i) (k i) s) t
        + ∑ i, hybridModeF (k i) t = 0) ∧
    (∀ i, deriv (fun s => hybridModeBeta (w i) (k i) s * hybridModeK (τ i) (k i) s) t
        + hybridModeBeta (w i) (k i) t * hybridModeK (τ i) (k i) t * hybridModeF (k i) t = 0) ∧
    (∀ i, -(1 / 2) * deriv (fun s => hybridModeK (τ i) (k i) s) t
        - hybridModeK (τ i) (k i) t * hybridModeF (k i) t = 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-10, Sec. IV A, Eqs. (44)–(51), (54), (55)

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 every finite type $\iota$ , all real families $k=(k_i)_{i\in\iota}$ , $\tau=(\tau_i)$ , $w=(w_i)$ , all real $m$ and $t$ , assuming $\cos(k_it)\ne0$ for every $i\in\iota$ , the following five statements hold simultaneously (with $F$ , $G$ , $K$ , $\beta$ , $N^c$ the functions $\mathrm{hybridModeF}$ , $\mathrm{hybridModeG}$ , $\mathrm{hybridModeK}$ , $\mathrm{hybridModeBeta}$ , $\mathrm{hybridNc}$ defined as $-k\tan(kt)$ , $\sqrt{k^2+m^2}$ , $\tau_k/\cos^2(kt)$ , $w_k\cos(kt)$ , $1/\prod_i\cos(k_it)$ ):

for all $i$ : $\frac{d}{ds}\bigl[-k_i\tan(k_is)\bigr]_{s=t} + k_i^2\tan^2(k_it) + k_i^2 = 0$ ;
for all $i$ : $-\bigl(\sqrt{k_i^2+m^2}\bigr)^2 + (k_i^2+m^2) = 0$ ;
$\dfrac{(N^c)'(t)}{N^c(t)} - \dfrac12\,\dfrac{d}{ds}\Bigl[\sum_i \beta_i(s)K_i(s)\beta_i(s)\Bigr]_{s=t} + \sum_i F_i(t) = 0$ , where $\beta_i(s)=w_i\cos(k_is)$ , $K_i(s)=\tau_i/\cos^2(k_is)$ ;
for all $i$ : $\frac{d}{ds}\bigl[\beta_i(s)K_i(s)\bigr]_{s=t} + \beta_i(t)K_i(t)F_i(t) = 0$ ;
for all $i$ : $-\tfrac12\,K_i'(t) - K_i(t)F_i(t) = 0$ .

Derivatives are Lean's deriv (which is $0$ at points of non-differentiability; under the cosine hypothesis all functions involved are differentiable at $t$ ). The index type may be empty, in which case the three "for all $i$ " clauses are vacuous and clause 3 reads $0/1 - 0 + 0 = 0$ . There are no sign or positivity assumptions on $k_i$ , $m$ , $\tau_i$ , $w_i$ ; $k_i=0$ is 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