deficit_real
plain-language theorem explainer
The theorem establishes that the gallium neutrino capture ratio falls below 0.85, confirming a genuine ~20% deficit relative to the standard-model prediction of 74 SNU. Solar-neutrino experimentalists would cite it when testing Recognition Science nuclear-structure corrections against GALLEX/SAGE data. The proof is a one-line wrapper that unfolds the three ratio definitions and discharges the numerical inequality by norm_num.
Claim. Let $r = 57.7 / 74.0$ be the ratio of measured to predicted gallium capture rates in SNU. Then $r < 0.85$.
background
The module EA-003 treats the solar-neutrino gallium anomaly as a nuclear-structure effect inside the Recognition Science phi-ladder. ga_capture_measured is the SAGE value 57.7 SNU; ga_capture_predicted is the BP04 standard-model value 74.0 SNU; their ratio ga_capture_ratio is therefore the observable that must be shown to lie below 0.85. Upstream lemmas such as EdgeLengthFromPsi.is and MechanismDesignFromSigma.is supply the combinatorial scaffolding that later links the rung index r_Ga to the suppression factor, but are not invoked in this numerical step.
proof idea
The term proof unfolds ga_capture_ratio, ga_capture_measured and ga_capture_predicted, then applies norm_num to reduce the concrete inequality 57.7 / 74.0 < 0.85 to a decidable numerical statement.
why it matters
deficit_real supplies the first concrete datum for the EA-003 certificate, which asserts that the gallium anomaly is resolved by phi-ladder suppression rather than sterile neutrinos. It sits at the experimental interface of the T5 J-uniqueness and T6 phi-fixed-point steps, converting the abstract rung r_Ga ≈ 4.5 into a falsifiable ratio bound. The downstream certificate string explicitly records this theorem as the anchor for the ~20% deficit claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.