affine_log_parameters_forced
plain-language theorem explainer
Three-point calibration on the affine-log gap candidate uniquely determines its parameters to match the canonical gap function. Physicists modeling the phi-ladder mass spectrum would cite this result to justify the specific form of the gap function. The proof applies three specialized forcing lemmas in sequence after substituting the forced value of b.
Claim. Let $g(x) = a log(1 + x/b) + c$. If $b > 1$, $g(0) = 0$, $g(1) = 1$, and $g(-1) = -2$, then $b = phi$, $a = 1 / log phi$, and $c = 0$.
background
The affine-log candidate family is defined by gapAffineLogR(a, b, c, x) = a * log(1 + x/b) + c. The module imposes three normalization conditions on this family: g(0) = 0, g(1) = 1, g(-1) = -2 with b > 1. These conditions are shown to collapse the family to the canonical gap function gap(Z) = log(1 + Z/phi) / log(phi). Upstream lemmas include minus_one_step_forces_phi_shift, which forces the shift parameter b to phi under the three-point conditions, together with unit_step_forces_log_scale and zero_normalization_forces_offset that fix the remaining coefficients.
proof idea
The proof first applies minus_one_step_forces_phi_shift to obtain b = phi from the three-point conditions and b > 1. It substitutes this value into the remaining hypotheses via simpa, then invokes unit_step_forces_log_scale on the reduced g(0) = 0 and g(1) = 1 to fix a, and zero_normalization_forces_offset on g(0) = 0 to fix c.
why it matters
This theorem supplies the parameter uniqueness needed for three_point_closure in the same module. It realizes the three-point calibration described in the module documentation, which collapses the affine-log family to the canonical gap. The result is a structural postulate within the Recognition Science bridge from multiplicative costs to additive phi-ladder shifts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.