Reconstruction with Lyndon patterns

Lax100001.Lyndon · concepts/Lax100001/Lyndon.lean · lax-100001

proven

Natural Language Statement

Theorem

Every query is a Lyndon word: it is smaller than each of its proper rotations. Even so, every binary word can be reconstructed. The number of queries on a word of length $n$ is at most a constant times $1 + \log_2 n$ , where $\log_2$ is the integer logarithm, which rounds down.

Concept map

100%

Preparing this local graph with the browser’s fonts…

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax100001.Lyndon

⊢Lax100001Proofs.lyndon_reconstruction

In the paper

page 2 of this submission's paper

Lean source

Show types on hover

1	/-
2	Copyright (c) 2026 Anonymous. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	Authors: ChatGPT (OpenAI), Claude (Anthropic)
5	-/
6	import Lax100001.Counting
7	import Mathlib.Data.Nat.Log
8
9	/-!
10	---
11	title: Reconstruction with Lyndon patterns
12	type: theorem
13	---
14	Every query is a Lyndon word: it is smaller than each of its proper rotations. Even so, every
15	binary word can be reconstructed. The number of queries on a word of length $n$ is at most a
16	constant times $1 + \log_2 n$ , where $\log_2$ is the integer logarithm, which rounds down.
17	-/
18
19	namespace Lax100001.Lyndon
20
21	/-- The bound $1 + \log_2 n$ on the number of queries for a word of length $n$ . The integer
22	logarithm $\texttt{Nat.log 2 n}$ is the largest $k$ with $2^k \le n$ , and $0$ when $n = 0$ . For
23	example $\texttt{Nat.log 2 8} = 3$ and $\texttt{Nat.log 2 9} = 3$ . -/
24	def rate (n : ℕ) : ℝ := ((1 + Nat.log 2 n : ℕ) : ℝ)
25
26	/-- One rule reconstructs every binary word with Lyndon queries only, using a number of queries
27	that is at most a constant times $\mathit{rate}$ . -/
28	axiom reconstruction : Counting.Reconstructs Counting.IsLyndon rate
29
30	end Lax100001.Lyndon
31

Builds on

Lax100001.Counting

Used by

none

From Mathlib

Mathlib.Data.Nat.Log