ThreePointAffineLogClosure
plain-language theorem explainer
The three-point affine-log closure structure records that parameters a, b, c for the candidate gap family must satisfy b equals the golden ratio, a equals one over the logarithm of that ratio, and c equals zero, while also forcing exact agreement with the canonical gap expression on every integer. Mass-spectrum modelers cite the record when they adopt the affine-log ansatz and need a compact witness that three calibration points remove all coefficient freedom. The declaration is a pure structure definition that simply bundles the four required
Claim. Let $a,b,c$ be real numbers. A three-point affine-log closure certificate for these parameters asserts that $b=φ$, $a=1/ℝ.log φ$, $c=0$, and that the map $Z↦a⋅log(1+Z/b)+c$ equals the canonical gap function $log(1+Z/φ)/log φ$ for every integer $Z$.
background
The module records closure steps inside the affine-log candidate family $g(x)=a⋅log(1+x/b)+c$. The integer specialization gapAffineLog applies this family to ℤ arguments. The RSBridge.gap definition supplies the target closed form $log(1+Z/φ)/log φ$, which the module documentation identifies as the expression obtained once the three normalizations $g(0)=0$, $g(1)=1$, and $g(-1)=-2$ are imposed. Upstream, Anchor.Z maps sector and charge data to the integer labels that enter the gap function, while AnchorPolicy.gap already encodes the same logarithmic expression in the anchor setting.
proof idea
The declaration is a structure definition that packages four field assertions; no lemmas are invoked and no tactics are executed.
why it matters
The structure supplies the certificate consumed by the downstream theorem three_point_affine_log_closure, which builds the witness from the three calibration hypotheses. It thereby completes the coefficient-forcing step described in the module documentation for Tier 1.1, removing free parameters inside the affine-log family once that family is adopted. The construction sits inside the Recognition Science treatment of the phi-ladder and the canonical gap expression that appears in the RSBridge anchor relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.