phi_fifth_bounds
Physicists modeling BAO scales or mass ladders cite the bound 10.7 < phi^5 < 11.3 when placing the fifth rung on the phi-ladder. The result composes the fourth-power interval 6.7 < phi^4 < 6.9 with the tighter phi interval 1.61 < phi < 1.62. The tactic proof rewrites the product via ring, extracts the component bounds, and closes both sides with nlinarith.
claim$10.7 < phi^5 < 11.3$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module supplies calculated proofs for cosmological predictions drawn from the COMPLETE_PROBLEM_REGISTRY, covering spectral index, Hubble positivity, and dark-energy bounds via explicit numerical intervals on powers of phi. Phi itself is the unique positive root of x^2 - x - 1 = 0, equipped with the interval lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo that tighten the classical bounds around 1.618. The local setting assumes the phi-forcing chain of the Foundation module, where phi emerges as the self-similar fixed point of the recognition cost J.
proof idea
The proof rewrites phi^5 as phi^4 * phi by ring. It pulls the lower and upper bounds on phi^4 directly from phi_fourth_bounds.1 and phi_fourth_bounds.2, and the bounds on phi from phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The conjunction is formed and both resulting inequalities are discharged by nlinarith.
why it matters in Recognition Science
This bound is invoked by cosmological_predictions_cert_exists to certify the full prediction set and supplies the numerical interval for kappa = 8 phi^5 in ZeroParameterGravity.kappa_bounds and for the Born-exponent proxy in IonicBond.born_exponent_in_range. It also anchors phi_fifth_in_alpha_band in the photobiomodulation device. Within the Recognition framework it supplies the phi^5 rung required by the eight-tick octave and D = 3 spatial dimensions of the forcing chain (T7-T8).
scope and limits
- Does not establish the exact algebraic value of phi^5.
- Does not derive the phi bounds from the J-function definition.
- Does not extend to complex or non-real embeddings of phi.
- Does not address higher powers or other constants beyond the supplied interval.
Lean usage
have h := phi_fifth_bounds; constructor <;> nlinarith [h.1, h.2]formal statement (Lean)
116theorem phi_fifth_bounds : (10.7 : ℝ) < (phi : ℝ)^(5 : ℕ) ∧ (phi : ℝ)^(5 : ℕ) < (11.3 : ℝ) := by
proof body
Tactic-mode proof.
117 have h1 : (phi : ℝ)^(5 : ℕ) = (phi : ℝ)^(4 : ℕ) * phi := by ring
118 rw [h1]
119 have h2 : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ) := phi_fourth_bounds.1
120 have h3 : (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ) := phi_fourth_bounds.2
121 have h4 : phi > (1.61 : ℝ) := phi_gt_onePointSixOne
122 have h5 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
123 constructor
124 · nlinarith
125 · nlinarith
126
127/-! ## Section: Certificate -/
128
129/-- **CERTIFICATE**: Cosmological predictions with calculated bounds.
130
131 **EU-003**: 0.5 < n_s < 1 (spectral index from φ³)
132 **T-001**: H₀ > 0 from ln(φ)
133 **Phi powers**: φ², φ⁴, φ⁵ bounds for various predictions
134
135 **All from φ with rigorous bounds.** -/