`sigma_nu_reference_cm2`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard
domain: Physics
line: 35 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard on GitHub at line 35.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  32noncomputable section
  33
  34/-- Protocol normalization for the neutrino-reference channel in cm^2. -/
  35def sigma_nu_reference_cm2 : ℝ := 1e-38
  36
  37/-- Absolute dark-matter cross-section prediction in cm^2. -/
  38def sigma_DM_cm2 : ℝ := sigma_DM_over_sigma_nu_RS * sigma_nu_reference_cm2
  39
  40theorem row_sigma_nu_reference_pos : 0 < sigma_nu_reference_cm2 := by
  41  unfold sigma_nu_reference_cm2
  42  norm_num
  43
  44theorem row_sigma_DM_cm2_band :
  45    1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39 := by
  46  unfold sigma_DM_cm2 sigma_nu_reference_cm2
  47  have h := row_sigma_ratio_band
  48  constructor
  49  · nlinarith [h.1]
  50  · nlinarith [h.2]
  51
  52structure DarkMatterAbsoluteCrossSectionScoreCardCert where
  53  sigma_nu_ref_pos : 0 < sigma_nu_reference_cm2
  54  sigma_ratio_band :
  55    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  56  sigma_absolute_band : 1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39
  57
  58theorem darkMatterAbsoluteCrossSectionScoreCardCert_holds :
  59    Nonempty DarkMatterAbsoluteCrossSectionScoreCardCert :=
  60  ⟨{ sigma_nu_ref_pos := row_sigma_nu_reference_pos
  61     sigma_ratio_band := row_sigma_ratio_band
  62     sigma_absolute_band := row_sigma_DM_cm2_band }⟩
  63
  64end
  65

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.