zero_normalization_forces_offset
The lemma shows that zero normalization of the affine-log gap function at argument zero forces the additive offset to vanish. Collapse theorems in the gap forcing module cite it to reduce the candidate family to canonical form. The proof is a direct simplification from the function definition.
claimLet $g(x) := a log(1 + x/φ) + c$. If $g(0) = 0$, then $c = 0$.
background
The module records closure steps for the affine-log candidate family $g(x) = a log(1 + x/b) + c$ under normalizations. With $b$ fixed to φ, the conditions $g(0)=0$ and $g(1)=1$ force the canonical coefficients, collapsing to $gap(Z) = log(1 + Z/φ)/log(φ)$. This lemma handles the zero normalization case for the real-valued family gapAffineLogR.
proof idea
Term-mode proof consisting of a single simplification. It applies simpa with the gapAffineLogR definition to hypothesis h0, which substitutes the logarithmic term at zero to yield c = 0 directly.
why it matters in Recognition Science
Invoked by affine_log_collapses_to_canonical_gap and affine_log_parameters_forced_by_three_point_calibration to eliminate the offset before fixing the scale coefficient. It advances the module's reduction of the gap function family under three-point calibration, aligning with Recognition Science constraints on the phi-ladder mass formula.
scope and limits
- Does not prove the affine-log family is uniquely forced from T0-T8.
- Does not constrain the scale parameter b.
- Applies only when the second argument equals phi.
- Does not address non-affine or higher-order corrections.
Lean usage
have hc : c = 0 := zero_normalization_forces_offset h0formal statement (Lean)
66lemma zero_normalization_forces_offset
67 {a c : ℝ}
68 (h0 : gapAffineLogR a phi c 0 = 0) :
69 c = 0 := by
proof body
Term-mode proof.
70 simpa [gapAffineLogR] using h0
71
72/-- Unit-step calibration fixes the log scale coefficient. -/