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

sigma_rs

show as:
view Lean formalization →

The RS cross-section for gallium neutrino capture is defined by scaling the standard model prediction of 74 SNU by the fixed ratio 57.7/74.0. Nuclear physicists addressing the gallium anomaly would cite this scaled value to obtain an RS-adjusted rate near 58 SNU. The definition performs a direct numerical multiplication of the upstream predicted capture rate.

claim$σ_{RS} = σ_{SM} × (57.7 / 74.0)$, where $σ_{SM}$ is the standard model predicted Ga(ν,e)Ge capture rate in solar neutrino units.

background

The gallium anomaly module treats the observed ~20% deficit in solar neutrino capture rates on gallium targets. Standard model calculations give 74 SNU while measurements fall in 55-58 SNU. Recognition Science resolves the discrepancy by nuclear φ-ladder structure that suppresses the cross-section by a factor near 0.8 for gallium rung ~4.5. The upstream definition ga_capture_predicted supplies the base value 74.0 SNU drawn from the BP04 solar model.

proof idea

The definition is a direct arithmetic scaling that multiplies ga_capture_predicted by the constant ratio 57.7/74.0.

why it matters in Recognition Science

This definition supplies the explicit RS cross-section that feeds correction_factor, rs_matches_measurement, and ssm_plus_rs_equals_obs. It completes the EA-003.4 step in the gallium anomaly derivation, confirming that φ-ladder suppression accounts for the deficit without sterile neutrinos. The value lies in the 55-65 SNU band used for solar-model-independent checks.

scope and limits

formal statement (Lean)

 123noncomputable def sigma_rs : ℝ := ga_capture_predicted * (57.7 / 74.0)

proof body

Definition body.

 124
 125/-- **THEOREM EA-003.4**: The RS cross-section matches measurement. -/

used by (5)

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

depends on (1)

Lean names referenced from this declaration's body.