structure
definition
CosmicRayCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CosmicRaysFromPhiLadder on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35 unfold spectralIndex
36 exact ⟨by linarith [phi_gt_onePointSixOne], by linarith [phi_lt_onePointSixTwo]⟩
37
38structure CosmicRayCert where
39 five_compositions : Fintype.card CRComposition = 5
40 spectral_index_band : (2.61 : ℝ) < spectralIndex ∧ spectralIndex < 2.63
41
42noncomputable def cosmicRayCert : CosmicRayCert where
43 five_compositions := crCompositionCount
44 spectral_index_band := spectralIndexBand
45
46end IndisputableMonolith.Physics.CosmicRaysFromPhiLadder