one_add_inv_phi_eq_phi
plain-language theorem explainer
The golden ratio satisfies 1 + 1/φ = φ, which normalizes the unit-step condition when fixing the scale parameter b in the affine-log gap function. Researchers calibrating the canonical gap(Z) = log_φ(1 + Z/φ) from three-point conditions cite this identity. The proof is a one-line wrapper that applies the symmetric form of the defining equation for φ.
Claim. The golden ratio satisfies the equation $1 + 1/φ = φ$.
background
In the Gap Function Forcing module the affine-log candidate family is g(x) = a · log(1 + x/b) + c. Three normalization conditions fix the parameters: g(0) = 0 forces c = 0, g(-1) = -2 with b > 1 forces b = φ, and g(1) = 1 forces a = 1/log(φ). This collapses the family to the canonical gap function gap(Z) = log(1 + Z/φ)/log(φ) = log_φ(1 + Z/φ). The local setting is uniqueness within the affine-log family, a structural postulate motivated by the logarithmic cost-to-rung conversion rather than a theorem from T0–T8.
proof idea
The proof is a one-line wrapper that applies phi_eq_one_add_inv_phi.symm. The upstream lemma phi_eq_one_add_inv_phi establishes φ = 1 + 1/φ by the calculation phi = phi²/phi = (phi + 1)/phi = 1 + 1/phi, using field_simp and phi_sq_eq.
why it matters
This lemma supports the derivation of the canonical gap function and feeds directly into log_one_add_inv_phi_eq_log_phi, which rewrites the logarithm at the canonical shift argument for use in both RSBridge and Masses.GapFunctionForcing. In the Recognition Science framework it contributes to forcing φ as the self-similar fixed point (T6) and the phi-ladder used in mass formulas. The module doc notes that the uniqueness proved here is only within the affine-log family and remains a postulate not derived from T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.