log_one_add_inv_phi_eq_log_phi
plain-language theorem explainer
The lemma establishes that the natural log of one plus the reciprocal of the golden ratio equals the log of phi itself. Researchers calibrating the gap function within the affine-log family in Recognition Science cite this identity to fix the scale coefficient. The tactic proof substitutes the golden-ratio relation 1 + phi inverse equals phi and simplifies the logs directly.
Claim. $log(1 + phi^{-1}) = log phi$, where $phi$ is the golden ratio satisfying $phi = 1 + phi^{-1}$.
background
The module examines the affine-log candidate family $g(x) = a log(1 + x/b) + c$. Three normalization conditions fix the parameters uniquely inside this family: $g(0) = 0$ forces $c = 0$, $g(-1) = -2$ with $b > 1$ forces $b = phi$, and $g(1) = 1$ forces $a = 1/log phi$. The resulting canonical gap function is $gap(Z) = log(1 + Z/phi)/log(phi) = log_phi(1 + Z/phi)$ (MODULE_DOC). This lemma supplies the identity needed for the log-scale step. It rests on the upstream lemma one_add_inv_phi_eq_phi, which states the equivalent rewrite $1 + 1/phi = phi$.
proof idea
The tactic proof introduces the auxiliary equality $(1 + phi^{-1} : R) = phi$ by applying one_add_inv_phi_eq_phi (with simpa [one_div]), then uses simp on the logs to obtain the desired equality.
why it matters
The identity feeds unit_step_forces_log_scale, which fixes the coefficient $a = 1/log phi$ under the normalizations $gapAffineLogR a phi c 0 = 0$ and $gapAffineLogR a phi c 1 = 1$. It thereby completes the three-point calibration that collapses the affine-log family to the canonical gap function. In the Recognition framework this step relies on the self-similar fixed point phi (T6) and supports the phi-ladder mass formula; the uniqueness claim remains a structural postulate rather than a derivation from T0-T8 (MODULE_DOC).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.