phi_inv
plain-language theorem explainer
The golden ratio satisfies the reciprocal identity 1/φ = φ - 1. Researchers simplifying J-cost expressions or phi-ladder mass formulas in the forcing chain cite this relation to cancel terms. The proof is a short algebraic reduction that starts from φ² = φ + 1, multiplies out φ(φ - 1) = 1, and rearranges via the division rule.
Claim. $1/φ = φ - 1$
background
The module Inequalities assembles elementary lemmas on the golden ratio φ that recur across the Recognition framework. φ is the positive root of x² - x - 1 = 0 and obeys the defining relation φ² = φ + 1 (Constants.phi_sq_eq). Positivity of φ is recorded separately (Constants.phi_pos). These facts sit in the foundation layer that precedes the forcing chain (T5 J-uniqueness through T6 self-similar fixed point).
proof idea
The tactic proof first imports φ² = φ + 1 and 0 < φ. It then expands φ(φ - 1) = φ² - φ, substitutes the quadratic identity, and obtains 1. The final step applies eq_div_iff to the nonzero element φ and symmetrizes to reach 1/φ = φ - 1.
why it matters
This identity is invoked directly by PhiEmergence.phi_inv_eq and by PhiForcing.J_phi to evaluate J(φ) = φ - 3/2. It supplies the algebraic simplification required for the phi-ladder mass formula and for the lexicon-ratio conservation law. The step closes a basic prerequisite for the eight-tick octave and the D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.