Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `accCube`, `accGrav`, `accQuad`, `accSU2`, `accSU3`, `accYY`, `cubeTriLin`, `quadBiLin`, `SMCharges`, `D`, `E`, `L`, `Q`, `U`, `toSpecies`, `toSpeciesEquiv`, `SMSpecies`	17
Theorems `accCube_ext`, `accGrav_ext`, `accQuad_ext`, `accSU2_ext`, `accSU3_ext`, `accYY_ext`, `cubeTriLin_toFun_apply_apply`, `quadBiLin_toFun_apply`, `charges_eq_toSpecies_eq`, `toSMSpecies_toSpecies_inv`, `toSpeciesEquiv_apply`, `toSpeciesEquiv_symm_apply`, `toSpecies_apply`, `SMCharges_numberCharges`, `SMSpecies_numberCharges`	15
Total	32

SMACCs

Definitions

Name	Category	Theorems
`accCube` 📖	CompOp	5 math math: `accCube_ext`, `SM.accCube_invariant`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SM.SMNoGrav.cubeSol`, `SM.SMNoGrav.One.linearParameters.cubic`
`accGrav` 📖	CompOp	8 math math: `SM.SMNoGrav.One.linearParametersQENeqZero.grav_of_cubic`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SM.SMNoGrav.One.linearParameters.grav`, `SM.SMNoGrav.One.accGravSatisfied`, `accGrav_ext`, `SM.accGrav_invariant`, `SM.SMNoGrav.One.accGrav_Q_zero`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`
`accQuad` 📖	CompOp	2 math math: `SM.accQuad_invariant`, `accQuad_ext`
`accSU2` 📖	CompOp	3 math math: `SM.accSU2_invariant`, `SM.SMNoGrav.SU2Sol`, `accSU2_ext`
`accSU3` 📖	CompOp	3 math math: `SM.SMNoGrav.SU3Sol`, `accSU3_ext`, `SM.accSU3_invariant`
`accYY` 📖	CompOp	2 math math: `accYY_ext`, `SM.accYY_invariant`
`cubeTriLin` 📖	CompOp	1 math math: `cubeTriLin_toFun_apply_apply`
`quadBiLin` 📖	CompOp	1 math math: `quadBiLin_toFun_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accCube_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`HomogeneousCubic` `HomogeneousCubic.instFun` `accCube`	—	—
`accGrav_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`accGrav`	—	—
`accQuad_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`HomogeneousQuadratic` `HomogeneousQuadratic.instFun` `accQuad`	—	`quadBiLin.eq_1`
`accSU2_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`accSU2`	—	—
`accSU3_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`accSU3`	—	—
`accYY_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `SMSpecies` `ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMCharges.toSpecies`	`accYY`	—	—
`cubeTriLin_toFun_apply_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `cubeTriLin`	—	—
`quadBiLin_toFun_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `quadBiLin`	—	—

SMCharges

Definitions

Name	Category	Theorems
`D` 📖	CompOp	—
`E` 📖	CompOp	3 math math: `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`
`L` 📖	CompOp	—
`Q` 📖	CompOp	3 math math: `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`
`U` 📖	CompOp	—
`toSpecies` 📖	CompOp	8 math math: `SM.toSpecies_sum_invariant`, `charges_eq_toSpecies_eq`, `SM.chargesMapOfSpeciesMap_apply`, `SM.chargeMap_apply`, `SM.repCharges_toSpecies`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `toSpecies_apply`, `toSMSpecies_toSpecies_inv`
`toSpeciesEquiv` 📖	CompOp	5 math math: `SM.chargesMapOfSpeciesMap_apply`, `SM.chargeMap_apply`, `toSpeciesEquiv_symm_apply`, `toSpeciesEquiv_apply`, `toSMSpecies_toSpecies_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charges_eq_toSpecies_eq` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSpecies`	—	—
`toSMSpecies_toSpecies_inv` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSpecies` `toSpeciesEquiv`	—	—
`toSpeciesEquiv_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `toSpeciesEquiv`	—	—
`toSpeciesEquiv_symm_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `toSpeciesEquiv`	—	—
`toSpecies_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSpecies`	—	—

(root)

Definitions

Name	Category	Theorems
`SMCharges` 📖	CompOp	32 math math: `SMACCs.quadBiLin_toFun_apply`, `SM.toSpecies_sum_invariant`, `SM.SMNoGrav_linearACCs`, `SM.SMNoGrav.One.accGrav_Q_neq_zero`, `SM.SMNoGrav.SU3Sol`, `SMCharges.charges_eq_toSpecies_eq`, `SM.SMNoGrav_cubicACC_apply`, `SM.SMNoGrav_quadraticACCs`, `SM.accSU2_invariant`, `SM.chargesMapOfSpeciesMap_apply`, `SM.SMNoGrav.One.linearParameters.grav`, `SM.SMNoGrav.One.accGravSatisfied`, `SMACCs.cubeTriLin_toFun_apply_apply`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.accQuad_invariant`, `SMCharges_numberCharges`, `SM.accCube_invariant`, `SM.chargeMap_apply`, `SM.accGrav_invariant`, `SMCharges.toSpeciesEquiv_symm_apply`, `SM.SMNoGrav.SU2Sol`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `SM.repCharges_toSpecies`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `SM.accYY_invariant`, `SMCharges.toSpeciesEquiv_apply`, `SM.accSU3_invariant`, `SMCharges.toSpecies_apply`, `SM.SMNoGrav.cubeSol`, `SMCharges.toSMSpecies_toSpecies_inv`, `SM.SMNoGrav.One.linearParameters.cubic`
`SMSpecies` 📖	CompOp	15 math math: `SM.toSpecies_sum_invariant`, `SMSpecies_numberCharges`, `SMCharges.charges_eq_toSpecies_eq`, `SM.chargesMapOfSpeciesMap_apply`, `SM.SMNoGrav.One.E_zero_iff_Q_zero`, `SM.chargeMap_apply`, `SM.speciesFamilyUniversial_apply`, `SM.speciesEmbed_apply`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `SM.SMNoGrav.One.linearParametersQENeqZero.grav`, `SM.repCharges_toSpecies`, `SM.SMNoGrav.One.linearParameters.speciesVal`, `SM.speciesFamilyProj_apply`, `SMCharges.toSpecies_apply`, `SMCharges.toSMSpecies_toSpecies_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SMCharges_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMCharges`	—	—
`SMSpecies_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMSpecies`	—	—

---

← Back to Index