three_point_forces_canonical_gap
plain-language theorem explainer
Three-point normalization conditions on the affine-log gap candidate force its scale parameter to the golden ratio and collapse the function to the canonical gap on integers. Researchers constructing mass ladders from J-costs in Recognition Science would cite this uniqueness result. The proof first applies minus_one_step_forces_phi_shift to obtain b equals phi, then reduces the remaining conditions via simpa to the collapse theorem affine_log_collapses_to_gap.
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 for every integer $Z$, $g(Z)$ equals the canonical gap function $log(1 + Z/phi)/log(phi)$.
background
The module works inside the affine-log family $g(x) = a log(1 + x/b) + c$. gapAffineLogR implements this family on the reals while gapAffineLog restricts it to integer inputs. The canonical gap is the function gap(Z) = log(1 + Z/phi)/log(phi) that appears in the phi-ladder mass formula and in AnchorPolicy.gap. Module documentation states that the three conditions g(0)=0, g(1)=1, g(-1)=-2 with b>1 fix c=0, b=phi, and a=1/log(phi), collapsing the family to the canonical gap. The proof relies on the upstream lemma minus_one_step_forces_phi_shift, which extracts b=phi from the negative-one condition.
proof idea
The tactic proof first calls minus_one_step_forces_phi_shift on hb, h0, h1, hneg1 to produce b=phi. It then uses simpa to rewrite the zero and unit conditions under this substitution. The final step applies affine_log_collapses_to_gap to the adjusted hypotheses for arbitrary integer Z.
why it matters
The result supplies the uniqueness step that three_point_closure consumes to build the closure certificate. It realizes the three-point calibration described in the module documentation, converting the affine-log candidate into the canonical gap used by mass anchors and gap derivations. In the Recognition framework it bridges the logarithmic cost structure to phi-ladder shifts, though the choice of the affine-log family itself remains a structural postulate rather than a consequence of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.