phi_cubed_bounds
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.