affine_log_collapses_to_canonical_gap
plain-language theorem explainer
The theorem shows that any affine-log gap function with fixed base phi, normalized to vanish at zero and equal one at unity, coincides exactly with the canonical RS gap on all integers. Mass modelers working in the Recognition framework would cite it to remove free coefficients once the affine-log candidate family is adopted. The proof extracts the forced scale and offset from the two normalization conditions via dedicated lemmas, then substitutes to recover the logarithmic ratio form.
Claim. Let $g(Z) = a log(1 + Z/φ) + c$. If $g(0) = 0$ and $g(1) = 1$, then $g(Z) = log(1 + Z/φ) / log(φ)$ for every integer $Z$.
background
The module records closure steps for the affine-log family $g(x) = a log(1 + x/b) + c$ under structural normalizations. With $b$ fixed to phi, the conditions $g(0)=0$ and $g(1)=1$ determine the coefficients uniquely, collapsing the family to the canonical gap $log(1 + Z/φ)/log(φ)$. The function gapAffineLog is the integer specialization of this family, while RSBridge.gap supplies the target canonical expression (matching the form in AnchorPolicy.gap).
proof idea
The proof applies zero_normalization_forces_offset to the condition at zero, yielding $c=0$. It then invokes unit_step_forces_log_scale on both conditions to obtain $a = 1 / log φ$. Substitution into the unfolded expression followed by algebraic simplification (dividing the logs) recovers the canonical gap for arbitrary integer $Z$.
why it matters
This supplies the direct collapse step used by affine_log_collapses_from_three_point_calibration and affine_log_unique_under_normalizations. It realizes the first closure listed in the module documentation: normalizations force the canonical coefficients and remove all free parameters within the affine-log family. In the Recognition framework it fixes the gap on the phi-ladder, consistent with the self-similar fixed point and eight-tick octave, while leaving open whether the affine-log form itself is forced from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.