theorem
proved
detectionMethodCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.ParticlePhysicsDepthFromRS on GitHub at line 24.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
21 | tracking | calorimetry | timeOfFlight | cherenkov | transitionRadiation
22 deriving DecidableEq, Repr, BEq, Fintype
23
24theorem detectionMethodCount : Fintype.card DetectionMethod = 5 := by decide
25
26/-- 6 quarks = cube faces. -/
27def quarkFlavors : ℕ := 6
28theorem quarkFlavors_eq_cubeFaces : quarkFlavors = 6 := rfl
29
30/-- 6 leptons = cube faces. -/
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