phi_fourth_bounds
plain-language theorem explainer
The theorem establishes strict numerical bounds 6.7 < phi^4 < 6.9 for the golden ratio in the reals. Cosmologists using Recognition Science for BAO scale or spectral index derivations cite these bounds when chaining phi-powers. The proof rewrites the fourth power as the square of the second power and closes both sides of the conjunction with nlinarith applied to the known phi-squared interval.
Claim. $6.7 < phi^4 < 6.9$ where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The module supplies calculated proofs for cosmological predictions drawn from the COMPLETE_PROBLEM_REGISTRY. It treats bounds on powers of phi as inputs to large-scale structure calculations, covering items such as the primordial power spectrum n_s, dark energy density, and Hubble tension positivity. All proofs rely on norm_num, nlinarith and positivity with explicit numerical intervals. Upstream, phi_squared_bounds supplies the interval 2.59 < phi^2 < 2.62 obtained from phi > 1.61, phi < 1.62 and the identity phi^2 = phi + 1. The scale definition in LargeScaleStructureFromRS sets scale(k) := phi^k, placing these bounds inside the phi-ladder used for mass and distance predictions.
proof idea
The tactic proof begins by rewriting phi^4 as (phi^2)^2 via ring. It then obtains the lower and upper bounds on phi^2 directly from the sibling theorem phi_squared_bounds. The constructor splits the target conjunction, after which nlinarith verifies each resulting inequality by monotonicity of squaring on the positive interval.
why it matters
The bound sits inside the chain of phi-power calculations that support cosmological predictions. It is invoked by phi_fifth_bounds to obtain the interval 10.7 < phi^5 < 11.3 needed for BAO scale work and by cosmological_predictions_cert_exists. In the Recognition Science setting it contributes to the proved entries for EU-003 (primordial spectrum bounds from phi) and T-001 (Hubble positivity), consistent with the phi-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.