affine_log_collapses_from_three_point_calibration
plain-language theorem explainer
Three-point calibration on the affine-log family forces the scale parameter to the golden ratio and collapses the function to the canonical RS gap on integers. Mass modelers working with the phi-ladder would cite this to justify using the fixed gap formula without free coefficients. The proof first extracts b equals phi from the backward calibration, then reduces to the two-point collapse theorem.
Claim. Let $g(x) := a log(1 + x/b) + c$ with $b > 1$. Given the normalizations $g(0) = 0$, $g(1) = 1$, and $g(-1) = -2$, it holds that $g(Z) = log(1 + Z/φ) / log(φ)$ for every integer $Z$.
background
The module records closure for the affine-log candidate family $g(x) = a log(1 + x/b) + c$ under three-point normalizations, collapsing it to the canonical form $log(1 + Z/φ)/log(φ)$. gapAffineLogR denotes the real-valued affine-log family, gapAffineLog its integer restriction, and RSBridge.gap the canonical gap function from the anchor policy. Upstream, affine_log_collapses_to_canonical_gap establishes the two-point collapse once b is fixed to phi, while Gap45.Derivation.gap defines the gap as the product of closure and Fibonacci factors.
proof idea
The proof invokes minus_one_step_forces_phi_shift on the three calibration conditions to obtain b = phi. It then simplifies the hypotheses via simpa and applies affine_log_collapses_to_canonical_gap to conclude the equality for arbitrary integer Z.
why it matters
This supplies the three-point closure step that feeds directly into three_point_affine_log_closure, completing removal of free coefficients in the affine-log family for Tier 1.1. It relies on phi as the self-similar fixed point (T6) and supports the mass formula on the phi-ladder by fixing the gap function under the stated normalizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.