phi_fifth_bounds
plain-language theorem explainer
The theorem establishes that the fifth power of the golden ratio satisfies 10.7 < phi^5 < 11.3. Cosmologists and device designers cite this bound for BAO scale predictions and alpha-band frequencies within the Recognition Science phi-ladder. The proof factors phi^5 as phi^4 times phi then applies nlinarith to the component bounds on phi^4 and phi.
Claim. $10.7 < phi^5 < 11.3$
background
This module supplies calculated proofs for items in the COMPLETE_PROBLEM_REGISTRY, including EU-003 (spectral index bounds from phi^3) and T-001 (H_0 > 0 from ln(phi)). It operates in the setting of the forcing chain where phi is the self-similar fixed point (T6) and powers of phi supply numerical yardsticks for predictions. The declaration relies on phi_fourth_bounds (6.5 < phi^4 < 6.9) together with the tighter inequalities phi > 1.61 and phi < 1.62 established in Constants.
proof idea
The tactic proof first rewrites phi^5 as phi^4 * phi via ring. It then pulls the lower bound 6.7 < phi^4 and upper bound phi^4 < 6.9 from phi_fourth_bounds, plus phi > 1.61 from phi_gt_onePointSixOne and phi < 1.62 from phi_lt_onePointSixTwo. Constructor splits the conjunction; nlinarith closes each side.
why it matters
The bound is invoked by cosmological_predictions_cert_exists, phi_fifth_in_alpha_band (for photobiomodulation), born_exponent_in_range (chemistry), and kappa_bounds (ZeroParameterGravity and NumericalPredictions). It supplies the explicit Phi powers entry in the module certificate for BAO predictions and closes numerical scaffolding in the T6 phi fixed point and eight-tick octave. No open question remains for this specific interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.