deficit_bounded
plain-language theorem explainer
The theorem establishes that the gallium neutrino capture ratio exceeds 0.70, bounding the observed deficit at no more than 30 percent. Nuclear physicists modeling solar neutrino data would cite this to exclude catastrophic suppression. The proof reduces the ratio definition to numerical evaluation via unfolding and norm_num.
Claim. Let $r$ denote the ratio of measured to predicted gallium neutrino capture rates in solar units. Then $r > 0.70$.
background
The Gallium Anomaly module treats the solar neutrino deficit as a nuclear structure effect on the φ-ladder rather than new physics. Measured capture rate is fixed at 57.7 SNU and standard-model prediction at 74.0 SNU; their quotient defines the capture ratio. Upstream definitions ga_capture_measured, ga_capture_predicted and ga_capture_ratio supply these concrete values and the division.
proof idea
One-line wrapper that unfolds ga_capture_ratio, ga_capture_measured and ga_capture_predicted then applies norm_num to discharge the numerical inequality.
why it matters
The result feeds ea003_certificate, which certifies the full RS derivation of the gallium anomaly. It supplies the EA-003.2 step confirming the deficit remains bounded. The bound is consistent with the φ-suppression factor arising from the gallium rung on the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.