docs(higgs): add Higgs field API map

Physlib/Particles/StandardModel/HiggsBoson/API-map.yaml

@@ -0,0 +1,151 @@
+version: v0.1
+
+Title: Higgs Field
+
+Overview: |
+  The key data structure is `HiggsField`, the smooth sections of the Higgs bundle
+  `HiggsBundle` over `SpaceTime`. The bundle is currently the trivial bundle with
+  fiber `HiggsVec`, the two-dimensional complex vector space of pointwise Higgs
+  values. On `HiggsVec` the API provides an orthonormal basis, real-scalar
+  coordinates, the representation of the global Standard Model gauge group, its
+  invariance properties, and the characterisation of gauge orbits by the norm.
+  On `HiggsField` it provides constant fields, smoothness of components, the
+  pointwise inner product and norm-squared, the Standard Model Higgs potential
+  with its minimisation theory, and invariant effective potentials on pointwise
+  Higgs values. The two Higgs doublet model
+  (Physlib/Particles/BeyondTheStandardModel/TwoHDM) builds on this API.
+
+ParentAPIs:
+  - SpaceTime (Physlib/SpaceAndTime/SpaceTime)
+  - Standard Model gauge group (Physlib/Particles/StandardModel)
+
+References:
+  - "Peskin and Schroeder, An Introduction to Quantum Field Theory, Ch. 20 (gauge theories with spontaneous symmetry breaking)"
+
+Requirements:
+
+  - description: >
+      The pointwise Higgs vector space `HiggsVec` is defined, with its continuous
+      linear identification with `Fin 2 → ℂ`.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (HiggsVec, toFin2ℂ, smooth_toFin2ℂ)
+
+  - description: >
+      `HiggsVec` carries an orthonormal basis and a constructor from a real mass
+      scale with the expected norm.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (orthonormBasis, ofReal, ofReal_normSq)
+
+  - description: >
+      `HiggsVec` is related to four real scalar coordinates.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (toRealScalars, toRealScalars_smul_real, ofReal_toRealScalars, ofReal_toRealScalars_norm)
+
+  - description: >
+      The representation of the global Standard Model gauge group on `HiggsVec` is
+      defined, with its explicit form and group-law lemmas.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (repGaugeGroupI, repGaugeGroupI_apply, repGaugeGroupI_apply_eq_U1_mul_SU2, repGaugeGroupI_apply_eq_U1_smul_SU2, repGaugeGroupI_mul_apply, repGaugeGroupI_inv_apply_eq_iff)
+
+  - description: >
+      The gauge representation on `HiggsVec` preserves inner products and norms.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (repGaugeGroupI_inner, repGaugeGroupI_norm)
+
+  - description: >
+      Gauge orbits of `HiggsVec` are characterised by the norm, including the
+      gauge action removing the phase of the second component.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (toRealGroupElem, toRealGroupElem_apply_self, exists_repGaugeGroupI_eq_iff_norm_eq, ofU1Subgroup_repGaugeGroupI_apply, repGaugeGroupI_phase_snd)
+
+  - description: >
+      The stability groups of Higgs vectors are identified.
+    done: false
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (stability_group_single, stability_group); both are informal lemmas awaiting formalisation.
+
+  - description: >
+      The Higgs bundle over `SpaceTime` is defined as a smooth vector bundle.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (HiggsBundle)
+
+  - description: >
+      The Higgs bundle is upgraded from the trivial bundle to an associated-bundle
+      construction.
+    done: false
+    location: N/A
+
+  - description: >
+      Higgs fields are defined as smooth sections of the Higgs bundle, with
+      constant fields and the underlying map to pointwise Higgs values.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (HiggsField, const, const_apply, toHiggsVec, toHiggsVec_smooth, const_toHiggsVec_apply)
+
+  - description: >
+      Smoothness of the components of a Higgs field is proved, including real and
+      imaginary parts.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (contDiff, toVec_smooth, apply_smooth, apply_re_smooth, apply_im_smooth, toFin2ℂ_comp_toHiggsVec)
+
+  - description: >
+      The pointwise inner product of Higgs fields is defined, with its expansion,
+      conjugation symmetry, additivity, and smoothness.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (inner_apply, inner_eq_expand, inner_expand_conj, inner_symm, inner_add_left, inner_add_right, inner_zero_left, inner_zero_right, inner_neg_left, inner_neg_right, inner_smooth)
+
+  - description: >
+      The pointwise norm-squared of a Higgs field is defined, with its relation to
+      the inner product, nonnegativity, and smoothness.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (normSq, inner_self_eq_normSq, normSq_eq_inner_self_re, normSq_expand, normSq_nonneg, normSq_zero, normSq_smooth, const_normSq)
+
+  - description: >
+      The global gauge action on `HiggsField` is defined, and the pointwise inner
+      product, norm-squared, and potential are proved invariant under it.
+    done: false
+    location: Physlib/Particles/StandardModel/HiggsBoson/Basic.lean (gaugeAction, guage_orbit, gauge_orbit_surject); all three are informal declarations awaiting formalisation.
+
+  - description: >
+      The Standard Model Higgs potential is defined as a structure with mass and
+      coupling parameters, evaluated smoothly on Higgs fields, with negation and
+      zero-field lemmas.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Potential.lean (Potential, toFun, toFun_smooth, neg, toFun_neg, μ2_neg, 𝓵_neg, toFun_zero)
+
+  - description: >
+      The algebraic theory of the potential is developed: completing the square,
+      the quadratic form in the norm-squared, and the discriminant with its sign
+      and vanishing characterisations.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Potential.lean (complete_square, as_quad, toFun_eq_zero_iff, quadDiscrim, quadDiscrim_nonneg, quadDiscrim_eq_zero_iff, quadDiscrim_eq_zero_iff_normSq)
+
+  - description: >
+      Boundedness of the potential is defined and its extremal theory is proved:
+      attained values, bounds at vanishing discriminant, and the minimum and
+      maximum characterisations for positive and negative quartic coupling.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/Potential.lean (IsBounded, isBounded_𝓵_nonneg, isBounded_of_𝓵_pos, neg_𝓵_sol_exists_iff, pos_𝓵_sol_exists_iff, neg_𝓵_quadDiscrim_zero_bound, pos_𝓵_quadDiscrim_zero_bound, isMinOn_iff_field_of_𝓵_pos, isMaxOn_iff_field_of_𝓵_neg)
+
+  - description: >
+      Effective potentials on pointwise Higgs values are defined, with gauge
+      invariance and the proof that invariant potentials factor through the norm.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean (EffectivePotential, IsInvariant, eq_on_orbits, eq_of_norm_eq, factors_through_norm)
+
+  - description: >
+      Effective potentials of bounded mass dimension are expanded polynomially,
+      with homogeneous terms, vanishing of odd terms for invariant potentials, and
+      the expansion in powers of the norm.
+    done: true
+    location: Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean (HasMaxMassDimLE, polynomial, apply_eq_polynomial, termOfMassDim, termOfMassDim_homogeneity, termOfMassDim_zero_of_odd, apply_eq_sum_norm_pow)
+
+  - description: >
+      Effective potentials are connected to potentials on `HiggsField`, so that
+      field-level statements can be derived from pointwise invariant ones.
+    done: false
+    location: N/A
+
+  - description: >
+      Covariant derivatives and kinetic terms for Higgs fields are defined; this
+      depends on a gauge-connection API and the SpaceTime parent API.
+    done: false
+    location: N/A