Lemmas

📁 Source: PhysLean/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems E_zero_iff_Q_zero, accGravSatisfied, accGrav_Q_neq_zero, accGrav_Q_zero	4
Total	4

SM.SMNoGrav.One

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
E_zero_iff_Q_zero 📖	mathematical	—	ACCSystemCharges.Charges SMCharges SMSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMCharges.Q ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemQuad.QuadSols.toLinSols ACCSystem.Sols.toQuadSols SMCharges.E	—	SM.SMNoGrav.cubeSol linearParameters.cubic_zero_Q'_zero linearParameters.cubic_zero_E'_zero
accGravSatisfied 📖	mathematical	—	ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMACCs.accGrav ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemQuad.QuadSols.toLinSols ACCSystem.Sols.toQuadSols	—	accGrav_Q_zero accGrav_Q_neq_zero
accGrav_Q_neq_zero 📖	mathematical	—	ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMACCs.accGrav ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemQuad.QuadSols.toLinSols ACCSystem.Sols.toQuadSols	—	E_zero_iff_Q_zero SM.SMNoGrav.cubeSol linearParametersQENeqZero.grav_of_cubic
accGrav_Q_zero 📖	mathematical	ACCSystemCharges.Charges SMCharges SMSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMCharges.Q ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemQuad.QuadSols.toLinSols ACCSystem.Sols.toQuadSols	SMACCs.accGrav	—	SMACCs.accGrav.eq_1 E_zero_iff_Q_zero SM.SMNoGrav.SU2Sol SM.SMNoGrav.SU3Sol

---

← Back to Index