diff --git a/Physlib/Particles/StandardModel/HiggsBoson/API-map.yaml b/Physlib/Particles/StandardModel/HiggsBoson/API-map.yaml new file mode 100644 index 000000000..ff8f1be70 --- /dev/null +++ b/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