Sparse Ruler

A sparse ruler of length $L$ is a sequence of marks $0 = a_1 < a_2 < \dots < a_m = L$. A distance $k \in \mathbb{N}$ can be measured if there are $i, j \in \{1, \dots, m\}$, such that $k = a_j - a_i$.

One question concerns the structure of optimal rulers. Wichmann [Wi63] gave a parametric family of sparse rulers and conjectured that, beyond a small number of exceptions, every optimal ruler is of his type. The known exceptions occur at lengths $1, 13, 17, 23, 58$; the largest of these has $13$ segments, which motivates the bound below.

The asymptotic growth of the minimal number of marks of an optimal ruler of length $L$ — i.e. the limit of $l(n)^2 / n$, conjectured to lie in $[2.434\ldots, 3]$ — is the subject of FormalConjectures.ErdosProblems.«170» (there phrased via $F(N)/\sqrt{N}$), and is not restated here.

References:

• [Wi63] Wichmann, B. "A note on restricted difference bases." Journal of the London Mathematical Society 38 (1963): 465-466.
• Wikipedia

def SparseRuler.marks (g : List ℕ) : Finset ℕ

A ruler is described by its list of segment lengths (gaps) g, so that its marks are the partial sums $0 = m_0 < m_1 < \cdots < m_n = L$, where $n$ (g.length) is the number of segments and $L$ (g.sum) is the length.

Equations

• SparseRuler.marks g = Finset.image (fun (i : ℕ) => (List.take i g).sum) (Finset.range (g.length + 1))

def SparseRuler.IsComplete (g : List ℕ) : Prop

A ruler is complete (a perfect ruler) if its marks form a difference basis for $\{0, 1, \ldots, L\}$, i.e. every distance $k \le L$ is the difference of two marks. This is Finset.IsDifferenceBasis applied to the marks.

Equations

• SparseRuler.IsComplete g = (SparseRuler.marks g).IsDifferenceBasis (Finset.range (g.sum + 1))

def SparseRuler.IsMinimal (g : List ℕ) : Prop

A complete ruler is minimal if no complete ruler of the same length $L$ has fewer marks (equivalently, fewer segments).

Equations

• SparseRuler.IsMinimal g = (SparseRuler.IsComplete g ∧ ∀ (g' : List ℕ), SparseRuler.IsComplete g' → g'.sum = g.sum → g.length ≤ g'.length)

def SparseRuler.IsMaximal (g : List ℕ) : Prop

A complete ruler is maximal if no complete ruler with the same number of marks (equivalently, the same number of segments) has greater length.

Equations

• SparseRuler.IsMaximal g = (SparseRuler.IsComplete g ∧ ∀ (g' : List ℕ), SparseRuler.IsComplete g' → g'.length = g.length → g'.sum ≤ g.sum)

def SparseRuler.IsOptimal (g : List ℕ) : Prop

A ruler is optimal if it is both minimal and maximal.

Equations

• SparseRuler.IsOptimal g = (SparseRuler.IsMinimal g ∧ SparseRuler.IsMaximal g)

def SparseRuler.wichmannGaps (r s : ℕ) : List ℕ

The Wichmann ruler $W(r, s)$ [Wi63], given by its segment-length sequence $$1^r,\; (r+1),\; (2r+1)^r,\; (4r+3)^s,\; (2r+2)^{r+1},\; 1^r,$$ where $a^b$ denotes $b$ consecutive segments of length $a$.

Equations

• SparseRuler.wichmannGaps r s = List.replicate r 1 ++ [r + 1] ++ List.replicate r (2 * r + 1) ++ List.replicate s (4 * r + 3) ++ List.replicate (r + 1) (2 * r + 2) ++ List.replicate r 1

theorem SparseRuler.wichmannGaps_length (r s : ℕ) : (wichmannGaps r s).length = 4 * r + s + 2

The Wichmann ruler $W(r, s)$ has $4r + s + 2$ segments, hence $4r + s + 3$ marks [Wi63].

theorem SparseRuler.wichmannGaps_sum (r s : ℕ) : (wichmannGaps r s).sum = 4 * r * (r + s + 2) + 3 * (s + 1)

The Wichmann ruler $W(r, s)$ has length $4r(r + s + 2) + 3(s + 1)$ [Wi63].

theorem SparseRuler.wichmann_conjecture {g : List ℕ} (hopt : IsOptimal g) (hseg : 13 < g.length) : ∃ (r : ℕ) (s : ℕ), g = wichmannGaps r s ∨ g = (wichmannGaps r s).reverse

Wichmann's conjecture on optimal rulers. Every optimal ruler with more than $13$ segments is a Wichmann ruler $W(r, s)$ (up to reflection, i.e. reversing the segment list). Posed by Wichmann [Wi63]; the finitely many known exceptions all have at most $13$ segments (lengths $1, 13, 17, 23, 58$), and no further exceptions are known up to length $213$.