Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2603.08139

Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature

Joseph Tooby-Smith
View original source ↗Read source document ↗Export metadata ↓

Abstract

In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (2HDM) potential. Twenty years on, it is now easier to apply the process of formalization into an interactive theorem prover to this work thanks to projects like Mathlib and Physlib (the latter formerly PhysLean and Lean-QuantumInfo), and to ask for a higher standard of mathematical correctness. Doing so has revealed an error in the arguments of this 2006 paper, invalidating their main theorem on the stability of the 2HDM potential. This case is noteworthy because to the best of our knowledge it is the first non-trivial error in a physics paper found through formalization. It was one of the first papers where formalization was attempted, which raises the uncomfortable question of how many physics papers would not pass this higher level of scrutiny.

Explore related subjects

hep-phcs.LOhep-th

Keep this discovery

BibTeXRIS

Joseph Tooby-Smith. 2026-03-09. Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. https://arxiv.org/abs/2603.08139

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Axionic Wormholes in Metric-Affine Gravity

The axion is a promising candidate for solving the strong CP problem. To solve this problem, the global U(1) symmetry must be preserved to a high degree of accuracy. However, it is well known that global symmetries are explicitly violated by quantum gravity effects, giving rise to what is referred to as the axion quality problem. In this paper, we investigate axionic wormholes as a source of explicit U(1) violation in Metric-Affine Gravity. This framework allows for spacetime torsion and non-metricity, which accommodate additional curvature-like and topological terms, such as the Holst and Nieh--Yan terms, that are absent from the metric and Palatini formalisms. We show that non-minimal couplings to these terms modify the wormhole dynamics and enhance the Euclidean wormhole action, thereby alleviating the axion quality problem. We also find that the viable parameter space is enlarged when two of these couplings are simultaneously present. We further identify representative parameter regions where the alleviation of the axion quality problem is compatible with inflationary constraints.

hep-ph↗
arXiv2026

Qubit-Qutrit Quantum Tomography of hadronic $\Lambda\phi$ and $\Lambda K^{\ast 0}$ systems

Quantum-information observables have emerged in recent years as new tools in nuclear and particle physics, from entanglement in top-quark pairs to spin correlations in $\Lambda\bar{\Lambda}$ production. Extending these studies to unequal-spin hadronic final states poses a fundamental challenge: the $6\times6$ density matrix of a qubit-qutrit system contains 35 independent spin parameters, but the decays of $\Lambda V$ pairs, with $V=\phi$ or $K^{*0}$, provide access to only 23 due to the hidden vector polarization from the strong decay. In this Letter, we formulate a qubit-qutrit quantum tomography (QQQT) technique for these spin-$\tfrac{1}{2}\otimes1$ systems and establish exact criteria for entanglement certification from the \textit{incomplete} density matrix. Compared with the $\Lambda\bar{\Lambda}$ system, QQQT of $\Lambda\phi$ and $\Lambda K^{*0}$ provides a new probe of nonperturbative QCD hadronization, enabling a direct comparison of the spin evolution of entangled quark pairs produced from the vacuum as they hadronize into a baryon or a vector meson.

hep-ph↗
arXiv2026

Twist decomposition of exclusive heavy meson production cross sections

We study the twist decomposition of the total cross sections for exclusive heavy vector meson electroproduction and photoproduction in the $\gamma^\ast p$ processes, within the leading logarithmic $1/x$ BFKL formalism. The Mellin transforms of the impact factors of the vector meson are calculated. We show that the higher twist contributions are strongly suppressed in the low-$x$ kinematical regime. Possible enhancement of the higher twists effects for nuclei targets is discussed.

hep-ph↗