gallium_anomaly_explained
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.