affine_log_parameters_forced_by_three_point_calibration
plain-language theorem explainer
Under the three-point calibration the affine-log gap function g(x) = a log(1 + x/b) + c is forced to the canonical coefficients involving phi. Mass-gap modelers in Recognition Science cite the result to close free parameters once the affine-log family is adopted. The tactic proof chains three sibling lemmas: first minus_one_step_forces_phi_shift on the negative point to fix b, then unit_step_forces_log_scale and zero_normalization_forces_offset on the remaining conditions.
Claim. Let $g(x) = a · log(1 + x/b) + c$ with $b > 1$. If $g(0) = 0$, $g(1) = 1$ and $g(-1) = -2$, then $b = φ$, $a = 1 / log φ$ and $c = 0$.
background
The Gap Function Forcing module records closure steps for Tier 1.1 inside the affine-log candidate family $g(x) = a log(1 + x/b) + c$. The module states that the normalizations $g(0)=0$ and $g(1)=1$ together with the backward calibration $g(-1)=-2$ remove all free parameters and collapse the family to the canonical gap $gap(Z) = log(1 + Z/φ) / log(φ)$. Upstream results supply the arithmetic object canonical and the gap definition from Gap45.Derivation, while sibling lemmas encode the individual normalization steps.
proof idea
The tactic proof first applies minus_one_step_forces_phi_shift to the hypothesis $b > 1$ and the three point conditions to obtain $b = φ$. It substitutes this value into the zero and unit conditions, then invokes unit_step_forces_log_scale on those normalized conditions to force $a = 1 / log φ$. Finally it applies zero_normalization_forces_offset to the zero condition to obtain $c = 0$ and assembles the conjunction by exact.
why it matters
The theorem supplies the parameter-forcing step invoked by the downstream three_point_affine_log_closure to build the full closure certificate. It completes the second item listed in the module documentation: the backward-step calibration forces $b = φ$. Within the Recognition framework it contributes to collapsing the gap function to its canonical form on the phi-ladder, consistent with the self-similar fixed point (T6) and the eight-tick octave. It touches the open question whether the affine-log family itself is forced from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.