Eq. (10): a positive singlet quartic coupling reaches a Landau pole within $\Delta t \le 16\pi^2/(3h(t_0))$

Proved

NewMinimalStandardModel.singlet_quartic_landau_pole

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsoderenormalization-group

Let $h,k:\mathbb R\to\mathbb R$ and $t_0, T\in\mathbb R$ . Suppose that $h$ solves the one-loop equation (10),

(4\pi)^2\frac{dh}{dt}(t) = 3h(t)^2 + 12k(t)^2,

at every $t\in[t_0,T)$ , and that $h(t_0)>0$ . Then

T \le t_0 + \frac{16\pi^2}{3\,h(t_0)} .

In words: a solution starting from a positive value cannot remain finite for more than $\frac{16\pi^2}{3h(t_0)}$ units of $t=\log\mu$ . This quantifies why large $h(m_Z)$ is excluded by the triviality bound (the allowed region in Fig. 1 disappears for $h(m_Z)\gtrsim1.3$ ).

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem singlet_quartic_landau_pole (h k : ℝ → ℝ) (t₀ T : ℝ)
    (hODE : ∀ t ∈ Set.Ico t₀ T,
      HasDerivAt h ((3 * h t ^ 2 + 12 * k t ^ 2) / (4 * Real.pi) ^ 2) t)
    (h₀ : 0 < h t₀) :
    T ≤ t₀ + 16 * Real.pi ^ 2 / (3 * h t₀) := by sorry

end NewMinimalStandardModel

Source

H. Davoudiasl, R. Kitano, T. Li, H. Murayama, The new Minimal Standard Model, Phys. Lett. B 609 (2005) 117-123, https://doi.org/10.1016/j.physletb.2005.01.026, Eq. (10), p. 121 (triviality bound, Fig. 1)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent that drafted the statements; NON-BLIND, not an independent auditor

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor and must not be treated as independent evidence of faithfulness. Reviewers should compare the Lean code against the source themselves.

For all functions $h,k:\mathbb R\to\mathbb R$ and reals $t_0, T$ : if for every $t$ with $t_0\le t<T$ the function $h$ has (two-sided) derivative at $t$ equal to $\frac{3h(t)^2+12k(t)^2}{(4\pi)^2}$ , and $h(t_0)>0$ , then $T\le t_0+\frac{16\pi^2}{3h(t_0)}$ . No assumption is made on $k$ . If $T\le t_0$ the derivative hypothesis is vacuous and the conclusion holds trivially since the right-hand side exceeds $t_0$ .

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

Eq. (10): a positive singlet quartic coupling reaches a Landau pole within Δt≤16π2/(3h(t0))\Delta t \le 16\pi^2/(3h(t_0))Δt≤16π2/(3h(t0​))

Eq. (10): a positive singlet quartic coupling reaches a Landau pole within $\Delta t \le 16\pi^2/(3h(t_0))$