affine_log_collapses_to_gap
plain-language theorem explainer
The theorem shows that the affine-log family normalized at zero and unit with base phi coincides exactly with the canonical gap function on all integers Z. Bridge module authors cite it to close the uniqueness argument inside three-point calibration. The proof extracts the forced parameters a and c from prior normalization lemmas then reduces the expression by substitution and change-of-base identities.
Claim. Let $g(Z) = a · log(1 + Z/φ) + c$. If $g(0) = 0$ and $g(1) = 1$, then $g(Z) = log_φ(1 + Z/φ)$ for every integer $Z$.
background
The module works inside the affine-log candidate family $g(x) = a · log(1 + x/b) + c$. Three normalizations are imposed: $g(0)=0$ forces the offset $c=0$; $g(1)=1$ forces the scale $a = 1/log φ$; the remaining condition at $-1$ forces $b=φ$. The integer specialization gapAffineLog is defined by restricting the real affine-log to integer arguments. Upstream, gapAffineLogR supplies the real version while RSBridge.gap is the target canonical form $log(1 + Z/φ)/log φ$.
proof idea
Apply zero_normalization_forces_offset to the zero condition to obtain c=0. Apply unit_step_forces_log_scale to both conditions to obtain a = 1/Real.log phi. Unfold the definitions of gapAffineLog, gapAffineLogR and RSBridge.gap, then simplify the resulting expression by substitution, commutativity of multiplication, and the change-of-base identity for logarithms.
why it matters
The result supplies the collapse step required by the downstream theorem three_point_forces_canonical_gap, which completes the three-point uniqueness argument. It realizes the module claim that the affine-log family collapses to the canonical gap under the stated normalizations. The construction links the multiplicative J-cost structure to additive phi-ladder shifts, consistent with the Recognition Composition Law and the phi fixed point forced in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.