phi_gt_1618
plain-language theorem explainer
The lemma establishes the strict inequality 1.618 < φ for the golden ratio, supplying a concrete numerical anchor used in all subsequent RS mass and resonance calculations. Mass-prediction authors and resonance modelers cite it to justify bounds such as φ^7 > 29 or alpha-G lower limits. The proof unfolds the definition of φ, verifies a quadratic comparison for √5 via norm_num and sqrt monotonicity, then closes the inequality with linarith.
Claim. $1.618 < φ$ where $φ = (1 + √5)/2$ is the golden ratio.
background
In the Earth-Brain Resonance module the golden ratio φ enters the zero-parameter Schumann formula f(n) = (4n − 1)φ + 3, which reproduces the five measured harmonics (7.83, 14.3, 20.8, 27.3, 33.8 Hz) to within 0.4 %. The module imports φ from Constants and treats it as the self-similar fixed point forced by T6 of the UnifiedForcingChain. The present bound is the local copy of the same inequality proved in Numerics.Interval.PhiBounds.phi_gt_1618 and reused verbatim in the Ising2D sibling.
proof idea
The tactic proof first applies simp only [phi] to expose the explicit form (1 + √5)/2. It then proves (2.236 : ℝ)^2 < 5 by norm_num, rewrites the target via Real.sqrt_sq and Real.sqrt_lt_sqrt to obtain (2.236 : ℝ) < √5, and finally invokes linarith to finish the comparison with 1.618.
why it matters
The bound is invoked by thirty-one downstream declarations, including alphaG_pred_lower (AlphaGScoreCard), phi_pow_7_gt_29 (NumericalPredictions), and phi17_gt (Verification). These results rely on φ > 1.618 to close the phi-ladder inequalities that feed the mass formula yardstick · φ^(rung − 8 + gap(Z)) and the alpha-band predictions. It directly supports the T6 self-similarity step and the D = 3 octave structure used in the Schumann resonance derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.