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 word represented by a list of letters. The alphabet defaults to bits, where
33	$\texttt{false}$ is the letter $\texttt{0}$ and $\texttt{true}$ is the letter $\texttt{1}$ . -/
34	abbrev Word (α : Type := Bool) := List α
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 {α : Type} [DecidableEq α] (word pattern : Word α) : ℕ :=
45	word.sublists.count pattern
46
47	/-- One question and the answer that the guesser received. -/
48	structure Exchange (α : Type := Bool) where
49	/-- The word whose occurrences the guesser asked for. -/
50	query : Word α
51	/-- The number of occurrences that the guesser was told. -/
52	answer : ℕ
53
54	/-- What the guesser does next: ask for another count, or stop with a guess. -/
55	inductive Move (α : Type := Bool) where
56	/-- Ask for the number of occurrences of $\mathit{query}$ in the hidden word. -/
57	\| ask (query : Word α)
58	/-- Stop and name $\mathit{guess}$ as the hidden word. -/
59	\| stop (guess : Word α)
60
61	/-- A guesser. It sees the earlier exchanges, oldest first, and chooses its next move. The
62	empty list is what it sees at the start. -/
63	abbrev Rule (α : Type := Bool) := List (Exchange α) → Move α
64
65	/-- $\mathit{history}$ is a complete play of $\mathit{rule}$ against the hidden word
66	$\mathit{word}$ .
67
68	Every answer in the history is true. Every query in the history is the one that the rule asks
69	when it has seen only the exchanges before it. After the last exchange the rule stops with
70	the hidden word. For example, let a rule ask $\texttt{0}$ first and stop with $\texttt{000}$ after
71	the answer $3$ . Then $[\langle[\texttt{false}], 3\rangle]$ is a run of this rule against the hidden
72	word $\texttt{000}$ . -/ structure IsRun {α : Type} [DecidableEq α] (rule : Rule α) (word : Word α)
73	(history : List (Exchange α)) : Prop
74	where
75	/-- Every answer is the number of occurrences of its query in the hidden word. -/
76	answers_true : ∀ e ∈ history, e.answer = count word e.query
77	/-- Each query is the one that the rule asks after the exchanges before it. -/
78	asks_next : ∀ (i : ℕ) (hi : i < history.length),
79	rule (history.take i) = .ask history[i].query
80	/-- After the whole history the rule stops with the hidden word. -/
81	stops : rule history = .stop word
82
83	/-- A nonempty word is a Lyndon word when it is smaller than each of its proper rotations.
84
85	Words are compared in dictionary order, with $0 < 1$ . For example $\texttt{0}$ , $\texttt{01}$ and
86	$\texttt{0011}$ are Lyndon words, while $\texttt{10}$ and $\texttt{0101}$ are not. -/
87	def IsLyndon (pattern : Word) : Prop :=
88	pattern ≠ [] ∧ ∀ k, 0 < k → k < pattern.length →
89	pattern < pattern.drop k ++ pattern.take k
90
91	/-- One rule reconstructs every binary word, asks only allowed queries, and uses few queries.
92
93	There are a rule, a positive constant and a length threshold such that every hidden word has a
94	run of the rule in which every query satisfies $\mathit{allowed}$ . When the hidden word has length
95	$n$ at least the threshold, the run has at most $C \cdot \mathrm{rate}(n)$ exchanges. The rule is
96	chosen before the hidden word, so it does not know $n$ , which occurs only in the bound. -/
97	def Reconstructs (allowed : Word → Prop) (rate : ℕ → ℝ) : Prop :=
98	∃ rule : Rule, ∃ constant : ℝ, 0 < constant ∧ ∃ threshold : ℕ,
99	∀ word : Word, ∃ history : List Exchange,
100	IsRun rule word history ∧ (∀ e ∈ history, allowed e.query) ∧
101	(threshold ≤ word.length → (history.length : ℝ) ≤ constant * rate word.length)
102
103	end Lax100001.Counting
104

Builds on

none

Used by

From Mathlib