phi_eq_one_add_inv_phi
plain-language theorem explainer
The golden ratio satisfies φ = 1 + 1/φ. Researchers normalizing the unit-step condition inside the affine-log gap function family cite this identity to remove coefficient freedom under three-point calibration. The proof is a short calc block that rewrites φ as φ²/φ, substitutes the square identity, and simplifies the resulting fraction using field tactics.
Claim. The golden ratio satisfies $φ = 1 + 1/φ$.
background
The Gap Function Forcing module examines the affine-log family g(x) = a log(1 + x/b) + c. Fixed b = φ together with the normalizations g(0) = 0 and g(1) = 1 forces the canonical coefficients; the additional calibration g(-1) = -2 then forces the shift parameter itself to equal φ, collapsing the family to gap(Z) = log(1 + Z/φ) / log(φ). This lemma supplies the algebraic identity required to normalize the unit-step condition inside that collapse. It rests on the upstream facts that φ ≠ 0 and that φ² = φ + 1, the latter being the defining quadratic equation of the golden ratio.
proof idea
The proof is a tactic-mode calculation. It first obtains φ ≠ 0, then rewrites φ as φ²/φ by field_simp. Substitution of the square identity replaces the numerator with φ + 1, producing (φ + 1)/φ. A final field_simp step expands the fraction to 1 + 1/φ.
why it matters
The lemma closes one normalization step inside the gap-function forcing chain and is invoked directly by the symmetric rewrite one_add_inv_phi_eq_phi in both the Masses and RSBridge modules. It encodes the self-similar fixed-point property of φ (T6 of the forcing chain) that removes free parameters once the affine-log family is adopted. The surrounding module notes that this step does not yet prove the affine-log family itself is uniquely forced from T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.