Pith. sign in

StandardModel

StandardModel modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

39 modules · 304 thm/lemma · 6289 lines
module thm lemma def lines papers
StandardModel.CKMExact 40 0 13 337 -
StandardModel.CKMFromCube 14 0 7 266 -
StandardModel.CKMMatrix 9 0 29 297 -
StandardModel.CKM_Cabibbo_Exact_RS 4 0 3 36 -
StandardModel.CPPhaseDerivation 12 0 6 232 -
StandardModel.ElectroweakBreaking 8 0 16 271 -
StandardModel.ElectroweakMassBridge 11 0 7 212 -
StandardModel.HiggsCoshBSMPredictions 10 0 6 240 -
StandardModel.HiggsEFTBridge 11 0 6 303 -
StandardModel.HiggsEFTLowEnergyLimit 1 0 1 114 -
StandardModel.HiggsObservableSkeleton 10 0 5 231 -
StandardModel.HiggsRungAssignment 8 0 8 220 -
StandardModel.HiggsYukawaBridge 7 0 3 182 -
StandardModel.Higgs_Coupling_RS 4 0 3 36 -
StandardModel.JarlskogInvariant 5 0 3 175 -
StandardModel.LongitudinalVectorScattering 7 0 7 202 -
StandardModel.NeutrinoMassHierarchy 12 4 19 334 -
StandardModel.PMNSMatrix 7 0 23 343 -
StandardModel.PMNS_Atmospheric_Theta23_RS 4 0 3 36 -
StandardModel.PMNS_Reactor_Theta13_RS 4 0 3 36 -
StandardModel.ProtonMass 4 2 6 88 -
StandardModel.Q3Representations 13 0 10 216 -
StandardModel.RS_STD_Structural_001 4 0 3 36 -
StandardModel.RS_STD_Structural_002 4 0 3 36 -
StandardModel.RS_STD_Structural_003 4 0 3 36 -
StandardModel.RS_STD_Structural_004 4 0 3 36 -
StandardModel.RS_STD_Structural_005 4 0 3 36 -
StandardModel.RS_STD_Structural_006 4 0 3 36 -
StandardModel.RS_STD_Structural_007 4 0 3 36 -
StandardModel.RS_STD_Structural_008 4 0 3 36 -
StandardModel.RS_STD_Structural_009 4 0 3 36 -
StandardModel.RS_STD_Structural_010 4 0 3 36 -
StandardModel.RelativisticDOF 23 0 22 335 -
StandardModel.StrongCP 7 0 14 322 -
StandardModel.SupersymmetryBreaking 2 0 10 248 -
StandardModel.WZMassRatio 5 0 18 228 -
StandardModel.WeakCoupling 7 1 1 123 -
StandardModel.WeinbergAngle 4 0 16 232 -
StandardModel.WeinbergAngle_Exact_RS 4 0 3 34 -

full source mirrored from github.com/jonwashburn/shape-of-logic