correction_within_bounds
plain-language theorem explainer
The theorem establishes that the RS-modified gallium neutrino capture cross-section exceeds 75 percent of the standard-model prediction. Nuclear physicists analyzing the solar neutrino deficit would cite this bound to confirm that φ-ladder suppression accounts for the observed shortfall without new particles. The proof is a one-line wrapper that substitutes the correction-factor equality and evaluates the resulting numerical inequality.
Claim. $σ_{RS} / σ_{pred} > 0.75$, where $σ_{RS}$ is the recognition-science cross-section for Ga(ν,e)Ge and $σ_{pred}$ is the standard-model prediction of 74 SNU.
background
The Gallium Anomaly module derives the neutrino capture deficit from nuclear φ-ladder structure. ga_capture_predicted is the constant 74.0 SNU from the BP04 solar model. sigma_rs is defined as ga_capture_predicted multiplied by the factor 57.7/74.0, which encodes the φ-suppression arising from the rung structure of the gallium nucleus. correction_factor states that the ratio sigma_rs / ga_capture_predicted equals exactly 57.7/74.0. This theorem follows directly after that equality and precedes the EA-003 certificate that summarizes the full resolution.
proof idea
The proof is a one-line wrapper that rewrites the goal using the correction_factor theorem, which substitutes the explicit ratio 57.7/74.0, then applies norm_num to verify the numerical inequality 0.78 > 0.75 holds.
why it matters
This declaration completes EA-003.6 and feeds the ea003_certificate, which declares the gallium anomaly resolved through nuclear φ-ladder structure with an overall correction near 0.80. It confirms the suppression factor stays inside the φ^(-4.5) band modified by gap resonances, consistent with the 20 percent deficit. The result supports the Recognition Science claim that the anomaly is a nuclear-structure effect rather than evidence for sterile neutrinos, closing one step in the experimental verification chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.