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

Physlib/Particles/BeyondTheStandardModel/TwoHDM/API-map.yaml

@@ -0,0 +1,135 @@
+version: v0.1
+
+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.
+
+ParentAPIs:
+  - Higgs Field (Physlib/Particles/StandardModel/HiggsBoson)
+  - Pauli matrices (Physlib/Relativity/PauliMatrices)
+
+References:
+  - https://arxiv.org/abs/hep-ph/0605184
+  - https://arxiv.org/abs/1605.03237
+
+Requirements:
+
+  - 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)
+
+  - 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)
+
+  - description: >
+      The API contains an instance of a vector space (ℝ-module) on the key data
+      structure `TwoHiggsDoublet`.
+    done: false
+    location: N/A
+
+  - description: >
+      The API contains an action of the group ℤ₂ swapping the two Higgs vectors.
+    done: false
+    location: N/A
+
+  - 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)
+
+  - 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)
+
+  - 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)
+
+  - 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)
+
+  - 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.η)
+
+  - 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)
+
+  - 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)
+
+  - 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)
+
+  - 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)
+
+  - 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)
+
+  - 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)