phi_suppression_bounded
plain-language theorem explainer
The theorem establishes that the gallium φ-suppression factor lies strictly between zero and one. Neutrino experimentalists modeling the gallium anomaly would cite it to bound the nuclear correction to the capture cross-section. The proof reduces the claim to positivity of real powers and a comparison showing the base-φ exponent 4.5 exceeds unity.
Claim. $0 < φ^{-4.5} < 1$, where the exponent -4.5 arises from the gallium rung on the φ-ladder and φ denotes the golden ratio.
background
In the Gallium Anomaly module the RS framework resolves the solar neutrino deficit by assigning gallium a rung on the φ-ladder. The sibling definition gallium_rung sets this rung to the natural number 45. The companion definition phi_suppression_ga then sets the suppression factor to phi raised to the real power (-gallium_rung / 10), which simplifies to phi^(-4.5). The module states that this factor, after gap-resonance modification, accounts for the observed ~20% deficit relative to the Standard Model prediction of 74 SNU.
proof idea
The tactic proof first unfolds phi_suppression_ga and gallium_rung, then applies norm_num to obtain equality with phi^(-4.5). Positivity is immediate from Real.rpow_pos_of_pos using the upstream fact phi_pos. The upper bound rewrites the negative exponent as a reciprocal, proves phi^(4.5) > 1 by comparing to (1.618)^4.5 via repeated rpow_lt_rpow and linarith, and finishes with div_lt_iff together with nlinarith.
why it matters
The result supplies the strict bounds required by the EA-003 certificate, which records that the gallium anomaly is resolved by nuclear φ-ladder structure. It is invoked directly by the downstream theorem no_sterile_needed to extract the positivity conjunct. Within the Recognition framework the bound closes the suppression estimate at rung 4.5 on the φ-ladder, consistent with the self-similar fixed point and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.