phiInv_eq_phi_minus_one
plain-language theorem explainer
The identity 1/φ = φ - 1 holds for the golden ratio φ. Researchers modeling decay rates, target ratios, and mixing angles across domains cite this result to unify negative-rung quantities. The proof is a short algebraic reduction that invokes φ² = φ + 1 to establish the product φ(φ - 1) = 1 and then rewrites the division definition.
Claim. Let φ denote the golden ratio. Then 1/φ = φ - 1.
background
The module establishes invariants for the quantity 1/φ across domains, with phiInv defined as the real number 1/φ. The upstream lemma phi_sq_eq states that φ² = φ + 1, the defining quadratic equation of the golden ratio. The local setting is the C22 structural claim that 1/φ ≈ 0.618 acts as the canonical attractor for decay rates, dampings, target ratios, and optimal share fractions in independent domains.
proof idea
The tactic proof first obtains φ ≠ 0 from positivity. It applies the upstream identity φ² = φ + 1 to derive φ(φ - 1) = 1 via nlinarith. After unfolding the definition of phiInv as 1/φ, it rewrites the target equality using eq_div_iff and closes with linarith.
why it matters
This theorem supplies the fib_identity field to the downstream certificate phiInverseInvariantsCert that collects all 1/φ properties. It anchors the cross-domain convergence on 1/φ as the negative-rung value, consistent with the phi-ladder and the self-similar fixed point in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.