three_point_closure
plain-language theorem explainer
The three-point closure theorem shows that the normalization conditions g(0)=0, g(1)=1, g(-1)=-2 with b>1 force the affine-log parameters to b=phi, a=1/log phi, c=0 and collapse the function to the canonical gap on integers. A physicist calibrating the Recognition Science mass ladder from J-cost data would cite this result to justify the phi-ladder placement. The proof is a term-mode construction that applies the parameter-forcing theorem to extract the first three fields and the canonical-collapse theorem for the final predicate.
Claim. Assume $b>1$. Let $g(x)=a log(1+x/b)+c$. If $g(0)=0$, $g(1)=1$, and $g(-1)=-2$, then $b=phi$, $a=1/log phi$, $c=0$, and $g(Z)$ coincides with the canonical gap function for every integer $Z$.
background
The module examines the affine-log family $g(x)=a log(1+x/b)+c$ as a candidate bridge converting multiplicative J-costs to additive rung shifts on the phi-ladder. The ThreePointClosure structure certifies that the three calibration points force $b=phi$, $a=1/log phi$, $c=0$, and that the resulting function equals RSBridge.gap on all integers Z. The upstream theorem affine_log_parameters_forced extracts the explicit parameter values from the three equations, while three_point_forces_canonical_gap shows the direct collapse to the canonical form.
proof idea
The proof invokes affine_log_parameters_forced on the three normalization hypotheses to obtain the forced values of b, a, and c. It then applies three_point_forces_canonical_gap to the same hypotheses to obtain the collapse predicate. These four components are assembled directly into the ThreePointClosure structure via a constructor term.
why it matters
This theorem completes the three-point calibration in the GapFunctionForcing module by supplying the full certificate that the affine-log family collapses to the canonical gap. It supports downstream mass formulas that locate particle masses on the phi-ladder via yardstick times phi to the power (rung-8+gap(Z)). The result stays inside the affine-log family; the choice of this family as the correct bridge remains a structural postulate motivated by the logarithmic cost-to-rung conversion rather than a derivation from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.