phi_eq_one_add_inv_phi
The golden ratio satisfies φ = 1 + 1/φ. Researchers normalizing the affine-log gap function under three-point calibration in Recognition Science cite this identity for the unit-step condition. The proof is a short tactic-mode calculation that rewrites φ via division, substitutes the square identity, and simplifies the resulting fraction.
claimThe golden ratio satisfies the equation $φ = 1 + 1/φ$.
background
In the Gap Function Forcing module the affine-log family is written g(x) = a · log(1 + x/b) + c. Three normalization conditions collapse it to the canonical gap(Z) = log_φ(1 + Z/φ). The golden ratio φ is introduced in Constants and satisfies the quadratic identity φ² = φ + 1. Upstream, phi_sq_eq states that φ² = φ + 1 follows from the defining equation x² - x - 1 = 0, while phi_ne_zero asserts φ ≠ 0 to license division in field_simp.
proof idea
The tactic proof opens with phi_ne_zero to obtain a non-zero hypothesis, then performs a calc block. It rewrites φ as φ²/φ by field_simp, replaces the numerator with φ + 1 via phi_sq_eq, and finishes with a second field_simp to reach 1 + 1/φ.
why it matters in Recognition Science
This lemma supplies the unit-step normalization required by the three-point calibration. It is used directly by one_add_inv_phi_eq_phi in both Masses.GapFunctionForcing and RSBridge.GapFunctionForcing, which in turn feed the canonical gap function. The identity instantiates the self-similar fixed-point property of φ (T6 in the forcing chain). The module doc notes that the affine-log family itself remains a structural postulate motivated by logarithmic cost-to-rung conversion rather than a theorem derived from T0–T8.
scope and limits
- Does not prove existence or positivity of φ.
- Does not derive the affine-log form of the gap function from T0–T8.
- Does not establish uniqueness of the gap function outside the affine-log family.
- Does not compute numerical approximations or bounds for φ.
formal statement (Lean)
47lemma phi_eq_one_add_inv_phi : phi = 1 + (1 : ℝ) / phi := by
proof body
Tactic-mode proof.
48 have hne : phi ≠ 0 := phi_ne_zero
49 calc
50 phi = phi ^ 2 / phi := by field_simp [hne]
51 _ = (phi + 1) / phi := by simp [phi_sq_eq]
52 _ = 1 + (1 : ℝ) / phi := by field_simp [hne]
53