phi_eq_formula
plain-language theorem explainer
The golden ratio equals (1 + sqrt(5))/2 by definition. Numerics code for interval power bounds cites this identity to substitute the Mathlib constant inside containment checks for phi powers. The proof is a direct reflexivity step that matches the library definition exactly.
Claim. $phi = (1 + sqrt(5))/2$
background
The Numerics.Interval.Pow module supplies rigorous interval arithmetic for the power function via the identity x^y = exp(y * log x) for x > 0, with direct computation for natural exponents. It imports the spacetime interval definition from SpacetimeEmergence: interval(v) := sum_{i:Fin 4} eta(i,i) * v(i)^2. The theorem equates the goldenRatio constant to its algebraic closed form, enabling substitution in power bounds.
proof idea
The proof is a term-mode reflexivity that directly matches the Mathlib definition of goldenRatio. No additional lemmas or tactics are required beyond the built-in rfl.
why it matters
This identity is invoked by the five phi_pow_*_in_interval theorems (phi_pow_5_in_interval, phi_pow_8_in_interval, phi_pow_16_in_interval, phi_pow_neg3_in_interval, phi_pow_neg5_in_interval) to replace goldenRatio inside interval containment statements. It supports the framework's phi as the self-similar fixed point from T6 and the eight-tick octave, permitting exact algebraic evaluation of powers that enter the mass ladder and alpha band. No open questions remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.