phi_approx
plain-language theorem explainer
The lemma establishes that the golden ratio φ satisfies φ < 1.62. Researchers working on Recognition Science constants and mass ladders would cite this coarse bound for preliminary estimates in forcing-chain calculations. The proof is a one-line term reference to the upstream lemma that derives the same inequality from √5 < 2.24.
Claim. Let φ = (1 + √5)/2. Then φ < 1.62.
background
The Constants module defines the RS-native time quantum τ₀ as one tick and collects bounds on the golden ratio φ that appears as the self-similar fixed point (T6) in the UnifiedForcingChain. The upstream lemma phi_lt_onePointSixTwo supplies the tighter statement φ < 1.62 because √5 < 2.24, proved by showing 5 < (2.24)² and taking square roots. This coarse version is intended for quick checks in modules that do not need the full precision of the √5 estimate.
proof idea
The proof is a one-line wrapper that directly invokes the lemma phi_lt_onePointSixTwo.
why it matters
The bound supports preliminary calculations on the phi-ladder for mass formulas and the alpha band (137.030, 137.039) inside the Recognition framework. It fills a utility slot in the Constants module without feeding any downstream theorem, as the used_by count is zero. The result closes a simple scaffolding need for coarse numerical checks while the tighter √5-based lemma remains the primary reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.