VC-dimensions of nondeterministic finite automata for words of equal length

Definition 10, Lemma 11, and Lemma 12 from the paper.
(Bonus material for ac-exercises)

theorem rescue_lemma_12 {m : ℕ} : (2 * m.succ).succ < 2 ^ Nat.clog 2 (2 * m.succ).succ

def ν₂ (n : ℕ) : ℕ

ν₂ is called t in the paper.

Equations

• ν₂ = padicValNat 2

theorem ν₂_odd (n : ℕ) : ν₂ (2 * n + 1) = 0

theorem ν₂_2 (n : ℕ) (h : 0 < n) : ν₂ (2 * n) = ν₂ n + 1

theorem bits_odd {n : ℕ} : (2 * n + 1).bits = true :: n.bits

theorem bits_even {n : ℕ} (h : n ≠ 0) : (2 * n).bits = false :: n.bits

theorem length_map_sum (l : List Bool) : (List.map Bool.toNat l).sum ≤ l.length

def hammingBits (n : ℕ) : ℕ

Equations

• hammingBits n = (List.map Bool.toNat n.bits).sum

theorem hammingBits_2 (n : ℕ) : hammingBits (2 * n) = hammingBits n

theorem hammingBits_odd (n : ℕ) : hammingBits (2 * n + 1) = hammingBits n + 1

theorem mentioned_in_lemma_12 {n : ℕ} {s : ℕ} (h : n < 2 ^ s) : hammingBits n ≤ s

theorem andhence {m : ℕ} : hammingBits (2 * m.succ) < Nat.clog 2 (2 * m.succ).succ

theorem ν₂_hammingBits (n : ℕ) : ν₂ (n + 1) + hammingBits (n + 1) = hammingBits n + 1

def arndt : ℕ → ℕ

This function is called a at https://oeis.org/A005187 and we name it in honor of Jörg Arndt.

Equations

• arndt 0 = 0
• arndt k.succ = arndt k + 1 + ν₂ (k + 1)

theorem lemma11 (m : ℕ) : arndt m + hammingBits (2 * m) = 2 * m

Jörg Arndt (2019) claimed this without proof as a resolution of a conjecture of Benoit Cloitre (2003). Cloitre is a coauthor of Shallit (2023) and Jean-Paul Allouche.

theorem lemma12 (n : ℕ) : arndt n + Nat.clog 2 n.succ ≥ 2 * n