gallium_anomaly_explained
Neutrino experimentalists would cite the result that the gallium capture ratio satisfies |ratio - 0.80| < 0.10. The claim shows the observed ~22% deficit lies within the nuclear correction band near 0.80. The proof reduces the statement to numerical evaluation after unfolding the ratio from the measured 57.7 SNU and predicted 74.0 SNU values.
claim$|r - 0.80| < 0.10$ where $r$ is the ratio of measured gallium neutrino capture rate (57.7 SNU) to standard-model predicted rate (74.0 SNU).
background
The Gallium Anomaly module resolves the solar neutrino deficit observed in gallium experiments. ga_capture_measured is the SAGE value 57.7 SNU. ga_capture_predicted is the BP04 standard-model value 74.0 SNU. ga_capture_ratio is their quotient, yielding ~0.78 and a ~22% deficit. The module setting states that the phi-ladder rung near 4.5 modifies the capture cross-section to produce an overall factor ~0.80 after gap resonance, eliminating the need for sterile neutrinos. The upstream correction definition supplies the finite-N phi-ladder adjustment used in related bounds.
proof idea
Term-mode proof that unfolds ga_capture_ratio, ga_capture_measured, and ga_capture_predicted, then applies norm_num with abs_of_pos to confirm the numerical deviation bound.
why it matters in Recognition Science
The theorem supplies the final numerical check for EA-003.7 and feeds the ea003_certificate summary. It anchors the Recognition Science resolution of the gallium anomaly via nuclear phi-ladder structure, consistent with the T5 J-uniqueness and phi self-similar fixed point. It closes one link in the EA-003 chain while leaving open whether identical rung corrections appear in other solar neutrino detectors.
scope and limits
- Does not derive the gallium rung value from the phi-ladder axioms.
- Does not compute the explicit phi-suppression factor.
- Does not incorporate measurement systematic uncertainties.
- Does not address other solar neutrino experiments or oscillation channels.
formal statement (Lean)
143theorem gallium_anomaly_explained : |ga_capture_ratio - 0.80| < 0.10 := by
proof body
Term-mode proof.
144 unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
145 norm_num [abs_of_pos]
146
147/-- **THEOREM EA-003.8**: No sterile neutrinos are needed.
148 3 generations suffice with nuclear correction. -/