affine_log_unique_under_normalizations
plain-language theorem explainer
Two affine-log functions with fixed scale phi that both vanish at zero and equal one at unity coincide on every integer. Mass-spectrum work in Recognition Science cites this to drop coefficient ambiguity once the affine-log candidate is chosen. The proof reduces each side to the canonical gap via the collapse lemma applied to the shared normalizations.
Claim. Let $g_i(x) = a_i log(1 + x/φ) + c_i$ for $i=1,2$. If $g_1(0)=0$, $g_1(1)=1$, $g_2(0)=0$, and $g_2(1)=1$, then $g_1(Z)=g_2(Z)$ for every integer $Z$.
background
gapAffineLogR(a,b,c,x) is the real affine-log family a*log(1+x/b)+c; gapAffineLog is its restriction to integer arguments. The module records a Tier 1.1 closure: with b fixed at phi the two normalizations g(0)=0 and g(1)=1 force the coefficients, collapsing the family to the canonical gap(Z)=log(1+Z/φ)/log(φ). Upstream affine_log_collapses_to_canonical_gap states that under exactly these normalizations the affine-log expression equals RSBridge.gap for all Z.
proof idea
One-line wrapper that applies affine_log_collapses_to_canonical_gap to each normalized pair and equates the resulting canonical expressions.
why it matters
The result finishes the coefficient-forcing step inside the Gap Function Forcing module, removing all free parameters once the affine-log form is adopted. It supports the canonical gap used in the phi-ladder mass formula and the eight-tick octave structure, though the module notes it does not yet derive the affine-log shape from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.