deficit_bounded
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the gallium rung on the φ-ladder.
- Does not compute the exact suppression factor φ^(-4.5).
- Does not address sterile-neutrino oscillation signatures.
formal statement (Lean)
55theorem deficit_bounded : ga_capture_ratio > 0.70 := by
proof body
Term-mode proof.
56 unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
57 norm_num
58
59/-! ## II. The φ-Ladder Structure -/
60
61/-- Gallium rung on the φ-ladder (from mass ~70 u). -/