Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `TwoHiggsDoublet`, `instMulActionGaugeGroupI`, `instSMulGaugeGroupI`, `Φ1`, `Φ2`	5
Theorems `ext_of_fst_snd`, `ext_of_fst_snd_iff`, `gaugeGroupI_smul_fst`, `gaugeGroupI_smul_snd`	4
Total	9

TwoHiggsDoublet

Definitions

Name	Category	Theorems
`instMulActionGaugeGroupI` 📖	CompOp	—
`instSMulGaugeGroupI` 📖	CompOp	8 math math: `gaugeGroupI_smul_gramMatrix`, `gaugeGroupI_smul_quarticTerm`, `gaugeGroupI_smul_fst`, `gaugeGroupI_smul_massTerm`, `gaugeGroupI_smul_snd`, `gaugeGroupI_smul_potential`, `mem_orbit_gaugeGroupI_iff_gramMatrix`, `gaugeGroupI_smul_fst_gramVector`
`Φ1` 📖	CompOp	20 math math: `ext_of_fst_snd_iff`, `gramVector_inr_one_eq`, `massTerm_stabilityCounterExample`, `gaugeGroupI_smul_fst`, `quarticTerm_stabilityCounterExample`, `gramVector_inl_zero_eq`, `gaugeGroupI_exists_fst_eq`, `gaugeGroupI_exists_fst_eq_snd_eq`, `eq_fst_norm_of_eq_gramMatrix`, `gramMatrix_det_eq_real`, `normSq_Φ1_eq_gramVector`, `Φ2_inner_Φ1_eq_gramVector`, `potential_stabilityCounterExample`, `gramVector_inr_two_eq`, `quarticTerm_stabilityCounterExample_eq_norm_pow_four`, `gramVector_inr_zero_eq`, `Φ1_inner_Φ2_eq_gramVector`, `gramMatrix_det_eq`, `quarticTerm_𝓵₄_expand`, `Φ1_inner_Φ2_normSq_eq_gramVector`
`Φ2` 📖	CompOp	20 math math: `ext_of_fst_snd_iff`, `gramVector_inr_one_eq`, `massTerm_stabilityCounterExample`, `normSq_Φ2_eq_gramVector`, `quarticTerm_stabilityCounterExample`, `gramVector_inl_zero_eq`, `gaugeGroupI_exists_fst_eq`, `gaugeGroupI_exists_fst_eq_snd_eq`, `gramMatrix_det_eq_real`, `gaugeGroupI_smul_snd`, `Φ2_inner_Φ1_eq_gramVector`, `potential_stabilityCounterExample`, `gramVector_inr_two_eq`, `quarticTerm_stabilityCounterExample_eq_norm_pow_four`, `gramVector_inr_zero_eq`, `eq_snd_norm_of_eq_gramMatrix`, `Φ1_inner_Φ2_eq_gramVector`, `gramMatrix_det_eq`, `quarticTerm_𝓵₄_expand`, `Φ1_inner_Φ2_normSq_eq_gramVector`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_fst_snd` 📖	—	`Φ1` `Φ2`	—	—	—
`ext_of_fst_snd_iff` 📖	mathematical	—	`Φ1` `Φ2`	—	`ext_of_fst_snd`
`gaugeGroupI_smul_fst` 📖	mathematical	—	`Φ1` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI` `StandardModel.HiggsVec` `StandardModel.HiggsVec.instSMulGaugeGroupI`	—	—
`gaugeGroupI_smul_snd` 📖	mathematical	—	`Φ2` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI` `StandardModel.HiggsVec` `StandardModel.HiggsVec.instSMulGaugeGroupI`	—	—

(root)

Definitions

Name	Category	Theorems
`TwoHiggsDoublet` 📖	CompData	11 math math: `TwoHiggsDoublet.quarticTerm_zero`, `TwoHiggsDoublet.gaugeGroupI_smul_gramMatrix`, `TwoHiggsDoublet.gaugeGroupI_smul_quarticTerm`, `TwoHiggsDoublet.gaugeGroupI_smul_fst`, `TwoHiggsDoublet.massTerm_zero`, `TwoHiggsDoublet.gaugeGroupI_smul_massTerm`, `TwoHiggsDoublet.potential_zero`, `TwoHiggsDoublet.gaugeGroupI_smul_snd`, `TwoHiggsDoublet.gaugeGroupI_smul_potential`, `TwoHiggsDoublet.mem_orbit_gaugeGroupI_iff_gramMatrix`, `TwoHiggsDoublet.gaugeGroupI_smul_fst_gramVector`

---

← Back to Index