SparseRuler.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 1 contain sorry, 0 declared as axioms

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 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\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

Imports (2)

def SparseRuler.marks A ruler is described by its list of segment lengths (gaps) g, so that its marks are the partial sums line 53 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Finset
Proof uses: Finset.image, List.sum, List.take, Finset.range, HAdd.hAdd, List.length, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def marks (g : List ℕ) : Finset ℕ :=
…
```
def SparseRuler.IsComplete 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 line 59 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: Finset.IsDifferenceBasis, SparseRuler.marks, Finset.range, HAdd.hAdd, List.sum, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def IsComplete (g : List ℕ) : Prop :=
…
```
def SparseRuler.IsMinimal A complete ruler is minimal if no complete ruler of the same length $L$ has fewer marks (equivalently, fewer segments) line 64 source
Source documentation
A complete ruler is minimal if no complete ruler of the same length $L$ has fewer marks (equivalently, fewer segments).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: And, SparseRuler.IsComplete, Eq, List.sum, LE.le, List.length
4 instances, coercions and auxiliary constants left out.
```
def IsMinimal (g : List ℕ) : Prop :=
…
```
def SparseRuler.IsMaximal A complete ruler is maximal if no complete ruler with the same number of marks (equivalently, the same number of segments) has greater length line 69 source
Source documentation
A complete ruler is maximal if no complete ruler with the same number of marks (equivalently, the same number of segments) has greater length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: And, SparseRuler.IsComplete, Eq, List.length, LE.le, List.sum
4 instances, coercions and auxiliary constants left out.
```
def IsMaximal (g : List ℕ) : Prop :=
…
```
def SparseRuler.IsOptimal A ruler is optimal if it is both minimal and maximal line 73 source
Source documentation
A ruler is optimal if it is both minimal and maximal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: And, SparseRuler.IsMinimal, SparseRuler.IsMaximal
```
def IsOptimal (g : List ℕ) : Prop := IsMinimal g ∧ IsMaximal g
```
Mentions: SparseRuler.IsMinimal, SparseRuler.IsMaximal
def SparseRuler.wichmannGaps The Wichmann ruler line 78 source
Source documentation
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$.

no axioms what this means
Statement uses: Nat, List
Proof uses: HAppend.hAppend, List.replicate, OfNat.ofNat, List.cons, HAdd.hAdd, List.nil, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
def wichmannGaps (r s : ℕ) : List ℕ :=
…
```
lemma SparseRuler.wichmannGaps_length The Wichmann ruler $W(r, s)$ has $4r + s + 2$ segments, hence $4r + s + 3$ marks [Wi63] line 84 source
Source documentation
The Wichmann ruler $W(r, s)$ has $4r + s + 2$ segments, hence $4r + s + 3$ marks [Wi63].

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, List.length, SparseRuler.wichmannGaps, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, HAppend.hAppend, List, List.replicate, List.cons, List.nil, List.length_append, congr, List.length_replicate, Decidable.byContradiction, Not
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma wichmannGaps_length (r s : ℕ) : (wichmannGaps r s).length = 4 * r + s + 2 := by
…
```
Mentions: SparseRuler.wichmannGaps
lemma SparseRuler.wichmannGaps_sum The Wichmann ruler $W(r, s)$ has length $4r(r + s + 2) + 3(s + 1)$ [Wi63] line 91 source
Source documentation
The Wichmann ruler $W(r, s)$ has length $4r(r + s + 2) + 3(s + 1)$ [Wi63].

standard axioms: propext what this means
Statement uses: Nat, Eq, List.sum, SparseRuler.wichmannGaps, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, HAppend.hAppend, List, List.replicate, List.cons, List.nil, List.sum_append, congr, List.sum_replicate, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 22 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma wichmannGaps_sum (r s : ℕ) :
    (wichmannGaps r s).sum = 4 * r * (r + s + 2) + 3 * (s + 1) := by
…
```
Mentions: SparseRuler.wichmannGaps
theorem SparseRuler.wichmann_conjecture Wichmann's conjecture on optimal rulers sorry line 104 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Exists, Nat, List, SparseRuler.IsOptimal, LT.lt, List.sum, Or, Eq, SparseRuler.wichmannGaps, List.reverse
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem wichmann_conjecture :
    ∃ N : ℕ, ∀ g : List ℕ, IsOptimal g → N < g.sum →
      ∃ r s : ℕ, g = wichmannGaps r s ∨ g = (wichmannGaps r s).reverse := by
…
```
Mentions: SparseRuler.IsOptimal, SparseRuler.wichmannGaps