ThreePointClosure
plain-language theorem explainer
The ThreePointClosure structure certifies that the affine-log family collapses to the canonical gap function once three calibration conditions fix its parameters. Mass-spectrum derivations that rely on the phi-ladder would cite it to justify writing gap(Z) directly as log_phi(1 + Z/phi). It is a structure definition that simply bundles the four forced identities.
Claim. Let $g(a,b,c;Z) = a·log(1 + Z/b) + c$. The structure ThreePointClosure(a,b,c) asserts $b = φ$, $a = 1/log φ$, $c = 0$, and $g(a,b,c;Z) = gap(Z)$ for every integer $Z$, where $gap(Z) = log(1 + Z/φ)/log φ$.
background
The module works inside the affine-log candidate family $g(x) = a·log(1 + x/b) + c$. Three normalization conditions are imposed: $g(0) = 0$ forces the offset $c = 0$; $g(-1) = -2$ with $b > 1$ forces the shift $b = φ$; and $g(1) = 1$ forces the scale $a = 1/log φ$. These together collapse the family to the canonical gap function $gap(Z) = log(1 + Z/φ)/log φ$, which is the display function F(Z) already defined in the RSBridge.Anchor module as the closed-form residue at the anchor scale. Upstream, gapAffineLog supplies the integer specialization of the same family, while the PrimitiveDistinction.from theorem supplies the seven-axiom starting point that ultimately motivates the logarithmic cost-to-rung conversion.
proof idea
This is a structure definition whose four fields directly record the forced parameter values and the collapse identity. No lemmas are applied and no tactics are used; the structure itself serves as the certificate type that the downstream three_point_closure theorem constructs from calibration data.
why it matters
The definition supplies the certificate type consumed by the theorem three_point_closure, which builds the certificate from the three calibration hypotheses. It thereby closes the uniqueness argument inside the affine-log family, linking the phi-ladder (T6) and the eight-tick octave (T7) to the concrete gap function used for mass anchoring. The module doc notes that the choice of the affine-log family itself remains a structural postulate rather than a derived theorem from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.