Paper

Reconstructing Binary Words of Unknown Length with #-Subword Queries

19 pages · 13 marked passages · pdflatex · download PDF · lax-100001

defLax100001.Counting

The subword counting game

A guesser must find a hidden binary word. It may ask how often a chosen word occurs in the hidden word as a subword. The letters of the chosen word are matched, in order, to letters of the hidden word, and letters of the hidden word may be skipped. Occurrences that use different positions are counted separately. For example, $\texttt{01}$ occurs five times in $\texttt{010110}$ .

The guesser is a rule. It sees its earlier queries together with the answers, and then either asks one more query or stops with a guess. A history is a run of the rule when every answer is true, every query is the one that the rule asks after the exchanges before it, and the rule finally stops with the hidden word. A rule reconstructs all words, with a bound on the number of queries, when one rule, one constant and one length threshold work for every hidden word. The run uses only allowed queries, and a hidden word of length $n$ at least the threshold needs at most $C \cdot \mathrm{rate}(n)$ exchanges.

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 Mathlib.Data.List.Count
7	import Mathlib.Data.List.Lex
8	import Mathlib.Data.List.Sublists
9	import Mathlib.Data.Real.Basic
10
11	/-!
12	---
13	title: The subword counting game
14	type: definition
15	---
16	A guesser must find a hidden binary word. It may ask how often a chosen word occurs in the
17	hidden word as a subword. The letters of the chosen word are matched, in order, to letters of
18	the hidden word, and letters of the hidden word may be skipped. Occurrences that use different
19	positions are counted separately. For example, $\texttt{01}$ occurs five times in $\texttt{010110}$ .
20
21	The guesser is a rule. It sees its earlier queries together with the answers, and then either
22	asks one more query or stops with a guess. A history is a run of the rule when every answer is
23	true, every query is the one that the rule asks after the exchanges before it, and the rule
24	finally stops with the hidden word. A rule reconstructs all words, with a bound on the number of
25	queries, when one rule, one constant and one length threshold work for every hidden word. The
26	run uses only allowed queries, and a hidden word of length $n$ at least the threshold needs at
27	most $C \cdot \mathrm{rate}(n)$ exchanges.
28	-/
29
30	namespace Lax100001.Counting
31
32	/-- A binary word, written as a list of bits. The bit $\texttt{false}$ is the letter $\texttt{0}$
33	and the bit $\texttt{true}$ is the letter $\texttt{1}$ . -/
34	abbrev Word := List Bool
35
36	/-- The number of occurrences of $\mathit{pattern}$ in $\mathit{word}$ as a subword.
37
38	An occurrence is a choice of positions of $\mathit{word}$ , from left to right, whose letters spell
39	$\mathit{pattern}$ . The list $\texttt{word.sublists}$ has one entry for each choice of positions, so
40	counting the entries equal to $\mathit{pattern}$ counts the occurrences. For example,
41	$\texttt{count [false, true, false, true, true, false] [false, true]} = 5$ . The word is
42	$\texttt{010110}$ , and the pattern $\texttt{01}$ is spelled by the positions $(1, 2)$ , $(1, 4)$ ,
43	$(1, 5)$ , $(3, 4)$ and $(3, 5)$ . -/
44	def count (word pattern : Word) : ℕ := word.sublists.count pattern
45
46	/-- One question and the answer that the guesser received. -/
47	structure Exchange where
48	/-- The word whose occurrences the guesser asked for. -/
49	query : Word
50	/-- The number of occurrences that the guesser was told. -/
51	answer : ℕ
52
53	/-- What the guesser does next: ask for another count, or stop with a guess. -/
54	inductive Move where
55	/-- Ask for the number of occurrences of $\mathit{query}$ in the hidden word. -/
56	\| ask (query : Word)
57	/-- Stop and name $\mathit{guess}$ as the hidden word. -/
58	\| stop (guess : Word)
59
60	/-- A guesser. It sees the earlier exchanges, oldest first, and chooses its next move. The
61	empty list is what it sees at the start. -/
62	abbrev Rule := List Exchange → Move
63
64	/-- $\mathit{history}$ is a complete play of $\mathit{rule}$ against the hidden word
65	$\mathit{word}$ .
66
67	Every answer in the history is true. Every query in the history is the one that the rule asks
68	when it has seen only the exchanges before it. After the last exchange the rule stops with
69	the hidden word. For example, let a rule ask $\texttt{0}$ first and stop with $\texttt{000}$ after
70	the answer $3$ . Then $[\langle[\texttt{false}], 3\rangle]$ is a run of this rule against the hidden
71	word $\texttt{000}$ . -/ structure IsRun (rule : Rule) (word : Word) (history : List Exchange) : Prop
72	where
73	/-- Every answer is the number of occurrences of its query in the hidden word. -/
74	answers_true : ∀ e ∈ history, e.answer = count word e.query
75	/-- Each query is the one that the rule asks after the exchanges before it. -/
76	asks_next : ∀ (i : ℕ) (hi : i < history.length),
77	rule (history.take i) = .ask history[i].query
78	/-- After the whole history the rule stops with the hidden word. -/
79	stops : rule history = .stop word
80
81	/-- A nonempty word is a Lyndon word when it is smaller than each of its proper rotations.
82
83	Words are compared in dictionary order, with $0 < 1$ . For example $\texttt{0}$ , $\texttt{01}$ and
84	$\texttt{0011}$ are Lyndon words, while $\texttt{10}$ and $\texttt{0101}$ are not. -/
85	def IsLyndon (pattern : Word) : Prop :=
86	pattern ≠ [] ∧ ∀ k, 0 < k → k < pattern.length →
87	pattern < pattern.drop k ++ pattern.take k
88
89	/-- One rule reconstructs every binary word, asks only allowed queries, and uses few queries.
90
91	There are a rule, a positive constant and a length threshold such that every hidden word has a
92	run of the rule in which every query satisfies $\mathit{allowed}$ . When the hidden word has length
93	$n$ at least the threshold, the run has at most $C \cdot \mathrm{rate}(n)$ exchanges. The rule is
94	chosen before the hidden word, so it does not know $n$ , which occurs only in the bound. -/
95	def Reconstructs (allowed : Word → Prop) (rate : ℕ → ℝ) : Prop :=
96	∃ rule : Rule, ∃ constant : ℝ, 0 < constant ∧ ∃ threshold : ℕ,
97	∀ word : Word, ∃ history : List Exchange,
98	IsRun rule word history ∧ (∀ e ∈ history, allowed e.query) ∧
99	(threshold ≤ word.length → (history.length : ℝ) ≤ constant * rate word.length)
100
101	end Lax100001.Counting
102

thm✓Lax100001.Unrestricted

thm✓Lax100001.Lyndon

thm✓Lax100001.Rows

Counting a zero followed by ones

The ones of a binary word cut its zeros into groups. Group $s$ holds the zeros that have exactly $s$ ones before them. A word with $J$ ones has the groups $0, 1, \ldots, J$ . The number of occurrences of $\texttt{0}$ followed by $r$ ones is determined by the sizes of these groups: a zero in group $s$ has $J - s$ ones after it, and it starts as many occurrences as there are ways to choose $r$ of those ones.

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.Algebra.BigOperators.Group.Finset.Basic
8	import Mathlib.Data.Nat.Choose.Basic
9
10	/-!
11	---
12	title: Counting a zero followed by ones
13	type: theorem
14	---
15	The ones of a binary word cut its zeros into groups. Group $s$ holds the zeros that have exactly
16	$s$ ones before them. A word with $J$ ones has the groups $0, 1, \ldots, J$ . The number of
17	occurrences of $\texttt{0}$ followed by $r$ ones is determined by the sizes of these groups: a zero
18	in group $s$ has $J - s$ ones after it, and it starts as many occurrences as there are ways to
19	choose $r$ of those ones.
20	-/
21
22	namespace Lax100001.Rows
23
24	open Counting
25
26	/-- The sizes of the groups of zeros of $\mathit{word}$ .
27
28	Entry $s$ counts the zeros of $\mathit{word}$ that have exactly $s$ ones before them, and the list
29	has one entry for each of the $J + 1$ groups, where $J$ is the number of ones. For example,
30	$\texttt{groups [false, true, false, true, true, false]} = [1, 1, 0, 1]$ : the word $\texttt{010110}$
31	has one zero before the first one, one between the first and second ones, none between the second
32	and third ones, and one after the third one. -/
33	def groups : Word → List ℕ
34	\| [] => [0]
35	\| true :: tail => 0 :: groups tail
36	\| false :: tail =>
37	match groups tail with
38	\| [] => [1]
39	\| a :: rest => (a + 1) :: rest
40
41	/-- The number of occurrences of $\texttt{0}$ followed by $r$ ones in a word is the sum over the
42	groups $s$ of the size of group $s$ times $\binom{J-s}{r}$ , where $J$ is the number of ones and
43	$J + 1$ is the number of groups. For the word $\texttt{010110}$ and $r = 2$ the groups are
44	$[1, 1, 0, 1]$ . The sum is
45	$1 \cdot \binom{3}{2} + 1 \cdot \binom{2}{2} + 0 \cdot \binom{1}{2} + 1 \cdot \binom{0}{2}$ , which
46	is $4$ .
47	-/
48	axiom count_zero_ones (word : Word) (r : ℕ) :
49	count word (false :: List.replicate r true) =
50	∑ s ∈ Finset.range (groups word).length,
51	(groups word)[s]! * ((groups word).length - 1 - s).choose r
52
53	end Lax100001.Rows
54

⊢Lax100001Proofs.count_zero_ones

thm✓Lax100001.Tail

⊢Lax100001Proofs.tail_le

thm✓Lax100001.Peel

Peeling

Let $P_d(s)$ be the product of $1 - s/i$ over $i = 1, \ldots, d$ . It is $1$ at $s = 0$ . At a natural number $s \ge 1$ it is $(-1)^d$ times the binomial coefficient of $s - 1$ and $d$ , so it vanishes for $1 \le s \le d$ . Take numbers $g(s)$ and weights $\omega(s)$ for $s = 0, \ldots, N$ , with $\omega(0) = 1$ , and put $S = \sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ . Then $S - g(0)$ is $(-1)^d$ times the sum of $g(s)\,\omega(s)\binom{s-1}{d}$ over $1 \le s \le N$ . So $S$ keeps $g(0)$ , drops the next $d$ terms, and leaves a remainder that is small when the later terms are small. This is called peeling. It has three consequences.

If all $g(s)$ and $\omega(s)$ are nonnegative, then $(-1)^d (S - g(0)) \ge 0$ .
Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If $g(s)\,\omega(s) \le M y^s$ for $1 \le s \le N$ , then $(-1)^d (S - g(0)) < 1$ . This needs no sign condition on $g$ and $\omega$ .
Let $g$ and $g'$ be sequences of natural numbers that both satisfy this bound, with nonnegative weights. If they give the same $S$ , then $g(0) = g'(0)$ .

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 Mathlib.Algebra.BigOperators.Group.Finset.Defs
7	import Mathlib.Data.Rat.Defs
8	import Mathlib.Order.Interval.Finset.Nat
9
10	/-!
11	---
12	title: Peeling
13	type: theorem
14	---
15	Let $P_d(s)$ be the product of $1 - s/i$ over $i = 1, \ldots, d$ . It is $1$ at $s = 0$ . At a natural
16	number $s \ge 1$ it is $(-1)^d$ times the binomial coefficient of $s - 1$ and $d$ , so it vanishes
17	for $1 \le s \le d$ . Take numbers $g(s)$ and weights $\omega(s)$ for $s = 0, \ldots, N$ , with
18	$\omega(0) = 1$ , and put $S = \sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ . Then $S - g(0)$ is $(-1)^d$
19	times the sum of $g(s)\,\omega(s)\binom{s-1}{d}$ over $1 \le s \le N$ . So $S$ keeps $g(0)$ , drops
20	the next $d$ terms, and leaves a remainder that is small when the later terms are small. This is
21	called peeling. It has three consequences.
22
23	1. If all $g(s)$ and $\omega(s)$ are nonnegative, then $(-1)^d (S - g(0)) \ge 0$ .
24	2. Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If
25	$g(s)\,\omega(s) \le M y^s$ for $1 \le s \le N$ , then $(-1)^d (S - g(0)) < 1$ . This needs no
26	sign condition on $g$ and $\omega$ .
27	3. Let $g$ and $g'$ be sequences of natural numbers that both satisfy this bound, with nonnegative
28	weights. If they give the same $S$ , then $g(0) = g'(0)$ .
29	-/
30
31	namespace Lax100001.Peel
32
33	/-- The polynomial $P_d(s) = \prod_{i=1}^{d} (1 - s/i)$ of degree $d$ in $s$ . The index $i + 1$ lets
34	the product range over $\texttt{Finset.range d}$ . For example $P_2(s) = (1 - s)(1 - s/2)$ , which
35	takes the values $1, 0, 0, 1, 3, 6$ at $s = 0, \ldots, 5$ . -/
36	def P (d : ℕ) (s : ℚ) : ℚ := ∏ i ∈ Finset.range d, (1 - s / (i + 1))
37
38	/-- For nonnegative $g$ and $\omega$ with $\omega(0) = 1$ , the weighted sum
39	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ differs from $g(0)$ by $(-1)^d$ times a nonnegative number.
40	So it is at least $g(0)$ if $d$ is even, and at most $g(0)$ if $d$ is odd. -/
41	axiom sign_nonneg (d N : ℕ) (g ω : ℕ → ℚ) (hg : ∀ s ≤ N, 0 ≤ g s) (hω : ∀ s ≤ N, 0 ≤ ω s)
42	(hω₀ : ω 0 = 1) :
43	0 ≤ (-1) ^ d * (∑ s ∈ Finset.range (N + 1), g s * ω s * P d s - g 0)
44
45	/-- Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If $g(s)\,\omega(s) \le M y^s$
46	for $1 \le s \le N$ , and $\omega(0) = 1$ , then the weighted sum
47	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ differs from $g(0)$ by $(-1)^d$ times a number that is less
48	than $1$ . No sign condition on $g$ and $\omega$ is needed. -/
49	axiom lt_one (d N : ℕ) (y M : ℚ) (g ω : ℕ → ℚ) (hω₀ : ω 0 = 1) (hy : 0 ≤ y) (hy₁ : y < 1)
50	(hM : M * (y / (1 - y)) ^ (d + 1) < 1) (hgω : ∀ s ∈ Finset.Icc 1 N, g s * ω s ≤ M * y ^ s) :
51	(-1) ^ d * (∑ s ∈ Finset.range (N + 1), g s * ω s * P d s - g 0) < 1
52
53	/-- Two sequences $g$ and $g'$ of natural numbers that satisfy the bounds of $\texttt{lt\_one}$ ,
54	with nonnegative weights $\omega$ , and have the same weighted sum
55	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ , have the same first entry. -/
56	axiom head_eq (d N : ℕ) (y M : ℚ) (g g' : ℕ → ℕ) (ω : ℕ → ℚ) (hω : ∀ s ≤ N, 0 ≤ ω s)
57	(hω₀ : ω 0 = 1) (hy : 0 ≤ y) (hy₁ : y < 1) (hM : M * (y / (1 - y)) ^ (d + 1) < 1)
58	(hg : ∀ s ∈ Finset.Icc 1 N, g s * ω s ≤ M * y ^ s)
59	(hg' : ∀ s ∈ Finset.Icc 1 N, g' s * ω s ≤ M * y ^ s)
60	(hS : ∑ s ∈ Finset.range (N + 1), g s * ω s * P d s =
61	∑ s ∈ Finset.range (N + 1), g' s * ω s * P d s) :
62	g 0 = g' 0
63
64	end Lax100001.Peel
65

Loading the paper…