FiniteAlphabet.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.parameter_le_word_length line 12
Source documentation
The original (pre-encoding) word length already dominates the tree parameter. This lets any absolute code threshold be met by increasing k.
```
theorem parameter_le_word_length {k : ℕ} (hk : 0 < k) :
    k ≤ (20 * k * k ^ (20 * k)) ^ k := by
…
```
theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.code_threshold line 21
Source documentation
Explicit simultaneous threshold for the original word length and k≥2.
```
theorem code_threshold (M₀ : ℕ) :
    ∀ k ≥ max 2 M₀, 2 ≤ k ∧ M₀ ≤ (20 * k * k ^ (20 * k)) ^ k := by
…
```
theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.residue_budget_le_word_length line 29
Source documentation
The numerical alphabet budget holds already for every k≥2.
```
theorem residue_budget_le_word_length {k : ℕ} (hk : 2 ≤ k) :
    (20 * k) ^ k * (2 * k ^ (5 * k)) ≤ (20 * k * k ^ (20 * k)) ^ k := by
…
```

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.leaf_period_le line 42

Source documentation

Bounding each factor bounds the leaf period from the manuscript.

theorem leaf_period_le {m k : ℕ} (p : Fin k → Fin m → ℕ)
    (hupper : ∀ q i, p q i ≤ k ^ 5) (a : Fin k → Fin m) :
    2 * (∏ q, p q (a q)) ≤ 2 * k ^ (5 * k) := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.leaf_period_pos line 52

Source documentation

Positivity of every factor makes every leaf modulus nonzero.

theorem leaf_period_pos {m k : ℕ} (p : Fin k → Fin m → ℕ)
    (hpos : ∀ q i, 0 < p q i) (a : Fin k → Fin m) :
    0 < 2 * (∏ q, p q (a q)) := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.tagged_alphabet_card_le line 60
Source documentation
Bound the tagged residue alphabet on literal fixed-length leaf words. The local Fintype instances are constructed here, rather than presupposed.
```
theorem tagged_alphabet_card_le {m k H : ℕ}
    (Q : Word (Fin m) k → ℕ)
    (hQpos : ∀ a, 0 < Q a) (hQupper : ∀ a, Q a ≤ H) :
    Nat.card (Σ a : Word (Fin m) k, ZMod (Q a)) ≤ m ^ k * H := by
…
```
Mentions: OAI.TreeEdit.Word

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.finite_tree_alphabet_bounds line 82

Source documentation

The literal tagged residue alphabet satisfies the cardinal hypotheses of the fixed-length binary conversion theorem.

theorem finite_tree_alphabet_bounds {k : ℕ} (hk : 2 ≤ k)
    (Q : Word (Fin (20 * k)) k → ℕ)
    (hQpos : ∀ a, 0 < Q a) (hQupper : ∀ a, Q a ≤ 2 * k ^ (5 * k)) :
    Finite (Σ a : Word (Fin (20 * k)) k, ZMod (Q a)) ∧
    1 ≤ Nat.card (Σ a : Word (Fin (20 * k)) k, ZMod (Q a)) ∧
    Nat.card (Σ a : Word (Fin (20 * k)) k, ZMod (Q a)) ≤
      (20 * k * k ^ (20 * k)) ^ k := by
…

Mentions: OAI.TreeEdit.Word

theorem OAI.TreeEdit.BinaryLower.FiniteAlphabet.prime_product_alphabet_bounds line 103
Source documentation
Specialization to the source's products of one prime from each depth. Only positivity and the upper prime-size bound are needed for cardinality.
```
theorem prime_product_alphabet_bounds {k : ℕ} (hk : 2 ≤ k)
    (p : Fin k → Fin (20 * k) → ℕ)
    (hpos : ∀ q i, 0 < p q i) (hupper : ∀ q i, p q i ≤ k ^ 5) :
    let Q : Word (Fin (20 * k)) k → ℕ := fun a =>
…
```
Mentions: OAI.TreeEdit.Word