The subword counting game

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

definition

Natural Language Statement

Definition

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.

Concept map

100%

Preparing this local graph with the browser’s fonts…

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 1 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 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

Builds on

none

Used by

From Mathlib