gallium_rung
plain-language theorem explainer
Gallium receives rung 45 on the φ-ladder, fixed from its atomic mass near 70 u. Researchers modeling the solar neutrino deficit in gallium detectors cite this rung to obtain the suppression factor φ^(-4.5). The entry is a direct constant assignment with no internal computation or lemmas.
Claim. The rung index for gallium on the φ-ladder is defined as 45.
background
The Gallium Anomaly module treats the observed 20% deficit in Ga neutrino capture (55-58 SNU measured against 74 SNU predicted) as a nuclear φ-ladder effect rather than sterile neutrinos. Gallium mass places it at rung 45, which scales to an effective exponent -4.5 once divided by 10 in the suppression formula. This construction draws on the Recognition Composition Law and the self-similar fixed point φ from the forcing chain steps T5-T6. The imported 'for' structure records the meta-realization properties required by the orbit and step coherence axioms.
proof idea
The definition is a direct constant assignment of the natural number 45. No lemmas are invoked and no tactics are applied beyond the declaration itself.
why it matters
The value feeds directly into phi_suppression_ga, which sets the suppression to φ raised to minus (gallium_rung over 10), and into the bounding theorem phi_suppression_bounded that places the factor strictly inside (0,1). It supplies the numerical input for the EA-003 derivation that attributes the gallium anomaly to φ-ladder nuclear structure, consistent with the eight-tick octave and D=3 from T7-T8. The assignment leaves open the exact mapping from the mass formula yardstick times φ to the rung index.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.