phi_bound_lower
plain-language theorem explainer
The lemma supplies a concrete decimal lower bound on the golden ratio in the reals. Numerics work in Recognition Science, especially interval bounds on phi-ladder calculations, would cite it for safe flooring. The proof is a one-line wrapper that pulls the library fact goldenRatio_gt_one and discharges the target inequality via linarith.
Claim. $1.618033988 ≤ φ$, where $φ$ denotes the golden ratio.
background
The IntervalProofs module supplies minimal helpers that convert small numerical inequalities into formal proofs, relying on norm_num and monotonicity rather than heavy dependencies. This lemma records a verified floor for the golden ratio, the self-similar fixed point forced at T6 of the unified forcing chain. It draws on the Mathlib fact that the golden ratio exceeds one, together with structural results from Foundation and NumberTheory modules that guarantee collision-free and phase-lift properties.
proof idea
The term proof introduces the hypothesis Real.goldenRatio_gt_one and applies the linarith tactic to confirm the decimal bound.
why it matters
The bound anchors numeric work inside the Recognition framework by giving a machine-checked floor for phi, the fixed point at T6. It supports downstream interval arithmetic that feeds mass formulas and constants such as ħ = φ^{-5}. No parent theorems appear in the used_by graph, so the lemma functions as a leaf helper for the numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.