Counting a zero followed by ones

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

proven

Natural Language Statement

Theorem

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.

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.Rows

⊢Lax100001Proofs.count_zero_ones

In the paper

page 4 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.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

Builds on

Lax100001.Counting

Used by

none

From Mathlib