phi_gt_1618
plain-language theorem explainer
The lemma establishes the strict inequality 1.618 < phi for the golden ratio in the reals. Researchers deriving lower bounds on powers of phi for mass ladders and alpha predictions cite this result to anchor numerical estimates. The proof unfolds the definition of phi, verifies 2.236 squared lies below 5, and closes via linear arithmetic after the square-root monotonicity step.
Claim. The golden ratio satisfies $1.618 < phi$ where $phi = (1 + sqrt(5))/2$.
background
The module Physics.Ising2D supplies a diagnostic for the exactly solvable 2D Ising model against Recognition Science predictions. It records the Onsager exponents and tests whether the RS phi-algebra extends to D = 2, noting that the leading-order formula nu_0 = phi^{-1} fails to recover nu = 1. The present lemma supplies the concrete numerical anchor 1.618 < phi that appears in every downstream power bound. Upstream, Numerics.Interval.PhiBounds.phi_gt_1618 states the same inequality for goldenRatio and is mirrored here after the local definition of phi.
proof idea
The tactic proof first applies simp only [phi] to unfold the golden-ratio definition. It then builds an auxiliary fact that 2.236 < Real.sqrt 5 by showing 2.236 squared is less than 5 via norm_num, rewriting the square-root square identity, and invoking Real.sqrt_lt_sqrt. Linear arithmetic (linarith) combines the resulting inequalities to reach the target.
why it matters
This bound feeds alphaG_pred_lower in Masses.AlphaGScoreCard, phi_pow_7_gt_29 in NumericalPredictions, phi17_gt in Verification, and the suite of phi-power inequalities in Numerics.Interval.PhiBounds. It supplies the concrete lower estimate required by the phi-ladder mass formula and the self-similar fixed point T6 of the forcing chain. The module context underscores that D = 3 remains the unique physical dimension forced by the eight-tick octave, so the D = 2 diagnostic serves only as a consistency check rather than a derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.