minus_one_step_forces_phi_shift
plain-language theorem explainer
Three-point calibration at x = -1, 0, 1 on the affine-log gap function forces the scale parameter b to equal the golden ratio φ when b > 1. Researchers deriving the Recognition Science mass spectrum on the phi-ladder cite this to remove free coefficients from the candidate family. The proof extracts c = 0, equates the log relations, derives the quadratic b² - b - 1 = 0 via log product identities, and discards the extraneous root using positivity and the defining equation for φ.
Claim. Let $g(x) = a log(1 + x/b) + c$. If $b > 1$, $g(0) = 0$, $g(1) = 1$, and $g(-1) = -2$, then $b = φ$ where $φ$ satisfies $φ² = φ + 1$.
background
The module studies closure of the affine-log family under normalizations for the gap function in the mass formula. The candidate is gapAffineLogR a b c x := a * Real.log(1 + x / b) + c. Normalizations g(0) = 0 and g(1) = 1 fix a and c once b is given; the additional backward calibration at x = -1 forces b itself under the assumption b > 1 that selects the physically relevant branch.
proof idea
The proof first obtains c = 0 from the x = 0 condition. It rewrites the remaining conditions as a * log(1 + 1/b) = 1 and a * log(1 - 1/b) = -2. Algebraic rearrangement yields log(1 - 1/b) = -2 * log(1 + 1/b). Log product and power rules then produce the identity (1 - 1/b) * (1 + 1/b)² = 1. Field simplification gives the quadratic b² - b - 1 = 0. Comparison with phi_sq_eq, followed by mul_eq_zero and one_lt_phi together with hb > 1, eliminates the invalid root.
why it matters
This lemma supplies the forcing step that collapses the scale parameter under three-point calibration, feeding directly into affine_log_collapses_from_three_point_calibration and affine_log_parameters_forced_by_three_point_calibration. It removes coefficient freedom once the affine-log family is adopted, consistent with T6 (phi as self-similar fixed point) and the phi-ladder mass formula. It touches the open question whether the affine-log family itself is the unique choice selected from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.