deficit_real
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the phi-ladder rung for gallium from first principles.
- Does not compute the gap-resonance correction that raises the raw phi^(-4.5) factor to ~0.8.
- Does not address L/E-dependent oscillation signatures that would distinguish sterile neutrinos.
- Does not extend the bound to other solar-neutrino experiments such as SNO or Borexino.
formal statement (Lean)
49theorem deficit_real : ga_capture_ratio < 0.85 := by
proof body
Term-mode proof.
50 unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
51 norm_num
52
53/-- **THEOREM EA-003.2**: The deficit is bounded (not catastrophic).
54 Ratio > 0.70 means ~30% max deficit. -/