phi_neg_quarter_bounds
The theorem establishes that the reciprocal of the upper quarter-root bound lies below the golden ratio to the negative one-quarter power, which itself lies below the reciprocal of the lower quarter-root bound. Numerics code in Recognition Science applications cites it when chaining bounds for negative phi powers in mass formulas and decay estimates. The proof is a tactic sequence that invokes the positive quarter bounds, rewrites the negative exponent as a reciprocal, and applies the reciprocal inequality lemma twice before reassembling the ∧.
claimLet ϕ denote the golden ratio. Let ϕ_quarter_lo and ϕ_quarter_hi be the lower and upper bounds on ϕ^{1/4}. Then (1 / ϕ_quarter_hi) < ϕ^{-1/4} < (1 / ϕ_quarter_lo).
background
The module supplies rigorous algebraic bounds on powers of the golden ratio ϕ = (1 + √5)/2. It starts from the comparison 2.236² < 5 < 2.237² to obtain 2.236 < √5 < 2.237, then derives the quarter-root interval ϕ_quarter_lo < ϕ^{1/4} < ϕ_quarter_hi by taking fourth roots and refining decimal places as described in the module strategy paragraph.
proof idea
The proof obtains the positive quarter bounds from phi_quarter_bounds. It establishes positivity of goldenRatio via Real.goldenRatio_pos and of its positive quarter power via rpow_pos_of_pos. The negative exponent is rewritten as the reciprocal using rpow_neg. Two calls to one_div_lt_one_div_of_lt invert the inequalities on each side, after which constructor and simpa reassemble the conjunction while normalizing the exponent notation.
why it matters in Recognition Science
This supplies the inversion step for negative exponents on the phi-ladder, directly enabling the downstream results phi_neg2174_gt, phi_neg2174_lt and phi_neg58_lt that bound high negative powers for nucleosynthesis and complexity numerics. It supports the Recognition Science mass formula and the eight-tick octave by keeping all rational multiples of 1/4 under explicit control. No open scaffolding remains.
scope and limits
- Does not supply bounds for exponents outside rational multiples of 1/4.
- Does not assert that the interval is the narrowest possible.
- Does not extend to complex numbers or other base fields.
- Does not compute explicit decimal values of the bounds.
formal statement (Lean)
189theorem phi_neg_quarter_bounds :
190 (1 / phi_quarter_hi) < goldenRatio ^ (-(1/4 : ℝ)) ∧ goldenRatio ^ (-(1/4 : ℝ)) < (1 / phi_quarter_lo) := by
proof body
Tactic-mode proof.
191 have hq := phi_quarter_bounds
192 have hg0 : (0 : ℝ) ≤ goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
193 have hpos : (0 : ℝ) < goldenRatio ^ (4⁻¹ : ℝ) := by
194 have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
195 exact Real.rpow_pos_of_pos this _
196 have hneg : goldenRatio ^ (-(4⁻¹ : ℝ)) = (goldenRatio ^ (4⁻¹ : ℝ))⁻¹ := by
197 simpa using (Real.rpow_neg hg0 (4⁻¹ : ℝ))
198 have hlo : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) := by
199 simpa using hq.1
200 have hhi : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi := by
201 simpa using hq.2
202 have h_lower : (1 / phi_quarter_hi) < 1 / (goldenRatio ^ (4⁻¹ : ℝ)) :=
203 one_div_lt_one_div_of_lt hpos hhi
204 have h_upper : (1 / (goldenRatio ^ (4⁻¹ : ℝ))) < (1 / phi_quarter_lo) :=
205 one_div_lt_one_div_of_lt (by
206 have : (0 : ℝ) < phi_quarter_lo := by simp [phi_quarter_lo]; norm_num
207 exact this) hlo
208 -- `simp` normalizes `-(1/4)` to `-(4⁻¹)`
209 constructor
210 · simpa [hneg, one_div] using h_lower
211 · simpa [hneg, one_div] using h_upper
212
213/-! ## Powers of φ using the recurrence φ² = φ + 1 -/
214
215/-- φ² = φ + 1, so 2.618 < φ² < 2.619 -/