phi_fifth_bounds
The lemma establishes that the fifth power of the golden ratio satisfies 10.7 < phi^5 < 11.3. Researchers deriving RS-native constants for gravity, chemistry, or EEG bands would cite this interval. The proof reduces the claim to the algebraic identity phi^5 = 5 phi + 3 together with the supplied numerical bounds on phi via linear arithmetic.
claim$10.7 < phi^5 < 11.3$ where $phi = (1 + sqrt(5))/2$ is the positive root of $x^2 - x - 1 = 0$, equivalently satisfying $phi^5 = 5 phi + 3$.
background
In the Constants module the symbol phi denotes the golden ratio, the self-similar fixed point forced at step T6 of the UnifiedForcingChain. The module fixes the RS-native time quantum at one tick. Upstream, phi_fifth_eq records the closed identity phi^5 = 5 phi + 3 obtained from the Fibonacci recurrence by repeated use of phi^2 = phi + 1. Two further upstream lemmas supply the tight numerical bounds 1.61 < phi < 1.62.
proof idea
The term-mode proof first rewrites the goal with the phi_fifth_eq identity. It then pulls in the two bounding lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The constructor splits the conjunction and linarith discharges both sides by linear arithmetic over the reals.
why it matters in Recognition Science
Seven downstream declarations invoke this bound, among them phi_fifth_in_alpha_band (placing phi^5 inside the 8-13 Hz alpha EEG range), born_exponent_in_range (chemistry), and kappa_bounds (gravitational coupling kappa = 8 phi^5). It supplies the numerical content for the T6 fixed-point step and the alpha^{-1} band prediction inside the forcing chain. It closes one link in the zero-parameter derivation of observed constants.
scope and limits
- Does not establish the exact numerical value of phi^5.
- Does not extend the interval to other powers of phi.
- Does not treat complex or negative arguments.
- Does not incorporate experimental measurement error.
- Does not prove algebraic independence or irrationality properties.
Lean usage
theorem phi_fifth_in_alpha_band : 8 < phi ^ 5 ∧ phi ^ 5 < 13 := by constructor <;> linarith [phi_fifth_bounds.1, phi_fifth_bounds.2]formal statement (Lean)
162lemma phi_fifth_bounds : (10.7 : ℝ) < phi^5 ∧ phi^5 < 11.3 := by
proof body
Term-mode proof.
163 rw [phi_fifth_eq]
164 have h1 := phi_gt_onePointSixOne
165 have h2 := phi_lt_onePointSixTwo
166 constructor <;> linarith
167
168/-- Key identity: φ⁶ = 8φ + 5 (Fibonacci recurrence). -/