deficit_bounded
plain-language theorem explainer
Experimental neutrino physicists cite this result to bound the gallium capture deficit at no more than thirty percent. The measured rate of 57.7 SNU against the 74 SNU prediction yields a ratio above 0.70. The proof reduces to unfolding the ratio definition followed by direct numerical verification.
Claim. The gallium neutrino capture ratio satisfies $57.7 / 74.0 > 0.70$.
background
The module resolves the gallium solar neutrino anomaly via nuclear structure in Recognition Science. The capture ratio is the quotient of the SAGE-measured rate (57.7 SNU) by the standard-model prediction (74 SNU). Upstream definitions supply these constants and the ratio itself as a noncomputable real.
proof idea
The term proof unfolds the three ratio and rate definitions then applies norm_num to discharge the numerical inequality.
why it matters
This theorem supplies the second half of the EA-003 bounding argument and feeds the ea003_certificate that attributes the anomaly to φ-ladder suppression of the cross-section. It confirms the deficit remains non-catastrophic, consistent with the rung-based mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.