phi_minus_one_abs
plain-language theorem explainer
The lemma establishes that the absolute value of the golden ratio minus one equals the golden ratio minus one itself. Numerics researchers constructing interval enclosures for the logarithm at the golden ratio would cite this when preparing the Taylor argument x = φ - 1. The proof is a one-line rewrite that invokes the absolute-value identity for positive reals on the upstream positivity result.
Claim. $ |φ - 1| = φ - 1 $, where φ denotes the golden ratio.
background
This lemma belongs to the Numerics.Interval.Log module, whose strategy is to bound log on intervals inside (0, ∞) by monotonicity and, for arguments of the form 1 + x with |x| < 1, by the alternating Taylor series whose remainder satisfies the standard geometric estimate. The concrete choice x = φ - 1 is singled out because 0 < φ - 1 < 1, allowing the series to be applied directly to log(φ). The required positivity 0 < goldenRatio - 1 is supplied by the upstream lemma phi_sub_one_pos, proved by linarith from the earlier bound phi_gt_1618.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma abs_of_pos to the hypothesis phi_sub_one_pos.
why it matters
The result is the immediate predecessor of phi_minus_one_abs_lt_one, which in turn supplies the hypothesis |φ - 1| < 1 needed to invoke the log(1 + x) error bound inside the interval arithmetic for log(φ). It therefore closes a small but indispensable step in the chain that produces rigorous enclosures for the logarithm evaluated at the self-similar fixed point of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.