zero_normalization_forces_offset
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.