Documentation Verification Report

FamilyMaps

📁 Source: PhysLean/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean

Statistics

Metric	Count
Definitions `chargesMapOfSpeciesMap`, `familyEmbedding`, `familyProjection`, `familyUniversal`, `speciesEmbed`, `speciesFamilyProj`, `speciesFamilyUniversial`	7
Theorems `chargesMapOfSpeciesMap_apply`, `chargesMapOfSpeciesMap_toSpecies`, `familyUniversal_accCube`, `familyUniversal_accGrav`, `familyUniversal_accQuad`, `familyUniversal_accSU2`, `familyUniversal_accSU3`, `familyUniversal_accYY`, `familyUniversal_cubeTriLin`, `familyUniversal_cubeTriLin'`, `familyUniversal_quadBiLin`, `speciesEmbed_apply`, `speciesFamilyProj_apply`, `speciesFamilyUniversial_apply`, `sum_familyUniversal`, `sum_familyUniversal_one`, `sum_familyUniversal_three`, `sum_familyUniversal_two`, `toSpecies_familyUniversal`	19
Total	26

SMRHN

Definitions

Name	Category	Theorems
`chargesMapOfSpeciesMap` 📖	CompOp	2 math math: `chargesMapOfSpeciesMap_toSpecies`, `chargesMapOfSpeciesMap_apply`
`familyEmbedding` 📖	CompOp	—
`familyProjection` 📖	CompOp	—
`familyUniversal` 📖	CompOp	16 math math: `sum_familyUniversal_one`, `toSpecies_familyUniversal`, `sum_familyUniversal_three`, `familyUniversal_quadBiLin`, `familyUniversal_accSU2`, `PlusU1.Y_val`, `PlusU1.BL_val`, `familyUniversal_accCube`, `familyUniversal_accGrav`, `sum_familyUniversal`, `sum_familyUniversal_two`, `familyUniversal_accQuad`, `familyUniversal_accSU3`, `familyUniversal_cubeTriLin'`, `familyUniversal_accYY`, `familyUniversal_cubeTriLin`
`speciesEmbed` 📖	CompOp	1 math math: `speciesEmbed_apply`
`speciesFamilyProj` 📖	CompOp	1 math math: `speciesFamilyProj_apply`
`speciesFamilyUniversial` 📖	CompOp	1 math math: `speciesFamilyUniversial_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chargesMapOfSpeciesMap_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `chargesMapOfSpeciesMap` `SMνCharges.toSpeciesEquiv` `SMνSpecies` `SMνCharges.toSpecies`	—	—
`chargesMapOfSpeciesMap_toSpecies` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `SMνSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `chargesMapOfSpeciesMap`	—	`SMνCharges.toSMSpecies_toSpecies_inv`
`familyUniversal_accCube` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `SMνACCs.accCube` `familyUniversal`	—	`SMνACCs.accCube_decomp` `sum_familyUniversal`
`familyUniversal_accGrav` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accGrav` `familyUniversal`	—	`SMνACCs.accGrav_decomp` `sum_familyUniversal_one`
`familyUniversal_accQuad` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `SMνACCs.accQuad` `familyUniversal`	—	`SMνACCs.accQuad_decomp` `sum_familyUniversal`
`familyUniversal_accSU2` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accSU2` `familyUniversal`	—	`SMνACCs.accSU2_decomp` `sum_familyUniversal_one`
`familyUniversal_accSU3` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accSU3` `familyUniversal`	—	`SMνACCs.accSU3_decomp` `sum_familyUniversal_one`
`familyUniversal_accYY` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνACCs.accYY` `familyUniversal`	—	`SMνACCs.accYY_decomp` `sum_familyUniversal_one`
`familyUniversal_cubeTriLin` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `familyUniversal` `ACCSystemCharges.numberCharges` `SMνSpecies` `SMνCharges.Q` `SMνCharges.U` `SMνCharges.D` `SMνCharges.L` `SMνCharges.E` `SMνCharges.N`	—	`SMνACCs.cubeTriLin_decomp` `sum_familyUniversal_three` `SMνCharges.toSpecies_one`
`familyUniversal_cubeTriLin'` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `SMνACCs.cubeTriLin` `familyUniversal` `ACCSystemCharges.numberCharges` `SMνSpecies` `SMνCharges.Q` `SMνCharges.U` `SMνCharges.D` `SMνCharges.L` `SMνCharges.E` `SMνCharges.N`	—	`familyUniversal_cubeTriLin` `sum_familyUniversal_two` `SMνCharges.toSpecies_one`
`familyUniversal_quadBiLin` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `SMνACCs.quadBiLin` `familyUniversal` `ACCSystemCharges.numberCharges` `SMνSpecies` `SMνCharges.Q` `SMνCharges.U` `SMνCharges.D` `SMνCharges.L` `SMνCharges.E`	—	`SMνACCs.quadBiLin_decomp` `sum_familyUniversal_two` `SMνCharges.toSpecies_one`
`speciesEmbed_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesEmbed`	—	—
`speciesFamilyProj_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesFamilyProj`	—	—
`speciesFamilyUniversial_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesFamilyUniversial`	—	—
`sum_familyUniversal` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMνSpecies` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `familyUniversal`	—	`toSpecies_familyUniversal`
`sum_familyUniversal_one` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMνSpecies` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `familyUniversal`	—	`sum_familyUniversal`
`sum_familyUniversal_three` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMνSpecies` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `familyUniversal`	—	`toSpecies_familyUniversal`
`sum_familyUniversal_two` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `SMνSpecies` `ACCSystemCharges.Charges` `SMνCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `familyUniversal`	—	`toSpecies_familyUniversal`
`toSpecies_familyUniversal` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMνCharges` `SMνSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `SMνCharges.toSpecies` `familyUniversal` `ACCSystemCharges.numberCharges`	—	`chargesMapOfSpeciesMap_toSpecies`

---

← Back to Index