structure
definition
ParticlePhysicsDepthCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ParticlePhysicsDepthFromRS on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31def leptonFlavors : ℕ := 6
32theorem leptonFlavors_eq_cubeFaces : leptonFlavors = 6 := rfl
33
34structure ParticlePhysicsDepthCert where
35 five_detectors : Fintype.card DetectionMethod = 5
36 six_quarks : quarkFlavors = 6
37 six_leptons : leptonFlavors = 6
38
39def particlePhysicsDepthCert : ParticlePhysicsDepthCert where
40 five_detectors := detectionMethodCount
41 six_quarks := quarkFlavors_eq_cubeFaces
42 six_leptons := leptonFlavors_eq_cubeFaces
43
44end IndisputableMonolith.Physics.ParticlePhysicsDepthFromRS