pith. machine review for the scientific record. sign in
def definition def or abbrev high

gev2_to_cm2

show as:
view Lean formalization →

The definition supplies the numerical conversion 0.3894 × 10^{-27} that turns GeV^{-2} into cm². Dark-matter cross-section modelers cite it when scaling the Fermi-constant prediction to laboratory units for the P0-A6 weak reference channel. It is introduced as a bare constant assignment with no lemmas or reduction steps.

claimThe conversion factor satisfying $1~mathrm{GeV}^{-2} = 0.3894 times 10^{-27}~mathrm{cm}^{2}$.

background

The module implements the P0-A6 scorecard for the weak neutrino-reference cross-section. Module documentation states the reference formula sigma_nu_ref = G_F^2 * E_ref^2 * (GeV^{-2} to cm² conversion) with E_ref = 1 GeV, yielding the interval 5.2e-38 < sigma_nu_ref < 5.4e-38 cm² and the derived dark-matter band 5.7e-39 < sigma_DM < 7.1e-39 cm² from J(phi).

proof idea

One-line definition that directly assigns the numerical value 0.3894e-27.

why it matters in Recognition Science

It supplies the unit conversion required by the downstream definition sigma_nu_weak_ref_cm2 and is unfolded inside the proof of row_weak_ref_cross_section_band. The module documentation identifies this step as completing the arithmetic for the P0-A6 hypothesis interface, which normalizes the dark-matter cross-section band via the Recognition Composition Law and the phi-ladder mass formula.

scope and limits

formal statement (Lean)

  44def gev2_to_cm2 : ℝ := 0.3894e-27

proof body

Definition body.

  45
  46/-- Named weak-channel reference cross-section in cm^2. -/

used by (2)

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