CRComposition

formal source

  21namespace IndisputableMonolith.Physics.CosmicRaysFromPhiLadder
  22open Constants
  23
  24inductive CRComposition where
  25  | protons | helium | CNO | iron | ultraHeavy
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem crCompositionCount : Fintype.card CRComposition = 5 := by decide
  29
  30/-- Spectral index γ = 1 + φ ∈ (2.61, 2.63). -/
  31noncomputable def spectralIndex : ℝ := 1 + phi
  32
  33theorem spectralIndexBand :
  34    (2.61 : ℝ) < spectralIndex ∧ spectralIndex < 2.63 := by
  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