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

This paper reports the discovery of a critical error in the 2006 Maniatis et al. analysis of the two Higgs doublet model potential's stability, which was identified through formalization in the Lean theorem prover and represents the first known non-trivial error in a physics paper uncovered by this rigorous method.

The Gist

Imagine you are an architect who has spent decades designing skyscrapers based on a specific blueprint published in 2006. That blueprint, written by four respected experts, claimed to have the "Golden Rule" for ensuring these skyscrapers (which represent the universe's fundamental particles) wouldn't collapse into a black hole. Everyone trusted it. It was the standard reference.

Now, imagine a new technology arrives: a Super-Computer Architect. This isn't just a calculator; it's a robot that doesn't just read the blueprint, but actually builds the skyscraper in a perfect, mathematical simulation to see if it stands up.

This paper is the report from that robot. It says: "We tried to build the skyscraper using the 2006 blueprint, and it collapsed. The blueprint had a hidden crack."

Here is the story of that discovery, broken down simply:

1. The Setting: The Two Higgs Doublet Model (2HDM)

In physics, the "Higgs field" is like a cosmic molasses that gives particles their mass. The "Standard Model" of physics usually assumes there is only one type of this molasses (one Higgs doublet).

However, many physicists think there might be two types of Higgs fields interacting. This is called the Two Higgs Doublet Model (2HDM). It's like having two different flavors of molasses swirling together.

The big question for physicists is: Is this mixture stable?

• Stable: The mixture holds together, and the universe is safe.
• Unstable: The mixture falls apart, the energy goes negative, and the universe essentially implodes.

2. The 2006 "Golden Rule"

In 2006, a team of physicists (Maniatis et al.) published a paper claiming to have found a simple checklist (a mathematical condition) to determine if this two-molasses mixture is stable.

They said: "If you check these specific numbers, and they pass the test, the universe is safe. If they fail, it's not."
This paper became the "Bible" for anyone working on this theory. Everyone assumed it was 100% correct because it was written by experts using the best math of the time.

3. The New Tool: Lean and Formalization

The author of this paper, Joseph Tooby-Smith, didn't use a telescope or a particle collider. He used a computer program called Lean.

Think of Lean as a hyper-strict proofreader.

• When a human writes a math proof, they might skip a tiny step because "it's obvious."
• Lean doesn't believe in "obvious." It demands that every single logical step be written out in code. If there is a gap, the computer refuses to accept the proof.

The author took the 2006 "Golden Rule" and tried to translate it into Lean's strict code. He wasn't trying to find a mistake; he was just trying to digitize the rule to make it easier for computers to use later.

4. The Discovery: The Hidden Crack

As the computer tried to build the logic of the 2006 paper, it hit a wall. It found a flaw.

The 2006 paper claimed that a specific condition (let's call it Condition C) was the perfect test for stability. They said: "If Condition C is true, the potential is stable."

The computer found a Counter-Example.
It constructed a specific, imaginary version of the universe where:

1. Condition C was TRUE (it passed the 2006 test).
2. BUT the universe was actually UNSTABLE (it collapsed).

The Analogy:
Imagine the 2006 paper said: "If a bridge has red paint, it is safe to drive on."
The computer found a bridge that was painted bright red (passed the test) but had no support beams underneath (it was unsafe). The rule "Red = Safe" was wrong.

5. Why This Matters

You might think, "Well, the 2006 paper was mostly right, so who cares?"

Here is why this is a big deal:

1. It's the First Time: This is the first time a computer has found a non-trivial, real-world error in a major physics paper. Usually, computers find typos. This time, it found a broken logic chain that had fooled human experts for 20 years.
2. The "Gold Standard" Question: If the experts in 2006 missed this, how many other papers in physics might have similar hidden cracks? It suggests that we need to start using these "Super-Computer Architects" (formalization) to double-check our most important scientific theories.
3. The Fix: The author didn't just break the rule; he fixed it. He provided a new, correct, and more complex rule (a new checklist) that the computer verified is actually true.

The Takeaway

This paper is a story about humility and technology.

• Humility: Even the smartest physicists can make subtle mistakes that look obvious but aren't.
• Technology: We now have tools (like Lean) that can act as a "truth machine," checking our work with a level of precision that human brains simply can't sustain over long, complex arguments.

The author concludes that while the error in the 2006 paper doesn't destroy the whole theory of the Two Higgs Doublet Model, it does mean we can't trust the old "Golden Rule" anymore. We have to use the new, stricter rule to ensure our understanding of the universe is truly stable.

Technical Summary

Here is a detailed technical summary of the paper "Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature" by Joseph Tooby-Smith.

1. Problem Statement

The paper addresses the mathematical correctness of the stability conditions for the Two Higgs Doublet Model (2HDM) potential, a popular extension of the Standard Model of particle physics. Specifically, it investigates the validity of Theorem 1 in a widely cited 2006 paper by Maniatis, von Manteuffel, Nachtmann, and Nagel [6].

• The Claim: The 2006 paper asserted that a specific condition (referred to as Condition C) is both necessary and sufficient for the 2HDM potential to be stable (bounded from below).
• The Goal: To verify this claim using Interactive Theorem Proving (ITP) to ensure rigorous mathematical correctness, a standard increasingly applied to physics literature.

2. Methodology

The author utilized the Lean interactive theorem prover and the PhysLib (formerly PhysLean) library, an open-source community project for formalizing physics results.

• Formalization Process:
  • The 2HDM potential, originally defined by 10 parameters (mass terms and quartic couplings), was formalized using the Gram matrix approach.
  • The Higgs doublet vectors ($\Phi_1, \Phi_2$) were mapped to a 4-component Gram vector ($K_\mu$). This transformation allows the potential $V$ to be expressed as a quadratic form involving a vector $\xi$ and a matrix $\eta$:
    $$V = \sum \xi_\mu K_\mu + \sum \eta_{\mu\nu} K_\mu K_\nu$$
  • The stability condition (boundedness from below) was translated into a logical proposition involving quantifiers over real numbers and the constraints of the Gram vector space ($0 \le K_0$and$\sum K_a^2 \le K_0^2$).
• Verification Strategy:
  • The author formalized the definitions of the potential, the Gram vector, and the stability conditions.
  • The logical structure of the 2006 paper's argument was reconstructed in Lean.
  • A specific counter-example was constructed and verified within the system to test the sufficiency of Condition C.
• Human Verification: The paper explicitly notes that no AI was used in the formalization; all code and proofs were written and checked by humans to ensure physical and mathematical fidelity.

3. Key Contributions

A. Discovery of a Non-Trivial Error

The primary contribution is the identification of a non-trivial error in the 2006 paper [6].

• The Error: The authors of [6] claimed that Condition C is necessary and sufficient for stability. Condition C states:

  For all vectors $\vec{k}$ with $\|\vec{k}\|^2 \le 1$: $J_4(\vec{k}) > 0$ OR ($J_4(\vec{k}) = 0$ AND $J_2(\vec{k}) \ge 0$).
  (Where $J_2$ and $J_4$ are functions derived from the quadratic and quartic terms of the potential).

• The Finding: The formalization proved that while Condition C is necessary, it is not sufficient. There exist potentials that satisfy Condition C but are unstable (unbounded from below).
• Consequence: Since Theorem 1 in [6] is a reworking of this incorrect equivalence, Theorem 1 is invalid.

B. Construction of a Counter-Example

The paper provides an explicit, formally verified counter-example to disprove the sufficiency of Condition C:

• Parameters: A specific set of 2HDM parameters was chosen ($m_{11}^2=m_{22}^2=0, m_{12}^2=i, \lambda_{1..5}=2, \lambda_{6,7}=-2$).
• Resulting Potential: $V = 2 \text{Im}(\Phi_1^\dagger \Phi_2) + \|\Phi_1 - \Phi_2\|^4$.
• Analysis:
  • The quartic term is non-negative, and when it vanishes, the quadratic term vanishes. This structure naively suggests stability.
  • However, the formal proof demonstrates that for any real number $c$, there exist Higgs doublets $\Phi_1, \Phi_2$ such that $V(\Phi_1, \Phi_2) < c$.
  • Despite this instability, the potential satisfies Condition C, proving the condition is insufficient.

C. New Complexity Reduction

The paper introduces a correct reduction in the complexity of the stability condition, which has been formalized in PhysLib:

• The stability condition is equivalent to the existence of a non-negative real number $c$ such that for all $\vec{k}$ with $\|\vec{k}\|^2 \le 1$:
  $$0 \le J_4(\vec{k}) \quad \text{AND} \quad (J_2(\vec{k}) < 0 \implies J_2(\vec{k})^2 \le 4c J_4(\vec{k}))$$
• This formulation correctly handles the existential quantifier ($\exists c$) and provides a rigorous, verifiable criterion for stability, reducing the complexity of the problem compared to the original formulation.

4. Results

• Invalidation of Literature: The main theorem of the 2006 paper [6] is demonstrably false.
• Formal Verification: The error was not found through heuristic analysis but through a rigorous, machine-checked proof that an unstable potential satisfies the "stable" condition proposed in the literature.
• Corrected Framework: The paper provides the correct logical structure for 2HDM stability, distinguishing between necessary and sufficient conditions, and offering a new, verified reduction of the stability condition (Eq. 15 in the paper).

5. Significance

• First Non-Trivial Physics Error via Formalization: To the author's knowledge, this is the first instance where a non-trivial error in a research-level physics paper was discovered solely through the process of formalization. Previous instances were minor imprecisions.
• Implications for Physics Literature: The discovery raises concerns about the reliability of other physics papers that have not undergone similar scrutiny. It suggests that errors in complex theoretical arguments may be more common than previously thought.
• Advancement of Formal Methods in Physics: The work demonstrates the maturity of libraries like PhysLib and tools like Lean for handling high-energy physics problems. It establishes formal verification as a viable "gold standard" for ensuring the correctness of theoretical physics results.
• Community Impact: The corrected results and the counter-example are now part of the open-source PhysLib library, allowing future researchers to build upon a verified foundation rather than an erroneous one.

In conclusion, this paper serves as a landmark case study in the intersection of computer science and theoretical physics, proving that formal methods can uncover deep, non-obvious errors in established scientific literature and providing a corrected framework for the stability analysis of the 2HDM.