auto-task(TwoHDM): add API-map.yaml tracking the Two Higgs Doublet Model API

[ShlokVaibhav]

Summary

Adds Physlib/Particles/BeyondTheStandardModel/TwoHDM/API-map.yaml, a new in-repo tracker for
the Two Higgs Doublet Model API (Physlib/Particles/BeyondTheStandardModel/TwoHDM/). The map
is generated from the directory's three Lean files (Basic.lean, GramMatrix.lean,
Potential.lean), with GitHub issue
#853 "API: Two Higgs Doublet Model Vector Space"
used only as a reference for the intended scope. No Lean source is touched; lake build stays
green (a YAML-only change).

The directory has no API-map.yaml yet and no open PR is adding or editing an API-map.yaml
there. Two open PRs edit Lean files in this directory (#1321 touches Basic.lean, #1312 touches
Potential.lean), but neither adds a map, so the directory is eligible.

All links below pin commit 843373266f73adaccb4db401c545fdef9810f78e so line numbers are stable.

A note on the issue checklist vs. the code

Per the task rules, every done flag was decided by reading the code, not by trusting the
issue's checkboxes. The issue's checklist covers only 5 items; the directory actually provides a
large Gram-matrix / Gram-vector / potential-stability API beyond that, so the map adds done: true
requirements for the functionality the files genuinely contain (grounded in the module docstrings).
The two issue items left unchecked — a vector-space instance on TwoHiggsDoublet and a ℤ₂ swap
action — are confirmed absent by grep and are marked done: false.

---

Field-by-field justification (reviewer tick-box)

Title / Overview

Title: Two Higgs Doublet Model

Overview: |
    The key data structure is `TwoHiggsDoublet`, the configuration space of the two
    Higgs doublet model (an extension of the Standard Model with a second Higgs
    doublet), holding two Higgs vectors `Φ1 Φ2 : HiggsVec`. The API provides the
    gauge-group action on this space, its Gram-matrix and Gram-vector invariants that
    characterise the gauge orbits, and the 2HDM potential together with its stability
    theory.

Grounded in the Basic.lean module docstring
(Basic.lean#L11-L18):

# The Two Higgs Doublet Model

The two Higgs doublet model is the standard model plus an additional Higgs doublet.

## i. Overview

The two Higgs doublet model (2HDM) is an extension of the Standard Model which adds a second Higgs
doublet.

and the TwoHiggsDoublet structure docstring
(Basic.lean#L37-L43):

/-- The configuration space of the two Higgs doublet model.
  In otherwords, the underlying vector space associated with the model. -/
structure TwoHiggsDoublet where
  /-- The first Higgs doublet. -/
  Φ1 : HiggsVec
  /-- The second Higgs doublet. -/
  Φ2 : HiggsVec

Issue #853: "The key data structure shall correspond to the vector space associated with Higgs
fields. It shall contain two fields, one for each of the Higgs vectors."

ParentAPIs

ParentAPIs:
  - Higgs Field (Physlib/Particles/StandardModel/HiggsBoson)
  - Pauli matrices (Physlib/Relativity/PauliMatrices)

Higgs Field — the only external public import
(Basic.lean#L8):

public import Physlib.Particles.StandardModel.HiggsBoson.Basic

It is actually used: TwoHiggsDoublet is built from HiggsVec
(Basic.lean#L39-L43)
and the group action uses StandardModel.GaugeGroupI
(Basic.lean#L61-L64).
This matches issue #853's stated Parent API, #857 "API: Higgs Field".

Pauli matrices — the Gram vector is defined via the Pauli basis
PauliMatrix.pauliBasis (from Physlib/Relativity/PauliMatrices, imported transitively through the
Higgs-boson import)
(GramMatrix.lean#L280-L282):

/-- A real vector containing the components of the Gram matrix in the Pauli basis. -/
noncomputable def gramVector (H : TwoHiggsDoublet) : Fin 1 ⊕ Fin 3 → ℝ := fun μ =>
  2 * PauliMatrix.pauliBasis.repr ⟨gramMatrix H, gramMatrix_selfAdjoint H⟩ μ

References

References:
  - https://arxiv.org/abs/hep-ph/0605184
  - https://arxiv.org/abs/1605.03237

Taken verbatim from the Basic.lean ## References section
(Basic.lean#L20-L24):

## References

- https://arxiv.org/abs/hep-ph/0605184
- https://arxiv.org/abs/1605.03237

Both are also cited throughout GramMatrix.lean and Potential.lean (e.g. the potential follows
the convention of 1605.03237 and the stability analysis follows / corrects hep-ph/0605184,
Potential.lean#L44-L52).
No reference is invented.

---

Requirements

✅ TwoHiggsDoublet is defined

- description: >
    The key data structure `TwoHiggsDoublet`, the configuration space of the model
    holding two Higgs vectors, is defined.
  done: true
  location: Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean (TwoHiggsDoublet)

Basic.lean#L37-L43

structure TwoHiggsDoublet where
  /-- The first Higgs doublet. -/
  Φ1 : HiggsVec
  /-- The second Higgs doublet. -/
  Φ2 : HiggsVec

Issue #853: "## Key data structure … - [x] is defined."

✅ Global gauge group action

- description: >
    The API contains the action of the global gauge group on the two Higgs doublets.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
    (SMul GaugeGroupI TwoHiggsDoublet, MulAction GaugeGroupI TwoHiggsDoublet)

Basic.lean#L61-L78

noncomputable instance : SMul StandardModel.GaugeGroupI TwoHiggsDoublet where
  smul g H :=
    { Φ1 := g • H.Φ1
      Φ2 := g • H.Φ2 }
...
noncomputable instance : MulAction StandardModel.GaugeGroupI TwoHiggsDoublet where

Issue #853: "- [x] The API shall contain the action of the global gauge group on the two Higgs doublets."

❌ Vector-space (ℝ-module) instance on TwoHiggsDoublet (issue unchecked, absent)

- description: >
    The API contains an instance of a vector space (ℝ-module) on the key data
    structure `TwoHiggsDoublet`.
  done: false
  location: N/A

grep -nE "Module|AddCommGroup|VectorSpace" Physlib/Particles/BeyondTheStandardModel/TwoHDM/
returns nothing — only the SMul/MulAction of the gauge group exist on TwoHiggsDoublet, not an
additive/module structure. Issue #853 lists this as - [ ] (unchecked); confirmed done: false.

❌ ℤ₂ action swapping the two Higgs vectors (issue unchecked, absent)

- description: >
    The API contains an action of the group ℤ₂ swapping the two Higgs vectors.
  done: false
  location: N/A

grep -niE "zmod|ℤ_?2|z₂|swap" Physlib/Particles/BeyondTheStandardModel/TwoHDM/ returns nothing.
Issue #853 lists this as - [ ] (unchecked); confirmed done: false.

✅ Gram matrix and its positivity properties

- description: >
    The API contains the Gram matrix of a two Higgs doublet, together with its
    self-adjointness and the non-negativity of its determinant and trace.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
    (gramMatrix, gramMatrix_selfAdjoint, gramMatrix_det_nonneg, gramMatrix_tr_nonneg)

GramMatrix.lean#L32-L41
and
GramMatrix.lean#L73-L88

noncomputable def gramMatrix (H : TwoHiggsDoublet) : Matrix (Fin 2) (Fin 2) ℂ :=
  !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ]
...
lemma gramMatrix_det_nonneg (H : TwoHiggsDoublet) : 0 ≤ H.gramMatrix.det.re := ...
lemma gramMatrix_tr_nonneg (H : TwoHiggsDoublet) : 0 ≤ H.gramMatrix.trace.re := ...

Grounded in GramMatrix.lean's docstring: "the gram matrix … describes the gauge orbits of the
configuration space"
(GramMatrix.lean#L9-L18).

✅ Gauge orbits characterised by the Gram matrix

- description: >
    The API proves that two configurations lie in the same gauge orbit iff they have
    the same Gram matrix.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
    (mem_orbit_gaugeGroupI_iff_gramMatrix)

GramMatrix.lean#L156-L158

lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) :
    H1 ∈ MulAction.orbit GaugeGroupI H2 ↔ H1.gramMatrix = H2.gramMatrix := by

✅ Gram matrix surjectivity

- description: >
    The API proves surjectivity of the Gram matrix: every self-adjoint matrix with
    non-negative determinant and trace arises as the Gram matrix of some configuration.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
    (gramMatrix_surjective_det_tr)

GramMatrix.lean#L220-L222

lemma gramMatrix_surjective_det_tr (K : Matrix (Fin 2) (Fin 2) ℂ)
    (hKs : IsSelfAdjoint K) (hKdet : 0 ≤ K.det.re) (hKtr : 0 ≤ K.trace.re) :
    ∃ H : TwoHiggsDoublet, H.gramMatrix = K := by

✅ Gram vector, orbit characterisation, and surjectivity

- description: >
    The API contains the Gram vector (Pauli-basis components of the Gram matrix),
    with its gauge-orbit characterisation and surjectivity.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
    (gramVector, mem_orbit_gaugeGroupI_iff_gramVector, gramVector_surjective)

GramMatrix.lean#L280-L282,
#L425-L428,
#L456-L458

noncomputable def gramVector (H : TwoHiggsDoublet) : Fin 1 ⊕ Fin 3 → ℝ := ...
lemma gramVector_surjective (v : Fin 1 ⊕ Fin 3 → ℝ) ... : ∃ H : TwoHiggsDoublet, H.gramVector = v := ...
lemma mem_orbit_gaugeGroupI_iff_gramVector (H1 H2 : TwoHiggsDoublet) :
    H1 ∈ MulAction.orbit GaugeGroupI H2 ↔ H1.gramVector = H2.gramVector := ...

✅ Potential parameters and gram reparameterization (ξ, η)

- description: >
    The API contains the type of 2HDM potential parameters and its gram-vector
    reparameterization (ξ, η).
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (PotentialParameters, PotentialParameters.ξ, PotentialParameters.η)

Potential.lean#L74-L96,
#L151-L158,
#L165-L183

structure PotentialParameters where
  m₁₁2 : ℝ ; m₂₂2 : ℝ ; m₁₂2 : ℂ ; 𝓵₁ : ℝ ; ... ; 𝓵₇ : ℂ
...
noncomputable def ξ (P : PotentialParameters) (μ : Fin 1 ⊕ Fin 3) : ℝ := ...
noncomputable def η (P : PotentialParameters) : Fin 1 ⊕ Fin 3 → Fin 1 ⊕ Fin 3 → ℝ := ...

✅ Definition of the potential (mass + quartic terms)

- description: >
    The API contains the definition of the potential of the two Higgs doublets,
    built from its mass and quartic terms.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (potential, massTerm, quarticTerm)

Potential.lean#L422-L424,
massTerm #L267-L270,
quarticTerm #L307-L314

/-- The potential of the two Higgs doublet model. -/
noncomputable def potential (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ :=
  massTerm P H + quarticTerm P H

Issue #853: "- [x] The API shall contain the definition of the potential of the two Higgs doublets."

✅ Gauge invariance of the potential

- description: >
    The API contains a theorem proving that the potential (and its mass and quartic
    terms) is invariant under the global gauge group.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (gaugeGroupI_smul_potential, gaugeGroupI_smul_massTerm, gaugeGroupI_smul_quarticTerm)

Potential.lean#L426-L431

@[simp]
lemma gaugeGroupI_smul_potential (g : StandardModel.GaugeGroupI)
    (P : PotentialParameters) (H : TwoHiggsDoublet) :
    potential P (g • H) = potential P H := by
  rw [potential, potential]
  simp

Issue #853: "- [x] The API shall contain a theorem proving that the potential is invariant under
the global gauge group."

✅ Potential expressed via the Gram vector

- description: >
    The API expresses the potential and its terms in terms of the Gram vector.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (potential_eq_gramVector, massTerm_eq_gramVector, quarticTerm_eq_gramVector)

Potential.lean#L443-L446

lemma potential_eq_gramVector (P : PotentialParameters) (H : TwoHiggsDoublet) :
    potential P H = ∑ μ, P.ξ μ * H.gramVector μ +
    ∑ a, ∑ b, H.gramVector a * H.gramVector b * P.η a b := by
  rw [potential, massTerm_eq_gramVector, quarticTerm_eq_gramVector]

✅ Stability condition and its gram-vector characterisation

- description: >
    The API defines the stability (bounded-below) condition of the potential and
    gives gram-vector characterisations of it.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (PotentialIsStable, potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced)

Potential.lean#L462-L464
and
#L809-L813

/-- The condition that the potential is stable. -/
def PotentialIsStable (P : PotentialParameters) : Prop :=
  ∃ c : ℝ, ∀ H : TwoHiggsDoublet, c ≤ potential P H
...
lemma potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced (P : PotentialParameters) :
    PotentialIsStable P ↔ ...

✅ Strong stability implies stability

- description: >
    The API proves that strong stability (positivity of the reduced quartic term)
    implies stability of the potential.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (potentialIsStable_of_strong)

Potential.lean#L895-L900

/-- The potential is stable if it is strongly stable, i.e. its quartic term is always positive. ... -/
lemma potentialIsStable_of_strong (P : PotentialParameters)
    (h : ∀ k, ‖k‖ ^ 2 ≤ 1 → 0 < quarticTermReduced P k) :
    PotentialIsStable P := by

✅ Counterexample invalidating a step in hep-ph/0605184

- description: >
    The API gives an explicit counterexample invalidating a step in
    arXiv:hep-ph/0605184: an unstable potential whose reduced quartic term is
    non-negative and whose reduced mass term is non-negative wherever the reduced
    quartic term vanishes.
  done: true
  location: >
    Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
    (stabilityCounterExample, stabilityCounterExample_not_potentialIsStable,
    forall_reduced_exists_not_potentialIsStable)

Potential.lean#L200-L220,
#L474-L476,
#L940-L944

/-- A lemma invalidating the step in https://arxiv.org/pdf/hep-ph/0605184 leading to
  equation (4.4). -/
lemma forall_reduced_exists_not_potentialIsStable :
    ∃ P, ¬ PotentialIsStable P ∧ (∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
    0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k)) := by

Grounded in the Potential.lean docstring section "E.7. Showing step in hep-ph/0605184 is
invalid"
(Potential.lean#L42-L51).

---

Verification

• ruby -e 'require "yaml"; d=YAML.safe_load(File.read(ARGV[0])); raise "bad keys" unless (%w[version Title Overview ParentAPIs References Requirements]-d.keys).empty?' → valid YAML;
  top-level keys exactly version, Title, Overview, ParentAPIs, References, Requirements;
  15 requirements, 13 done: true, 2 done: false.
• Every done: true declaration was confirmed present in the source at the line ranges linked
  above (grep/read of Basic.lean, GramMatrix.lean, Potential.lean).
• Both done: false items confirmed absent:
  grep -nE "Module|AddCommGroup|VectorSpace" …/TwoHDM and
  grep -niE "zmod|ℤ_?2|z₂|swap" …/TwoHDM return nothing.
• lake build is unaffected — this is a YAML-only addition that cannot enter the Lean build graph.
• No .lean file, other map, docstring, or the GitHub issue was modified.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Approved - merging