Sparse Ruler

The question

Wichmann's conjecture on optimal rulers. Every optimal ruler of sufficiently large length is a Wichmann ruler $W (r, s)$ (up to reflection, i.e. reversing the segment list). Posed by Wichmann [Wi63]. The Wikipedia article records that no optimal ruler of length $1, 13, 17, 23$ or $58$ is a Wichmann ruler, and that every other optimal length up to $213$ is attained by one; non-Wichmann optimal rulers also occur alongside Wichmann ones at lengths $9, 29, 50$ and $68$ .

A sparse ruler of length $L$ is a sequence of marks $0 = a_{1} < a_{2} < \dots < a_{m} = L$ . A distance $k \in 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 speculated that every sufficiently large optimal ruler is of his type. The Wikipedia article records that no optimal ruler of length $1, 13, 17, 23$ or $58$ is a Wichmann ruler, and that every other optimal length up to $213$ is attained by one; non-Wichmann optimal rulers also occur alongside Wichmann ones at lengths $9, 29, 50$ and $68$ .

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 \dots, 3]$ — is the subject of FormalConjectures.ErdosProblems.«170» (there phrased via $F (N) / N$ ), and is not restated here.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.SparseRuler.

theorem wichmann_conjecture :
    ∃ N : ℕ, ∀ g : List ℕ, IsOptimal g → N < g.sum →
      ∃ r s : ℕ, g = wichmannGaps r s ∨ g = (wichmannGaps r s).reverse

What counts as progress

A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

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

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.

Current state

The problem