phi_cubed_bounds
Researchers modeling EEG bands or photobiomodulation devices cite this lemma to locate phi cubed inside the theta range. The claim 4 < phi^3 < 4.25 follows from the reduction phi^3 = 2 phi + 1 together with the interval 1.5 < phi < 1.62. The term proof applies the algebraic identity then discharges both sides of the conjunction by linear arithmetic.
claimLet $phi = (1 + sqrt(5))/2$. Then $4 < phi^3 land phi^3 < 4.25$.
background
The Constants module supplies numerical bounds on powers of the golden ratio for the phi-ladder used throughout Recognition Science. Upstream the identity phi^3 = 2 phi + 1 is obtained from the recurrence phi^2 = phi + 1 by direct expansion. The module also records the fundamental RS time quantum tau_0 equal to one tick.
proof idea
The term proof first rewrites the target via phi_cubed_eq to obtain the expression 2 phi + 1. It then pulls the lower bound from phi_gt_onePointFive and the upper bound from phi_lt_onePointSixTwo, after which linarith closes both conjuncts.
why it matters in Recognition Science
The lemma is called by phi_cubed_in_theta_band to embed phi^3 inside the theta EEG band and by modes_span_distinct_bands to separate distinct frequency ranges in the photobiomodulation device. It supplies the concrete numerical anchor for the third rung of the phi-ladder, consistent with the self-similar fixed point forced at T6 of the UnifiedForcingChain.
scope and limits
- Does not compute the exact decimal expansion of phi cubed.
- Does not tighten the bounds beyond the stated interval.
- Does not extend the argument to higher powers of phi.
- Does not invoke the J-cost or defect-distance machinery.
Lean usage
theorem theta_band_example : 4 < phi^3 ∧ phi^3 < 8 := by constructor <;> linarith [phi_cubed_bounds]formal statement (Lean)
146lemma phi_cubed_bounds : (4.0 : ℝ) < phi^3 ∧ phi^3 < 4.25 := by
proof body
Term-mode proof.
147 rw [phi_cubed_eq]
148 have h1 := phi_gt_onePointFive
149 have h2 := phi_lt_onePointSixTwo
150 constructor <;> linarith
151
152/-- φ⁴ is between 6.5 and 6.9.
153 φ⁴ = 3φ + 2 ≈ 6.854. -/