phi_inv_eq
plain-language theorem explainer
Golden ratio reciprocal identity states φ^{-1} equals φ minus one. Researchers deriving the exact Yang-Mills mass gap Δ = J(φ) in Recognition Science cite this to simplify J-cost expressions on the phi-ladder. The tactic proof reduces the claim to the quadratic φ² = φ + 1 via multiplication and cancellation.
Claim. The golden ratio φ satisfies $φ^{-1} = φ - 1$.
background
In the Recognition Science treatment of the Yang-Mills mass gap the golden ratio φ is the self-similar fixed point forced on the recognition lattice by T6. The J-cost functional is J(x) = ½(x + x^{-1}) - 1, and the phi-lattice supplies the discrete substrate for gauge excitations. Upstream the quadratic identity φ² = φ + 1 appears in Constants.phi_sq_eq as the defining equation of φ.
proof idea
The tactic proof first obtains phi ≠ 0 from Constants.phi_pos. It then applies nlinarith to phi_sq_eq to establish phi · (phi - 1) = 1. Multiplication cancellation on the right yields the reciprocal identity.
why it matters
This identity is required for the φ-sum identity phi_plus_inv that produces φ + φ^{-1} = √5 and thereby the exact mass gap J(φ) = (√5 - 2)/2. It closes a step in the T6 forcing chain from the phi fixed point to the spectral gap computation and is reused in phi_series_sum and the PhiBounds interval lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.