Potential

📁 Source: PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean

Statistics

Metric	Count
Definitions `PotentialIsStable`, `PotentialParameters`, `instZero`, `m₁₁2`, `m₁₂2`, `m₂₂2`, `stabilityCounterExample`, `η`, `ξ`, `𝓵₁`, `𝓵₂`, `𝓵₃`, `𝓵₄`, `𝓵₅`, `𝓵₆`, `𝓵₇`, `massTerm`, `massTermReduced`, `potential`, `quarticTerm`, `quarticTermReduced`	21
Theorems `zero_m₁₁2`, `zero_m₁₂2`, `zero_m₂₂2`, `zero_𝓵₁`, `zero_𝓵₂`, `zero_𝓵₃`, `zero_𝓵₄`, `zero_𝓵₅`, `zero_𝓵₆`, `zero_𝓵₇`, `η_symm`, `η_zero`, `ξ_zero`, `forall_reduced_exists_not_potentialIsStable`, `gaugeGroupI_smul_massTerm`, `gaugeGroupI_smul_potential`, `gaugeGroupI_smul_quarticTerm`, `massTermReduced_lower_bound`, `massTermReduced_pos_of_quarticTermReduced_zero_potentialIsStable`, `massTermReduced_stabilityCounterExample`, `massTermReduced_zero`, `massTerm_eq_gramVector`, `massTerm_stabilityCounterExample`, `massTerm_zero`, `massTerm_zero_of_quarticTerm_zero_stabilityCounterExample`, `potentialIsStable_iff_exists_forall_forall_reduced`, `potentialIsStable_iff_forall_euclid`, `potentialIsStable_iff_forall_euclid_lt`, `potentialIsStable_iff_forall_gramVector`, `potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`, `potentialIsStable_of_strong`, `potential_stabilityCounterExample`, `potential_zero`, `quarticTermReduced_nonneg_of_potentialIsStable`, `quarticTermReduced_stabilityCounterExample`, `quarticTermReduced_stabilityCounterExample_nonneg`, `quarticTermReduced_zero`, `quarticTerm_eq_gramVector`, `quarticTerm_stabilityCounterExample`, `quarticTerm_stabilityCounterExample_eq_norm_pow_four`, `quarticTerm_zero`, `quarticTerm_𝓵₄_expand`, `stabilityCounterExample_not_potentialIsStable`	43
Total	64

TwoHiggsDoublet

Definitions

Name	Category	Theorems
`PotentialIsStable` 📖	MathDef	8 math math: `potentialIsStable_iff_exists_forall_forall_reduced`, `potentialIsStable_iff_forall_euclid`, `stabilityCounterExample_not_potentialIsStable`, `forall_reduced_exists_not_potentialIsStable`, `potentialIsStable_of_strong`, `potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`, `potentialIsStable_iff_forall_euclid_lt`, `potentialIsStable_iff_forall_gramVector`
`PotentialParameters` 📖	CompData	17 math math: `quarticTerm_zero`, `PotentialParameters.zero_𝓵₁`, `massTerm_zero`, `PotentialParameters.zero_𝓵₅`, `PotentialParameters.η_zero`, `PotentialParameters.ξ_zero`, `potential_zero`, `PotentialParameters.zero_m₁₂2`, `massTermReduced_zero`, `PotentialParameters.zero_m₁₁2`, `PotentialParameters.zero_𝓵₄`, `PotentialParameters.zero_𝓵₃`, `quarticTermReduced_zero`, `PotentialParameters.zero_𝓵₆`, `PotentialParameters.zero_m₂₂2`, `PotentialParameters.zero_𝓵₇`, `PotentialParameters.zero_𝓵₂`
`massTerm` 📖	CompOp	5 math math: `massTerm_zero_of_quarticTerm_zero_stabilityCounterExample`, `massTerm_stabilityCounterExample`, `massTerm_eq_gramVector`, `massTerm_zero`, `gaugeGroupI_smul_massTerm`
`massTermReduced` 📖	CompOp	7 math math: `potentialIsStable_iff_exists_forall_forall_reduced`, `massTermReduced_pos_of_quarticTermReduced_zero_potentialIsStable`, `massTermReduced_lower_bound`, `forall_reduced_exists_not_potentialIsStable`, `massTermReduced_stabilityCounterExample`, `massTermReduced_zero`, `potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`
`potential` 📖	CompOp	3 math math: `potential_zero`, `potential_stabilityCounterExample`, `gaugeGroupI_smul_potential`
`quarticTerm` 📖	CompOp	6 math math: `quarticTerm_zero`, `gaugeGroupI_smul_quarticTerm`, `quarticTerm_stabilityCounterExample`, `quarticTerm_stabilityCounterExample_eq_norm_pow_four`, `quarticTerm_eq_gramVector`, `quarticTerm_𝓵₄_expand`
`quarticTermReduced` 📖	CompOp	7 math math: `potentialIsStable_iff_exists_forall_forall_reduced`, `forall_reduced_exists_not_potentialIsStable`, `quarticTermReduced_stabilityCounterExample_nonneg`, `quarticTermReduced_nonneg_of_potentialIsStable`, `quarticTermReduced_zero`, `potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`, `quarticTermReduced_stabilityCounterExample`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_reduced_exists_not_potentialIsStable` 📖	mathematical	—	`PotentialIsStable` `quarticTermReduced` `massTermReduced`	—	`stabilityCounterExample_not_potentialIsStable` `quarticTermReduced_stabilityCounterExample_nonneg` `quarticTermReduced_stabilityCounterExample` `massTermReduced_stabilityCounterExample`
`gaugeGroupI_smul_massTerm` 📖	mathematical	—	`massTerm` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI`	—	`massTerm_eq_gramVector` `gaugeGroupI_smul_fst_gramVector`
`gaugeGroupI_smul_potential` 📖	mathematical	—	`potential` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI`	—	`potential.eq_1` `gaugeGroupI_smul_massTerm` `gaugeGroupI_smul_quarticTerm`
`gaugeGroupI_smul_quarticTerm` 📖	mathematical	—	`quarticTerm` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI`	—	`quarticTerm_eq_gramVector` `gaugeGroupI_smul_fst_gramVector`
`massTermReduced_lower_bound` 📖	mathematical	—	`PotentialParameters.ξ` `massTermReduced`	—	—
`massTermReduced_pos_of_quarticTermReduced_zero_potentialIsStable` 📖	mathematical	`PotentialIsStable` `quarticTermReduced`	`massTermReduced`	—	`potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`
`massTermReduced_stabilityCounterExample` 📖	mathematical	—	`massTermReduced` `PotentialParameters.stabilityCounterExample`	—	—
`massTermReduced_zero` 📖	mathematical	—	`massTermReduced` `PotentialParameters` `PotentialParameters.instZero`	—	`PotentialParameters.ξ_zero`
`massTerm_eq_gramVector` 📖	mathematical	—	`massTerm` `PotentialParameters.ξ` `gramVector`	—	`normSq_Φ1_eq_gramVector` `normSq_Φ2_eq_gramVector` `Φ1_inner_Φ2_eq_gramVector` `Φ2_inner_Φ1_eq_gramVector`
`massTerm_stabilityCounterExample` 📖	mathematical	—	`massTerm` `PotentialParameters.stabilityCounterExample` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	—
`massTerm_zero` 📖	mathematical	—	`massTerm` `PotentialParameters` `PotentialParameters.instZero` `TwoHiggsDoublet`	—	—
`massTerm_zero_of_quarticTerm_zero_stabilityCounterExample` 📖	mathematical	`quarticTerm` `PotentialParameters.stabilityCounterExample`	`massTerm`	—	`massTerm_stabilityCounterExample` `quarticTerm_stabilityCounterExample_eq_norm_pow_four`
`potentialIsStable_iff_exists_forall_forall_reduced` 📖	mathematical	—	`PotentialIsStable` `massTermReduced` `quarticTermReduced`	—	`potentialIsStable_iff_forall_euclid_lt`
`potentialIsStable_iff_forall_euclid` 📖	mathematical	—	`PotentialIsStable` `PotentialParameters.ξ` `PotentialParameters.η`	—	`potentialIsStable_iff_forall_gramVector` `PotentialParameters.η_symm`
`potentialIsStable_iff_forall_euclid_lt` 📖	mathematical	—	`PotentialIsStable` `PotentialParameters.ξ` `PotentialParameters.η`	—	`potentialIsStable_iff_forall_euclid`
`potentialIsStable_iff_forall_gramVector` 📖	mathematical	—	`PotentialIsStable` `PotentialParameters.ξ` `PotentialParameters.η`	—	`gramVector_surjective` `potential.eq_1` `massTerm_eq_gramVector` `quarticTerm_eq_gramVector` `gramVector_inl_nonneg` `gramVector_inr_sum_sq_le_inl`
`potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced` 📖	mathematical	—	`PotentialIsStable` `quarticTermReduced` `massTermReduced`	—	`potentialIsStable_iff_exists_forall_forall_reduced` `quarticTermReduced_nonneg_of_potentialIsStable`
`potentialIsStable_of_strong` 📖	mathematical	`quarticTermReduced`	`PotentialIsStable`	—	`potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced`
`potential_stabilityCounterExample` 📖	mathematical	—	`potential` `PotentialParameters.stabilityCounterExample` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`massTerm_stabilityCounterExample` `quarticTerm_stabilityCounterExample_eq_norm_pow_four`
`potential_zero` 📖	mathematical	—	`potential` `PotentialParameters` `PotentialParameters.instZero` `TwoHiggsDoublet`	—	`massTerm_zero` `quarticTerm_zero`
`quarticTermReduced_nonneg_of_potentialIsStable` 📖	mathematical	`PotentialIsStable`	`quarticTermReduced`	—	`potentialIsStable_iff_exists_forall_forall_reduced`
`quarticTermReduced_stabilityCounterExample` 📖	mathematical	—	`quarticTermReduced` `PotentialParameters.stabilityCounterExample`	—	—
`quarticTermReduced_stabilityCounterExample_nonneg` 📖	mathematical	—	`quarticTermReduced` `PotentialParameters.stabilityCounterExample`	—	`quarticTermReduced_stabilityCounterExample`
`quarticTermReduced_zero` 📖	mathematical	—	`quarticTermReduced` `PotentialParameters` `PotentialParameters.instZero`	—	`PotentialParameters.η_zero`
`quarticTerm_eq_gramVector` 📖	mathematical	—	`quarticTerm` `gramVector` `PotentialParameters.η`	—	`quarticTerm_𝓵₄_expand` `normSq_Φ1_eq_gramVector` `normSq_Φ2_eq_gramVector` `Φ1_inner_Φ2_eq_gramVector` `Φ2_inner_Φ1_eq_gramVector`
`quarticTerm_stabilityCounterExample` 📖	mathematical	—	`quarticTerm` `PotentialParameters.stabilityCounterExample` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	—
`quarticTerm_stabilityCounterExample_eq_norm_pow_four` 📖	mathematical	—	`quarticTerm` `PotentialParameters.stabilityCounterExample` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`quarticTerm_stabilityCounterExample`
`quarticTerm_zero` 📖	mathematical	—	`quarticTerm` `PotentialParameters` `PotentialParameters.instZero` `TwoHiggsDoublet`	—	—
`quarticTerm_𝓵₄_expand` 📖	mathematical	—	`quarticTerm` `PotentialParameters.𝓵₁` `StandardModel.HiggsVec` `Φ1` `PotentialParameters.𝓵₂` `Φ2` `PotentialParameters.𝓵₃` `PotentialParameters.𝓵₄` `PotentialParameters.𝓵₅` `PotentialParameters.𝓵₆` `PotentialParameters.𝓵₇`	—	—
`stabilityCounterExample_not_potentialIsStable` 📖	mathematical	—	`PotentialIsStable` `PotentialParameters.stabilityCounterExample`	—	`potential.eq_1` `massTerm_stabilityCounterExample` `quarticTerm_stabilityCounterExample`

TwoHiggsDoublet.PotentialParameters

Definitions

Name	Category	Theorems
`instZero` 📖	CompOp	17 math math: `TwoHiggsDoublet.quarticTerm_zero`, `zero_𝓵₁`, `TwoHiggsDoublet.massTerm_zero`, `zero_𝓵₅`, `η_zero`, `ξ_zero`, `TwoHiggsDoublet.potential_zero`, `zero_m₁₂2`, `TwoHiggsDoublet.massTermReduced_zero`, `zero_m₁₁2`, `zero_𝓵₄`, `zero_𝓵₃`, `TwoHiggsDoublet.quarticTermReduced_zero`, `zero_𝓵₆`, `zero_m₂₂2`, `zero_𝓵₇`, `zero_𝓵₂`
`m₁₁2` 📖	CompOp	1 math math: `zero_m₁₁2`
`m₁₂2` 📖	CompOp	1 math math: `zero_m₁₂2`
`m₂₂2` 📖	CompOp	1 math math: `zero_m₂₂2`
`stabilityCounterExample` 📖	CompOp	8 math math: `TwoHiggsDoublet.massTerm_stabilityCounterExample`, `TwoHiggsDoublet.stabilityCounterExample_not_potentialIsStable`, `TwoHiggsDoublet.quarticTerm_stabilityCounterExample`, `TwoHiggsDoublet.massTermReduced_stabilityCounterExample`, `TwoHiggsDoublet.quarticTermReduced_stabilityCounterExample_nonneg`, `TwoHiggsDoublet.potential_stabilityCounterExample`, `TwoHiggsDoublet.quarticTerm_stabilityCounterExample_eq_norm_pow_four`, `TwoHiggsDoublet.quarticTermReduced_stabilityCounterExample`
`η` 📖	CompOp	6 math math: `TwoHiggsDoublet.potentialIsStable_iff_forall_euclid`, `η_zero`, `η_symm`, `TwoHiggsDoublet.quarticTerm_eq_gramVector`, `TwoHiggsDoublet.potentialIsStable_iff_forall_euclid_lt`, `TwoHiggsDoublet.potentialIsStable_iff_forall_gramVector`
`ξ` 📖	CompOp	6 math math: `TwoHiggsDoublet.potentialIsStable_iff_forall_euclid`, `TwoHiggsDoublet.massTerm_eq_gramVector`, `TwoHiggsDoublet.massTermReduced_lower_bound`, `ξ_zero`, `TwoHiggsDoublet.potentialIsStable_iff_forall_euclid_lt`, `TwoHiggsDoublet.potentialIsStable_iff_forall_gramVector`
`𝓵₁` 📖	CompOp	2 math math: `zero_𝓵₁`, `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`
`𝓵₂` 📖	CompOp	2 math math: `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`, `zero_𝓵₂`
`𝓵₃` 📖	CompOp	2 math math: `zero_𝓵₃`, `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`
`𝓵₄` 📖	CompOp	2 math math: `zero_𝓵₄`, `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`
`𝓵₅` 📖	CompOp	2 math math: `zero_𝓵₅`, `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`
`𝓵₆` 📖	CompOp	2 math math: `zero_𝓵₆`, `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`
`𝓵₇` 📖	CompOp	2 math math: `TwoHiggsDoublet.quarticTerm_𝓵₄_expand`, `zero_𝓵₇`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_m₁₁2` 📖	mathematical	—	`m₁₁2` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_m₁₂2` 📖	mathematical	—	`m₁₂2` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_m₂₂2` 📖	mathematical	—	`m₂₂2` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₁` 📖	mathematical	—	`𝓵₁` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₂` 📖	mathematical	—	`𝓵₂` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₃` 📖	mathematical	—	`𝓵₃` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₄` 📖	mathematical	—	`𝓵₄` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₅` 📖	mathematical	—	`𝓵₅` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₆` 📖	mathematical	—	`𝓵₆` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`zero_𝓵₇` 📖	mathematical	—	`𝓵₇` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`η_symm` 📖	mathematical	—	`η`	—	—
`η_zero` 📖	mathematical	—	`η` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—
`ξ_zero` 📖	mathematical	—	`ξ` `TwoHiggsDoublet.PotentialParameters` `instZero`	—	—

---

← Back to Index