phi_gt_161803395
plain-language theorem explainer
The theorem establishes that the golden ratio φ exceeds 1.61803395 in the reals. Numerics routines for interval arithmetic on logarithms and powers cite it to anchor decimal comparisons without floating-point error. The proof verifies a quadratic bound on an approximation to √5 via norm_num, applies the square-root monotonicity lemma, unfolds the definition of φ, and closes with linarith.
Claim. $1.61803395 < φ$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The W8 Numerical Bounds module supplies tight decimal intervals for φ and √2 to compute the gap weight w8_from_eight_tick = (348 + 210√2 - (204 + 130√2)φ)/7. The Constants structure bundles real parameters such as Knet with its nonnegativity hypothesis. This lower bound on φ supports the phi-ladder and eight-tick octave constructions.
proof idea
The tactic proof first asserts 0 ≤ 2.2360679 and (2.2360679)^2 < 5 by norm_num. It invokes Real.lt_sqrt to obtain 2.2360679 < √5. Unfolding the definition of φ and applying linarith yields the target inequality.
why it matters
The result supplies the lower anchor used by log_phi_gt_048 and log_phi_gt_0481 in the AlphaBounds and Log modules, which feed alpha-inverse bounds near 137.03. It closes a numerical step in the T6 self-similar fixed-point construction of the unified forcing chain. Downstream theorems quote the bound directly to maintain rigorous decimal control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.