phi5_bounds
plain-language theorem explainer
The golden ratio φ satisfies 10 < φ^5 < 12. Nuclear physicists using the Recognition Science bridge from QCD string tension to the semi-empirical mass formula cite this interval to anchor the φ-ladder mass formula and the Z_cf threshold. The proof is a direct numerical chaining that imports the lemmas 1.61 < φ < 1.62 and applies the monotonicity of x ↦ x^5 together with norm_num comparisons.
Claim. $10 < φ^5 ∧ φ^5 < 12$
background
The QCD-to-Nuclear Bridge module starts from the Recognition Science description of the strong force (α_s = 2/17 from wallpaper groups and string tension σ = φ^{-5}) and derives the coefficients of the semi-empirical mass formula. The golden ratio φ is the self-similar fixed point forced by the T6 step of the Unified Forcing Chain. Upstream lemmas in Constants supply the tight numerical bounds: phi_gt_onePointSixOne states “Even tighter lower bound: φ > 1.61” and phi_lt_onePointSixTwo states “Tighter upper bound: φ < 1.62 (since √5 < 2.24)”.
proof idea
The tactic proof first obtains the hypotheses 1.61 < φ and φ < 1.62 from phi_gt_onePointSixOne and phi_lt_onePointSixTwo. It then splits the conjunction and applies pow_lt_pow_left₀ with norm_num to show 10 < 1.61^5 < φ^5 for the lower bound and φ^5 < 1.62^5 < 12 for the upper bound.
why it matters
stringTension_bounds imports this result to conclude 0.08 < stringTension < 0.11, which in turn feeds the Cornell potential and volume/surface coefficients of the SEMF. The interval φ^5 ∈ (10,12) supplies the concrete numerical value required by the mass formula yardstick · φ^(rung-8+gap(Z)) and by the dream fraction φ^{-3}, closing the link from the T6 phi fixed point through the eight-tick octave to nuclear scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.