phi_gt_161
plain-language theorem explainer
The golden ratio satisfies 1.61 < φ with φ = (1 + √5)/2. Numerics work in Recognition Science cites this bound to anchor rational interval proofs for phi-ladder constants. The tactic proof obtains membership of φ in the precomputed interval [1.618, 1.619] then chains a direct rational comparison.
Claim. $1.61 < (1 + √5)/2$
background
The Numerics.Interval.Tactic module supplies tactics that certify bounds on expressions via interval arithmetic. The supporting definition phiInterval is the closed interval with rational endpoints 1618/1000 and 1619/1000. The upstream theorem phi_in_phiInterval asserts that φ lies inside this interval, proved by direct sqrt bounds and norm_num comparisons.
proof idea
The proof calls phi_in_phiInterval to obtain the membership fact whose lower component is φ > 1618/1000. It then proves the auxiliary rational inequality 1.61 < 1618/1000 by norm_num and finishes with lt_of_lt_of_le.
why it matters
This result supplies a concrete numerical anchor for φ, the self-similar fixed point forced at T6 of the UnifiedForcingChain. It supports downstream interval tactics that tighten constants such as ħ = φ^{-5} and G = φ^5/π inside the Recognition framework. No parent theorems are listed in the used-by graph, leaving the bound available for future phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.