Basic

📁 Source: PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean

Statistics

Metric	Count
Definitions HiggsBundle, HiggsField, const, gaugeAction, gauge_orbit_surject, guage_orbit, instInnerForallSpaceTimeOfNatNatComplex, normSq, toHiggsVec, «term‖_‖_H^2», HiggsVec, instDistribMulActionGaugeGroupI, instMulActionGaugeGroupI, instSMulGaugeGroupI, ofReal, orthonormBasis, stability_group, stability_group_single, toFin2ℂ, toRealGroupElem	20
Theorems apply_im_smooth, apply_re_smooth, apply_smooth, const_apply, const_normSq, const_toHiggsVec_apply, contDiff, inner_add_left, inner_add_right, inner_apply, inner_eq_expand, inner_expand_conj, inner_neg_left, inner_neg_right, inner_self_eq_normSq, inner_smooth, inner_symm, inner_zero_left, inner_zero_right, normSq_eq_inner_self_re, normSq_expand, normSq_nonneg, normSq_smooth, normSq_zero, toFin2ℂ_comp_toHiggsVec, toHiggsVec_smooth, toVec_smooth, gaugeGroupI_smul_eq, gaugeGroupI_smul_eq_U1_mul_SU2, gaugeGroupI_smul_eq_U1_smul_SU2, gaugeGroupI_smul_inner, gaugeGroupI_smul_norm, gaugeGroupI_smul_phase_snd, mem_orbit_gaugeGroupI_iff, ofReal_normSq, ofU1Subgroup_smul_eq_smul, smooth_toFin2ℂ, toRealGroupElem_smul_self, instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold	39
Total	59

StandardModel

Definitions

Name	Category	Theorems
HiggsBundle 📖	CompOp	27 math math: HiggsField.toVec_smooth, HiggsField.const_toHiggsVec_apply, HiggsField.apply_smooth, HiggsField.apply_im_smooth, HiggsField.const_apply, instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, HiggsField.inner_zero_right, HiggsField.inner_add_left, HiggsField.inner_neg_right, HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, HiggsField.inner_neg_left, HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, HiggsField.inner_add_right, HiggsField.normSq_expand, HiggsField.Potential.toFun_zero, HiggsField.apply_re_smooth, HiggsField.inner_eq_expand, HiggsField.inner_zero_left, HiggsField.inner_expand_conj, HiggsField.const_normSq, HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, HiggsField.Potential.toFun_eq_zero_iff, HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, HiggsField.toFin2ℂ_comp_toHiggsVec, HiggsField.inner_apply, HiggsField.contDiff, HiggsField.normSq_zero
HiggsField 📖	CompOp	34 math math: HiggsField.toVec_smooth, HiggsField.const_toHiggsVec_apply, HiggsField.inner_symm, HiggsField.Potential.isMinOn_iff_of_μSq_nonpos_𝓵_pos, HiggsField.apply_smooth, HiggsField.inner_smooth, HiggsField.apply_im_smooth, HiggsField.const_apply, HiggsField.inner_zero_right, HiggsField.Potential.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos, HiggsField.inner_add_left, HiggsField.inner_neg_right, HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, HiggsField.inner_neg_left, HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, HiggsField.inner_add_right, HiggsField.normSq_expand, HiggsField.Potential.toFun_zero, HiggsField.apply_re_smooth, HiggsField.Potential.isMaxOn_iff_isMinOn_neg, HiggsField.inner_eq_expand, HiggsField.inner_zero_left, HiggsField.inner_self_eq_normSq, HiggsField.inner_expand_conj, HiggsField.Potential.isMinOn_iff_of_μSq_nonneg_𝓵_pos, HiggsField.const_normSq, HiggsField.normSq_eq_inner_self_re, HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, HiggsField.Potential.toFun_eq_zero_iff, HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, HiggsField.toFin2ℂ_comp_toHiggsVec, HiggsField.inner_apply, HiggsField.contDiff, HiggsField.normSq_zero
HiggsVec 📖	CompOp	61 math math: HiggsField.toVec_smooth, HiggsField.const_toHiggsVec_apply, HiggsField.apply_smooth, HiggsField.apply_im_smooth, TwoHiggsDoublet.gramVector_inr_one_eq, HiggsVec.gaugeGroupI_smul_inner, TwoHiggsDoublet.massTerm_stabilityCounterExample, HiggsField.const_apply, TwoHiggsDoublet.gaugeGroupI_smul_fst, instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, TwoHiggsDoublet.normSq_Φ2_eq_gramVector, TwoHiggsDoublet.quarticTerm_stabilityCounterExample, HiggsField.inner_zero_right, HiggsVec.ofReal_normSq, HiggsVec.gaugeGroupI_smul_eq, TwoHiggsDoublet.gramVector_inl_zero_eq, HiggsField.inner_add_left, HiggsVec.gaugeGroupI_smul_phase_snd, TwoHiggsDoublet.gaugeGroupI_exists_fst_eq, HiggsField.inner_neg_right, HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, HiggsField.inner_neg_left, TwoHiggsDoublet.gaugeGroupI_exists_fst_eq_snd_eq, HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, HiggsField.inner_add_right, HiggsField.normSq_expand, TwoHiggsDoublet.eq_fst_norm_of_eq_gramMatrix, HiggsField.Potential.toFun_zero, TwoHiggsDoublet.gramMatrix_det_eq_real, TwoHiggsDoublet.gaugeGroupI_smul_snd, TwoHiggsDoublet.normSq_Φ1_eq_gramVector, HiggsVec.mem_orbit_gaugeGroupI_iff, HiggsField.apply_re_smooth, HiggsField.inner_eq_expand, HiggsField.inner_zero_left, HiggsVec.smooth_toFin2ℂ, HiggsField.inner_expand_conj, HiggsVec.gaugeGroupI_smul_eq_U1_smul_SU2, TwoHiggsDoublet.Φ2_inner_Φ1_eq_gramVector, HiggsField.toHiggsVec_smooth, TwoHiggsDoublet.potential_stabilityCounterExample, HiggsField.const_normSq, HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, HiggsField.Potential.toFun_eq_zero_iff, TwoHiggsDoublet.gramVector_inr_two_eq, HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, HiggsVec.gaugeGroupI_smul_eq_U1_mul_SU2, HiggsField.toFin2ℂ_comp_toHiggsVec, TwoHiggsDoublet.quarticTerm_stabilityCounterExample_eq_norm_pow_four, HiggsField.inner_apply, HiggsVec.gaugeGroupI_smul_norm, TwoHiggsDoublet.gramVector_inr_zero_eq, TwoHiggsDoublet.eq_snd_norm_of_eq_gramMatrix, TwoHiggsDoublet.Φ1_inner_Φ2_eq_gramVector, HiggsVec.ofU1Subgroup_smul_eq_smul, TwoHiggsDoublet.gramMatrix_det_eq, TwoHiggsDoublet.quarticTerm_𝓵₄_expand, HiggsField.contDiff, HiggsField.normSq_zero, TwoHiggsDoublet.Φ1_inner_Φ2_normSq_eq_gramVector, HiggsVec.toRealGroupElem_smul_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold 📖	mathematical	—	SpaceTime HiggsVec HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace	—	—

StandardModel.HiggsField

Definitions

Name	Category	Theorems
const 📖	CompOp	3 math math: const_toHiggsVec_apply, const_apply, const_normSq
gaugeAction 📖	CompOp	—
gauge_orbit_surject 📖	CompOp	—
guage_orbit 📖	CompOp	—
instInnerForallSpaceTimeOfNatNatComplex 📖	CompOp	13 math math: inner_symm, inner_smooth, inner_zero_right, inner_add_left, inner_neg_right, inner_neg_left, inner_add_right, inner_eq_expand, inner_zero_left, inner_self_eq_normSq, inner_expand_conj, normSq_eq_inner_self_re, inner_apply
normSq 📖	CompOp	14 math math: normSq_nonneg, normSq_smooth, Potential.as_quad, Potential.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos, Potential.isMaxOn_iff_field_of_𝓵_neg, normSq_expand, Potential.quadDiscrim_eq_zero_iff_normSq, inner_self_eq_normSq, const_normSq, normSq_eq_inner_self_re, Potential.isMinOn_iff_field_of_𝓵_pos, Potential.toFun_eq_zero_iff, normSq_zero, Potential.complete_square
toHiggsVec 📖	CompOp	3 math math: const_toHiggsVec_apply, toHiggsVec_smooth, toFin2ℂ_comp_toHiggsVec
«term‖_‖_H^2» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_im_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsField StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.asSmoothManifold StandardModel.HiggsVec	—	apply_smooth
apply_re_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsField StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.asSmoothManifold StandardModel.HiggsVec	—	apply_smooth
apply_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsField StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.asSmoothManifold StandardModel.HiggsVec	—	contDiff
const_apply 📖	mathematical	—	StandardModel.HiggsField SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec const	—	—
const_normSq 📖	mathematical	—	normSq StandardModel.HiggsVec StandardModel.HiggsField Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsBundle const	—	—
const_toHiggsVec_apply 📖	mathematical	—	StandardModel.HiggsField SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec const toHiggsVec	—	—
contDiff 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace StandardModel.HiggsField StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	toHiggsVec_smooth
inner_add_left 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
inner_add_right 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
inner_apply 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex StandardModel.HiggsBundle SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	—
inner_eq_expand 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	—
inner_expand_conj 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	—
inner_neg_left 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
inner_neg_right 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
inner_self_eq_normSq 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex normSq	—	—
inner_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex	—	inner_eq_expand apply_re_smooth apply_im_smooth
inner_symm 📖	mathematical	—	SpaceTime StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex	—	—
inner_zero_left 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
inner_zero_right 📖	mathematical	—	StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
normSq_eq_inner_self_re 📖	mathematical	—	normSq StandardModel.HiggsField instInnerForallSpaceTimeOfNatNatComplex	—	inner_self_eq_normSq
normSq_expand 📖	mathematical	—	normSq StandardModel.HiggsField SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	normSq_eq_inner_self_re inner_expand_conj
normSq_nonneg 📖	mathematical	—	normSq	—	—
normSq_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace normSq	—	normSq_expand apply_re_smooth apply_im_smooth
normSq_zero 📖	mathematical	—	normSq StandardModel.HiggsField Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold SpaceTime Lorentz.Vector.instChartedSpace StandardModel.HiggsVec StandardModel.HiggsBundle	—	—
toFin2ℂ_comp_toHiggsVec 📖	mathematical	—	toHiggsVec StandardModel.HiggsField SpaceTime StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.asSmoothManifold Lorentz.Vector.instChartedSpace StandardModel.HiggsVec	—	—
toHiggsVec_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsVec toHiggsVec	—	—
toVec_smooth 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector.instChartedSpace StandardModel.HiggsField StandardModel.HiggsBundle Lorentz.Vector Lorentz.Vector.asSmoothManifold StandardModel.HiggsVec	—	toHiggsVec_smooth

StandardModel.HiggsVec

Definitions

Name	Category	Theorems
instDistribMulActionGaugeGroupI 📖	CompOp	—
instMulActionGaugeGroupI 📖	CompOp	—
instSMulGaugeGroupI 📖	CompOp	13 math math: gaugeGroupI_smul_inner, TwoHiggsDoublet.gaugeGroupI_smul_fst, gaugeGroupI_smul_eq, gaugeGroupI_smul_phase_snd, TwoHiggsDoublet.gaugeGroupI_exists_fst_eq, TwoHiggsDoublet.gaugeGroupI_exists_fst_eq_snd_eq, TwoHiggsDoublet.gaugeGroupI_smul_snd, mem_orbit_gaugeGroupI_iff, gaugeGroupI_smul_eq_U1_smul_SU2, gaugeGroupI_smul_eq_U1_mul_SU2, gaugeGroupI_smul_norm, ofU1Subgroup_smul_eq_smul, toRealGroupElem_smul_self
ofReal 📖	CompOp	2 math math: ofReal_normSq, toRealGroupElem_smul_self
orthonormBasis 📖	CompOp	—
stability_group 📖	CompOp	—
stability_group_single 📖	CompOp	—
toFin2ℂ 📖	CompOp	1 math math: smooth_toFin2ℂ
toRealGroupElem 📖	CompOp	1 math math: toRealGroupElem_smul_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gaugeGroupI_smul_eq 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI StandardModel.GaugeGroupI.toU1 StandardModel.GaugeGroupI.toSU2	—	—
gaugeGroupI_smul_eq_U1_mul_SU2 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI StandardModel.GaugeGroupI.toSU2 StandardModel.GaugeGroupI.toU1	—	gaugeGroupI_smul_eq
gaugeGroupI_smul_eq_U1_smul_SU2 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI StandardModel.GaugeGroupI.toU1 StandardModel.GaugeGroupI.toSU2	—	gaugeGroupI_smul_eq
gaugeGroupI_smul_inner 📖	mathematical	—	StandardModel.HiggsVec StandardModel.GaugeGroupI instSMulGaugeGroupI	—	gaugeGroupI_smul_eq_U1_mul_SU2
gaugeGroupI_smul_norm 📖	mathematical	—	StandardModel.HiggsVec StandardModel.GaugeGroupI instSMulGaugeGroupI	—	gaugeGroupI_smul_inner
gaugeGroupI_smul_phase_snd 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI	—	ofU1Subgroup_smul_eq_smul
mem_orbit_gaugeGroupI_iff 📖	mathematical	—	StandardModel.HiggsVec StandardModel.GaugeGroupI instSMulGaugeGroupI	—	gaugeGroupI_smul_norm toRealGroupElem_smul_self
ofReal_normSq 📖	mathematical	—	StandardModel.HiggsVec ofReal	—	—
ofU1Subgroup_smul_eq_smul 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI StandardModel.GaugeGroupI.ofU1Subgroup	—	gaugeGroupI_smul_eq_U1_smul_SU2
smooth_toFin2ℂ 📖	mathematical	—	StandardModel.HiggsVec toFin2ℂ	—	—
toRealGroupElem_smul_self 📖	mathematical	—	StandardModel.GaugeGroupI StandardModel.HiggsVec instSMulGaugeGroupI toRealGroupElem ofReal	—	gaugeGroupI_smul_eq

---

← Back to Index