phi_lt_162
plain-language theorem explainer
Golden ratio φ obeys φ < 1.62. Interval arithmetic proofs in Recognition numerics cite this to close upper bounds on φ. The tactic proof invokes membership in phiInterval and a direct rational comparison.
Claim. $ (1 + √5)/2 < 1.62 $
background
The module supplies tactics for proving bounds on transcendental expressions via interval arithmetic. An Interval is a closed interval with rational endpoints lo ≤ hi. The specific interval phiInterval is defined as [1618/1000, 1619/1000] and contains φ by the upstream theorem phi_in_phiInterval, which itself relies on sqrt bounds.
proof idea
The proof applies the theorem phi_in_phiInterval to obtain that φ lies below the rational 1619/1000. It then proves the rational inequality 1619/1000 < 1.62 by norm_num and chains the two inequalities with lt_of_le_of_lt.
why it matters
This supplies a ready numerical bound on φ for use in interval-based proofs within the Recognition Science numerics layer. It supports the phi-ladder constructions and mass formulas that rely on precise bounds around the golden ratio fixed point. No downstream theorems currently depend on it, leaving it as a utility lemma for future interval verifications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.