Eq. (10): the singlet quartic coupling $h$ is non-decreasing under one-loop running

Proved

NewMinimalStandardModel.singlet_quartic_nondecreasing

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

mathematical-physicsoderenormalization-group

Let $a,b\in\mathbb R$ and let $h,k:\mathbb R\to\mathbb R$ . Suppose that at every $t\in[a,b]$ the function $h$ is differentiable with

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

the one-loop renormalization-group equation (10) for the singlet self-coupling $h$ , with $t=\log\mu$ and $k$ the Higgs–singlet coupling. Then $h$ is non-decreasing on $[a,b]$ .

This is the elementary fact behind the triviality bound on $h$ discussed with Fig. 1: the coupling can only grow with the renormalization scale.

Preamble

import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs

Formal statement

namespace NewMinimalStandardModel

theorem singlet_quartic_nondecreasing (h k : ℝ → ℝ) (a b : ℝ)
    (hODE : ∀ t ∈ Set.Icc a b,
      HasDerivAt h ((3 * h t ^ 2 + 12 * k t ^ 2) / (4 * Real.pi) ^ 2) t) :
    MonotoneOn h (Set.Icc a b) := 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

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 $a,b$ : if for every $t$ with $a\le t\le b$ the function $h$ has (two-sided) derivative at $t$ equal to $\frac{3h(t)^2+12k(t)^2}{(4\pi)^2}$ , then for all $s,t\in[a,b]$ with $s\le t$ one has $h(s)\le h(t)$ . No assumption is made on $k$ (not even continuity). If $a>b$ the interval is empty and the conclusion is vacuous.

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): the singlet quartic coupling hhh is non-decreasing under one-loop running

Eq. (10): the singlet quartic coupling $h$ is non-decreasing under one-loop running