correction_within_bounds
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 in Recognition Science
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.
scope and limits
- Does not derive the gallium rung value from the J-function or phi-ladder axioms.
- Does not incorporate experimental error bars on the measured capture rate.
- Does not address possible sterile-neutrino oscillation signatures.
- Does not compute the exact gap-resonance correction from first principles.
formal statement (Lean)
136theorem correction_within_bounds : sigma_rs / ga_capture_predicted > 0.75 := by
proof body
Term-mode proof.
137 rw [correction_factor]
138 norm_num
139
140/-! ## IV. The Anomaly Resolution -/
141
142/-- **THEOREM EA-003.7**: The Gallium anomaly is explained in RS. -/