zero_normalization_forces_offset
The lemma shows that for the affine-log family g(x) = a log(1 + x/φ) + c the condition g(0) = 0 forces the additive offset c to vanish. Researchers calibrating the gap function via three-point normalization in the Recognition Science bridge would cite this result as the first step before fixing the base and scale. The proof is a one-line simplification that substitutes the definition of the affine-log family.
claimIf $g(0)=0$ where $g(x)=a·log(1+x/φ)+c$, then $c=0$.
background
The module treats the affine-log candidate family g(x) = a · log(1 + x/b) + c on the reals, with the three normalization conditions g(0)=0, g(1)=1 and g(-1)=-2 used to collapse it to the canonical gap function gap(Z) = log_φ(1 + Z/φ). The local theoretical setting is the structural postulate that this family bridges multiplicative J-costs to additive φ-ladder shifts; the uniqueness claim is internal to the family and not derived from T0–T8. The lemma depends on the definition gapAffineLogR a b c x := a * Real.log(1 + x/b) + c together with the fixed base b = φ supplied by upstream results.
proof idea
The proof is a one-line wrapper that applies the definition of gapAffineLogR. Substituting x = 0 yields a * log(1 + 0/φ) + c = a * log(1) + c = c, so the hypothesis g(0) = 0 immediately gives c = 0 via simpa.
why it matters in Recognition Science
This lemma supplies the first normalization step in the three-point calibration, feeding directly into downstream results such as affine_log_collapses_to_canonical_gap and affine_log_parameters_forced_by_three_point_calibration. It thereby contributes to the collapse of the affine-log family onto the canonical gap function used in mass formulas on the φ-ladder. The module documentation notes that the choice of the affine-log family itself remains a structural postulate motivated by the logarithmic nature of cost-to-rung conversion rather than a theorem from the forcing chain.
scope and limits
- Does not prove the affine-log family is the correct bridge from J-costs to φ-ladder shifts.
- Does not establish uniqueness of the gap function outside the affine-log family.
- Does not derive the value of φ or the log base from T0–T8.
- Does not address convergence or analytic continuation of the gap function.
Lean usage
have hc : c = 0 := zero_normalization_forces_offset h0formal statement (Lean)
64lemma zero_normalization_forces_offset
65 {a c : ℝ}
66 (h0 : gapAffineLogR a phi c 0 = 0) :
67 c = 0 := by
proof body
Term-mode proof.
68 simpa [gapAffineLogR] using h0
69
70/-! ## Step 2: g(1) = 1 forces a = 1/log(φ) (given c = 0 and b = φ) -/
71