phi_fourth_bounds
Establishes 6.7 < φ⁴ < 6.9 for the golden ratio φ. Cosmologists deriving BAO scales or spectral indices from Recognition Science cite these bounds to anchor numerical predictions. The proof rewrites φ⁴ as (φ²)² and applies nlinarith to the sibling interval 2.59 < φ² < 2.62.
claim$6.7 < φ^4 ∧ φ^4 < 6.9$ where φ is the golden ratio satisfying 1.61 < φ < 1.62 and φ² = φ + 1.
background
The module supplies calculated proofs for cosmological predictions drawn from the COMPLETE_PROBLEM_REGISTRY, covering the primordial power spectrum index, dark energy density, and Hubble parameter. All proofs rely on explicit numerical intervals obtained from the golden ratio φ via the self-similar fixed point of the forcing chain. The scale map is defined by scale(k) := φ^k. The sibling theorem phi_squared_bounds supplies the prerequisite interval 2.59 < φ² < 2.62 obtained from 1.61 < φ < 1.62 together with the identity φ² = φ + 1.
proof idea
The tactic proof first rewrites φ⁴ as (φ²)² by ring. It obtains the lower bound from phi_squared_bounds.1 and the upper bound from phi_squared_bounds.2. Constructor splits the conjunction; each side is discharged by nlinarith.
why it matters in Recognition Science
The result is used by phi_fifth_bounds to produce the BAO-scale interval 10.7 < φ⁵ < 11.3 and by cosmological_predictions_cert_exists to witness the registry certificate. It supplies the calculated rung for the EU-003 spectral-index item. In the framework it converts the T6 self-similar fixed point and T7 eight-tick octave into concrete numerical bounds compatible with the observed α^{-1} band.
scope and limits
- Does not establish the exact algebraic value of φ⁴.
- Does not apply to bases other than the Recognition Science golden ratio.
- Does not replace the coarser 6.5–6.9 bounds proved in the Constants module.
- Assumes the φ² interval without re-deriving it from the forcing axioms.
Lean usage
have h : (6.7 : ℝ) < phi ^ 4 ∧ phi ^ 4 < (6.9 : ℝ) := phi_fourth_boundsformal statement (Lean)
103theorem phi_fourth_bounds : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ) ∧ (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ) := by
proof body
Tactic-mode proof.
104 have h1 : (phi : ℝ)^(4 : ℕ) = (phi ^ 2) ^ 2 := by ring
105 rw [h1]
106 have h2 : (2.59 : ℝ) < phi^2 := phi_squared_bounds.1
107 have h3 : phi^2 < (2.62 : ℝ) := phi_squared_bounds.2
108 constructor
109 · nlinarith
110 · nlinarith
111
112/-- **CALCULATED**: φ⁵ bounds (for BAO scale predictions).
113
114 φ⁵ = φ⁴ × φ, so with 6.7 < φ⁴ < 6.9 and 1.61 < φ < 1.62:
115 10.7 < φ⁵ < 11.3 -/