Sublogarithmic reconstruction

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

proven

Natural Language Statement

Theorem

Every binary word can be reconstructed using ordinary exact counts. The number of queries on a word of length $n$ is at most a constant times the square root of $\log_2 n \cdot \log_2 \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.Unrestricted

⊢Lax100001Proofs.unrestricted_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.Analysis.Real.Sqrt
8	import Mathlib.Data.Nat.Log
9
10	/-!
11	---
12	title: Sublogarithmic reconstruction
13	type: theorem
14	---
15	Every binary word can be reconstructed using ordinary exact counts. The number of queries on a
16	word of length $n$ is at most a constant times the square root of $\log_2 n \cdot \log_2 \log_2 n$ ,
17	where $\log_2$ is the integer logarithm, which rounds down.
18	-/
19
20	namespace Lax100001.Unrestricted
21
22	/-- The bound $\sqrt{\log_2 n \cdot \log_2 \log_2 n}$ on the number of queries for a word of length
23	$n$ . The integer logarithm $\texttt{Nat.log 2 n}$ is the largest $k$ with $2^k \le n$ , and $0$ when
24	$n = 0$ . For example $\texttt{Nat.log 2 8} = 3$ and $\texttt{Nat.log 2 9} = 3$ . -/
25	noncomputable def rate (n : ℕ) : ℝ :=
26	√((Nat.log 2 n : ℝ) * (Nat.log 2 (Nat.log 2 n) : ℝ))
27
28	/-- One rule reconstructs every binary word with any queries allowed, using a number of queries
29	that is at most a constant times $\mathit{rate}$ . -/
30	axiom reconstruction : Counting.Reconstructs (fun _ ↦ True) rate
31
32	end Lax100001.Unrestricted
33

Builds on

Lax100001.Counting

Used by

none

From Mathlib