log_one_add_inv_phi_eq_log_phi
plain-language theorem explainer
The equality log(1 + φ^{-1}) = log φ holds for the golden ratio φ. Workers normalizing the affine-log gap function under three-point calibration cite this when fixing the scale coefficient. The proof is a one-line wrapper that substitutes the algebraic identity 1 + φ^{-1} = φ into the logarithm argument and simplifies.
Claim. $log(1 + φ^{-1}) = log φ$ in the reals, where φ satisfies φ = 1 + φ^{-1}.
background
The GapFunctionForcing module records closure steps for 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 canonical coefficients, collapsing the family to gap(Z) = log(1 + Z/φ) / log(φ). The upstream lemma one_add_inv_phi_eq_phi supplies the identity 1 + φ^{-1} = φ that defines the golden ratio shift used throughout the module.
proof idea
The proof obtains the shift (1 + φ^{-1}) = φ by applying one_add_inv_phi_eq_phi, then substitutes this equality into the logarithm argument and simplifies to reach the target identity.
why it matters
This lemma feeds unit_step_forces_log_scale, which concludes a = 1 / log φ under the normalizations g(0)=0 and g(1)=1. It advances the module's collapse of the affine-log family to the canonical gap form. In the Recognition framework it supports the forcing of φ as the self-similar fixed point (T6) that removes coefficient freedom once the family is adopted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.