unit_step_forces_log_scale
plain-language theorem explainer
The lemma establishes that zero and unit normalizations on the affine-log gap function with fixed shift phi force the scale coefficient a to equal 1 over log phi. Mass-ladder calculations in Recognition Science cite it to pin the logarithmic spacing once the phi-shift is adopted. The proof first extracts c equals zero from the zero-normalization lemma, rewrites the unit condition via the log-identity lemma, and solves the resulting division equation.
Claim. Let $g(x) = a log(1 + x/φ) + c$. If $g(0) = 0$ and $g(1) = 1$, then $a = 1 / log φ$.
background
The module works inside the affine-log candidate family $g(x) = a log(1 + x/b) + c$ on the reals, with b fixed at phi. gapAffineLogR is the direct definition of this family. The local setting is Tier 1.1 closure: the normalizations g(0)=0 and g(1)=1 are imposed to remove coefficient freedom and collapse the family to the canonical gap(Z) = log(1 + Z/φ) / log(φ). Upstream, zero_normalization_forces_offset states that the zero condition alone forces the additive offset c to zero. log_one_add_inv_phi_eq_log_phi rewrites log(1 + phi inverse) as log phi, using the golden-ratio identity phi = 1 + 1/phi. one_lt_phi supplies the positivity needed for the logarithm to be well-defined and nonzero.
proof idea
Tactic proof begins by applying zero_normalization_forces_offset to the zero hypothesis, yielding c = 0. It then records that log phi is nonzero via one_lt_phi. The unit hypothesis is rewritten under the gapAffineLogR definition to obtain a * log(1 + phi inverse) = 1. A calc block invokes log_one_add_inv_phi_eq_log_phi to replace the argument with log phi, producing a * log phi = 1. The final step applies eq_div_iff to solve for a.
why it matters
This lemma supplies the scale coefficient needed by the downstream collapse theorems affine_log_collapses_to_canonical_gap and affine_log_collapses_to_gap, which equate the normalized affine-log family to the canonical RSBridge.gap. It completes one half of the three-point forcing program described in the module doc-comment, removing the free scale once the phi-shift is chosen. In the broader framework it fixes the logarithmic rung spacing on the phi-ladder after T6 has forced phi as the self-similar fixed point, preparing the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.