one_add_inv_phi_eq_phi
plain-language theorem explainer
The golden ratio satisfies the identity 1 + 1/φ = φ over the reals. Researchers normalizing the affine-log gap function under the unit-step condition in the Recognition Science masses module cite this rewrite. The proof is a one-line wrapper applying the symmetric form of the defining equation φ = 1 + 1/φ.
Claim. $1 + 1/φ = φ$, where φ denotes the golden ratio.
background
The Gap Function Forcing module examines the affine-log candidate family g(x) = a * log(1 + x / b) + c. With b fixed to φ, the normalizations g(0) = 0 and g(1) = 1 force the canonical coefficients, while the backward calibration g(-1) = -2 forces b = φ itself. This collapses the family to gap(Z) = log(1 + Z/φ) / log(φ). The upstream lemma phi_eq_one_add_inv_phi establishes φ = 1 + 1/φ via field_simp on phi_sq_eq and phi_ne_zero, supplying the identity rewritten here.
proof idea
This is a one-line wrapper that applies the symmetric form of phi_eq_one_add_inv_phi via simpa.
why it matters
The lemma feeds the log rewrite log(1 + 1/φ) = log φ used in both the Masses and RSBridge GapFunctionForcing modules to close the affine-log parameters. It supplies the normalization step required for the gap function under three-point calibration, aligning with the T6 self-similar fixed point for φ in the forcing chain. It touches the open question of whether 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.