unit_step_forces_log_scale
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the affine-log family is the correct or unique bridge from J-costs to the phi-ladder.
- Does not address the integer specialization of the gap function.
- Does not derive the value of phi or the eight-tick octave.
- Does not extend uniqueness beyond the affine-log family.
Lean usage
have ha : a = 1 / Real.log phi := unit_step_forces_log_scale h0 h1formal statement (Lean)
72lemma unit_step_forces_log_scale
73 {a c : ℝ}
74 (h0 : gapAffineLogR a phi c 0 = 0)
75 (h1 : gapAffineLogR a phi c 1 = 1) :
76 a = 1 / Real.log phi := by
proof body
Tactic-mode proof.
77 have hc : c = 0 := zero_normalization_forces_offset h0
78 have hlog_ne : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
79 have hmul_raw : a * Real.log (1 + phi⁻¹) = 1 := by
80 simpa [gapAffineLogR, hc] using h1
81 have hmul : a * Real.log phi = 1 := by
82 calc
83 a * Real.log phi = a * Real.log (1 + phi⁻¹) := by
84 rw [log_one_add_inv_phi_eq_log_phi]
85 _ = 1 := hmul_raw
86 exact (eq_div_iff hlog_ne).2 hmul
87
88/-! ## Step 3: g(-1) = -2 forces b = φ (the key theorem)
89
90This is the paper's Theorem 4.2: setting u = 1/b, the condition
91`(1 - u)(1 + u)^2 = 1` expands to `u^2 + u - 1 = 0`, giving u = 1/φ. -/
92