one_add_inv_phi_eq_phi
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 φ.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish that the affine-log family is the unique bridge from multiplicative J-costs to additive phi-ladder shifts.
- Does not derive the gap function parameters from the forcing chain T0 to T8.
- Does not address Berry creation threshold, Z_cf = phi^5, or the alpha band.
- Does not compute numerical values or close any open scaffolding in the mass formula.
Lean usage
lemma log_shift : Real.log (1 + phi⁻¹) = Real.log phi := by have h : 1 + phi⁻¹ = phi := one_add_inv_phi_eq_phi; simp [h]formal statement (Lean)
54lemma one_add_inv_phi_eq_phi : 1 + (1 : ℝ) / phi = phi :=
proof body
One-line wrapper that applies phi_eq_one_add_inv_phi.symm.
55 phi_eq_one_add_inv_phi.symm
56