theorem proved term proof

`row_sigma_DM_cm2_band`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  44theorem row_sigma_DM_cm2_band :
  45    1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39 := by

proof body

Term-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

darkMatterAbsoluteCrossSectionScoreCardCert_holds in IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard decl_use

depends on (3)

Lean names referenced from this declaration's body.

sigma_DM_cm2 in IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard decl_use
sigma_nu_reference_cm2 in IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard decl_use
row_sigma_ratio_band in IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard decl_use