no_sterile_needed
plain-language theorem explainer
The theorem establishes that the gallium phi-suppression factor is strictly positive. Nuclear physicists resolving the gallium neutrino deficit would cite it to confirm that three generations plus nuclear phi-ladder corrections account for the observed capture shortfall. The proof is a direct term projection of the first conjunct from the boundedness theorem on the same factor.
Claim. $phi^{-r_{Ga}/10} > 0$, where $r_{Ga}$ denotes the gallium rung on the phi-ladder and the left-hand side is the nuclear suppression factor for neutrino capture cross-section.
background
The GalliumAnomaly module resolves the ~20% deficit between Standard Solar Model prediction (74 SNU) and measured Ga capture rates (55-58 SNU) by nuclear phi-ladder structure. The definition phi_suppression_ga := phi ^ (-(gallium_rung : ℝ) / 10) supplies the suppression factor; upstream phi_suppression_bounded proves this quantity lies in (0,1) by direct substitution and positivity of real powers. The Model structure from LawOfExistence supplies the underlying constants and defect/ortho masses used to derive rung values.
proof idea
One-line term proof that applies the first projection of the conjunction proved in phi_suppression_bounded.
why it matters
It supplies EA-003.8 in the gallium anomaly derivation, feeding directly into the ea003_certificate that declares the anomaly resolved by nuclear phi-ladder structure rather than sterile neutrinos. The result closes the chain from phi_suppression_ga through boundedness to the certificate statement that three generations suffice. It instantiates the Recognition Science claim that experimental deficits are absorbed by phi-ladder corrections without new particles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.