The Golden Quadruple: Four Reals Whose Differences Form a Geometric Progression, Rigidity of the Golden Ratio, and a Bohr Almost Periodic Cosine Sum
Michał Przybylski
math.CO
Oct 31, 2026 · v1
math.NT
TL;DR
The combinatorial and algebraic core results (maximality, uniqueness, golden-ratio rigidity, cosine closed form) are formalized in Lean 4 with Mathlib in a Lake project, axiom-audited.
Abstract
Let $\varphi=(1+\sqrt5)/2$. The four-point set $\{0,\varphi,\varphi^2,\varphi^3\}$ is classical: up to a dilation it consists of the two endpoints and the two crossing points on a side of the regular pentagram (Euclid, Elements XIII.8), and, by the identity $\varphi^2=\varphi+1$, its six pairwise differences are $1,\varphi,\varphi^2,\varphi^3$, with multiplicities $1,2,2,1$. We write this configuration as the golden quadruple $S=(F, F-a, F-b, F-a-b)$, where $u>0$, $a=\varphi u$, $b=\varphi^2u$ and $F>a+b$, and study its extremal and rigidity properties. We prove that it is maximal and unique: no five distinct real numbers have all their positive differences in $\{u,\varphi u,\varphi^2u,\varphi^3u\}$ (indeed, not even in the whole set $\{u\varphi^n:n\in\mathbb{Z}\}$), and every four-element set with this property is a translate of $S$. We prove that the golden ratio is forced: $\varphi$ is the only ratio $x>1$ for which some four-point set of reals has the four-term progression $\{c,cx,cx^2,cx^3\}$ as its set of distinct differences. For the analogous quadruple with base $x>1$, $x\neq\varphi$, the failure is measured by two closure residues, $(x^2-x-1)u$ and $x(x^2-x-1)u$, which along Fibonacci quotients equal $\pm u/F_n^2$ and $\pm F_{n+1}u/F_n^3$. Finally, the cosine sum $C_S(t)=\sum\cos(2πd t)$ over the six differences equals $8\cos^2(πa t)\cos^2(πb t)-2$; it is not periodic, but it is almost periodic in the sense of Bohr, with explicit almost periods $F_n/u$. For an arbitrary scale $K>0$ the golden ladder $ν_n=K\varphi^{-n}$ realises the construction with $u=ν_{203}$, so that the differences are $ν_{200},\dots,ν_{203}$; we evaluate it for $K=\sqrt{c^5/(Gh)}$. We state explicitly what is classical and what is new, in relation to difference sets, Golomb rulers, Sidon sets, Fibonacci numbers, quasicrystals and almost periodic functions.
Problem
The work studies four-point sets of reals whose distinct positive differences form a geometric progression. It asks for maximality, uniqueness and rigidity of the golden quadruple {0, φ, φ², φ³}·u, and for the almost-periodic behaviour of the associated cosine sum.
Approach
Elementary gap-counting arguments show that no five reals have all positive differences in {u, φu, φ²u, φ³u}, or even in {uφ^n}. The same arguments show that every such four-set is a translate of the golden quadruple. For a general base x, closure residues (x²−x−1)u and x(x²−x−1)u measure the failure, and are evaluated along Fibonacci quotients. The cosine sum is put in closed form, and Bohr almost periods F_n/u are given. The core results are formalized in Lean 4 on Mathlib, and an axiom audit is reported.
Results
The golden quadruple is proved maximal and unique, and φ is the only ratio x>1 that admits such a four-point configuration. The cosine sum equals 8cos²(πat)cos²(πbt)−2 and is almost periodic but not periodic. 27 audited Lean declarations use only the standard axioms, with no sorry.
| pair | exact value | power of φ | decimal |
|---|
| s1−s2 | φ | φ¹ | 1.618034 |
| s1−s3 | φ+1 | φ² | 2.618034 |
| s1−s4 | 2φ+1 | φ³ | 4.236068 |
| s2−s3 | 1 | φ⁰ | 1.000000 |
Differences of S for u=1, F=φ⁴