Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `GaugeGroup`, `GaugeGroupI`, `instInvolutiveStar`, `instStar`, `ofU1Subgroup`, `toSU2`, `toSU3`, `toU1`, `GaugeGroupQuot`, `GaugeGroupℤ₂`, `GaugeGroupℤ₃`, `GaugeGroupℤ₆`, `gaugeBundleI`, `gaugeGroupI_lie`, `gaugeGroup_lie`, `gaugeGroupℤ₂SubGroup`, `gaugeGroupℤ₃SubGroup`, `gaugeGroupℤ₆SubGroup`, `gaugeTransformI`	19
Theorems `ext`, `ext_iff`, `ofU1Subgroup_toSU2`, `ofU1Subgroup_toSU3`, `ofU1Subgroup_toU1`, `star_eq`, `star_toSU2`, `star_toSU3`, `star_toU1`	9
Total	28
⚠️ With sorry `GaugeGroupℤ₆`, `gaugeGroupℤ₆SubGroup`	2

StandardModel

Definitions

Name	Category	Theorems
`GaugeGroup` 📖	CompOp	—
`GaugeGroupI` 📖	CompOp	27 math math: `GaugeGroupI.star_toU1`, `TwoHiggsDoublet.gaugeGroupI_smul_gramMatrix`, `GaugeGroupI.star_toSU3`, `HiggsVec.gaugeGroupI_smul_inner`, `TwoHiggsDoublet.gaugeGroupI_smul_quarticTerm`, `TwoHiggsDoublet.gaugeGroupI_smul_fst`, `GaugeGroupI.star_eq`, `HiggsVec.gaugeGroupI_smul_eq`, `HiggsVec.gaugeGroupI_smul_phase_snd`, `TwoHiggsDoublet.gaugeGroupI_exists_fst_eq`, `TwoHiggsDoublet.gaugeGroupI_smul_massTerm`, `TwoHiggsDoublet.gaugeGroupI_exists_fst_eq_snd_eq`, `TwoHiggsDoublet.gaugeGroupI_smul_snd`, `GaugeGroupI.star_toSU2`, `HiggsVec.mem_orbit_gaugeGroupI_iff`, `HiggsVec.gaugeGroupI_smul_eq_U1_smul_SU2`, `GaugeGroupI.ofU1Subgroup_toSU2`, `HiggsVec.gaugeGroupI_smul_eq_U1_mul_SU2`, `TwoHiggsDoublet.gaugeGroupI_smul_potential`, `HiggsVec.gaugeGroupI_smul_norm`, `GaugeGroupI.ext_iff`, `HiggsVec.ofU1Subgroup_smul_eq_smul`, `GaugeGroupI.ofU1Subgroup_toU1`, `TwoHiggsDoublet.mem_orbit_gaugeGroupI_iff_gramMatrix`, `GaugeGroupI.ofU1Subgroup_toSU3`, `HiggsVec.toRealGroupElem_smul_self`, `TwoHiggsDoublet.gaugeGroupI_smul_fst_gramVector`
`GaugeGroupQuot` 📖	CompData	—
`GaugeGroupℤ₂` 📖	CompOp	—
`GaugeGroupℤ₃` 📖	CompOp	—
`GaugeGroupℤ₆` 📖 ⚠️	CompOp	—
`gaugeBundleI` 📖	CompOp	—
`gaugeGroupI_lie` 📖	CompOp	—
`gaugeGroup_lie` 📖	CompOp	—
`gaugeGroupℤ₂SubGroup` 📖	CompOp	—
`gaugeGroupℤ₃SubGroup` 📖	CompOp	—
`gaugeGroupℤ₆SubGroup` 📖 ⚠️	CompOp	—
`gaugeTransformI` 📖	CompOp	—

StandardModel.GaugeGroupI

Definitions

Name	Category	Theorems
`instInvolutiveStar` 📖	CompOp	—
`instStar` 📖	CompOp	4 math math: `star_toU1`, `star_toSU3`, `star_eq`, `star_toSU2`
`ofU1Subgroup` 📖	CompOp	4 math math: `ofU1Subgroup_toSU2`, `StandardModel.HiggsVec.ofU1Subgroup_smul_eq_smul`, `ofU1Subgroup_toU1`, `ofU1Subgroup_toSU3`
`toSU2` 📖	CompOp	6 math math: `StandardModel.HiggsVec.gaugeGroupI_smul_eq`, `star_toSU2`, `StandardModel.HiggsVec.gaugeGroupI_smul_eq_U1_smul_SU2`, `ofU1Subgroup_toSU2`, `StandardModel.HiggsVec.gaugeGroupI_smul_eq_U1_mul_SU2`, `ext_iff`
`toSU3` 📖	CompOp	3 math math: `star_toSU3`, `ext_iff`, `ofU1Subgroup_toSU3`
`toU1` 📖	CompOp	6 math math: `star_toU1`, `StandardModel.HiggsVec.gaugeGroupI_smul_eq`, `StandardModel.HiggsVec.gaugeGroupI_smul_eq_U1_smul_SU2`, `StandardModel.HiggsVec.gaugeGroupI_smul_eq_U1_mul_SU2`, `ext_iff`, `ofU1Subgroup_toU1`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`StandardModel.GaugeGroupI` `toSU3` `toSU2` `toU1`	—	—	—
`ext_iff` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toSU3` `toSU2` `toU1`	—	`ext`
`ofU1Subgroup_toSU2` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toSU2` `ofU1Subgroup`	—	—
`ofU1Subgroup_toSU3` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toSU3` `ofU1Subgroup`	—	—
`ofU1Subgroup_toU1` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toU1` `ofU1Subgroup`	—	—
`star_eq` 📖	mathematical	—	`StandardModel.GaugeGroupI` `instStar`	—	—
`star_toSU2` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toSU2` `instStar`	—	—
`star_toSU3` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toSU3` `instStar`	—	—
`star_toU1` 📖	mathematical	—	`StandardModel.GaugeGroupI` `toU1` `instStar`	—	—

---

← Back to Index