unit_step_forces_log_scale
plain-language theorem explainer
The lemma shows that the scale factor a in the affine-log gap candidate is fixed to 1 over log phi once the function is normalized to pass through the points (0,0) and (1,1). Mass-gap calculations that rely on three-point calibration of the gap function cite this normalization. The argument first extracts c equals zero from the g(0) equals zero hypothesis, then substitutes the identity log(1 plus phi inverse) equals log phi to obtain a times log phi equals one.
Claim. Let $g(x) = a · log(1 + x/φ) + c$. If $g(0) = 0$ and $g(1) = 1$, then $a = 1 / log φ$.
background
The affine-log candidate family is defined by gapAffineLogR a b c x := a * Real.log(1 + x / b) + c. The module works inside this three-parameter family on the reals and shows that the three normalization conditions g(0)=0, g(1)=1 and g(-1)=-2 together collapse it to the canonical gap function. The upstream lemma one_lt_phi supplies 1 < phi, which guarantees that log phi is positive and nonzero. The sibling lemma zero_normalization_forces_offset directly converts the g(0)=0 hypothesis into c=0. The identity log_one_add_inv_phi_eq_log_phi, which rests on phi_eq_one_add_inv_phi, equates log(1 + phi^{-1}) with log phi.
proof idea
The proof is a short tactic sequence. It first applies zero_normalization_forces_offset to h0 to obtain c=0. It then rewrites the expression for g(1) using gapAffineLogR and the identity log_one_add_inv_phi_eq_log_phi, yielding a * log phi = 1. The final step invokes eq_div_iff on the nonzero term log phi to conclude a = 1 / log phi.
why it matters
This lemma supplies the scale coefficient required by affine_log_collapses_to_canonical_gap and affine_log_parameters_forced_by_three_point_calibration. It completes the second of the three normalization steps listed in the module documentation, thereby fixing the canonical gap function gap(Z) = log_φ(1 + Z/φ). The result sits inside the Recognition Science bridge from multiplicative J-costs to additive phi-ladder shifts; it does not derive the value of phi itself but assumes the golden-ratio fixed point already forced by the upstream chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.