OAI/Combinatorics/BinaryEdit/FiniteWordPrimeSeparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_append_child line 17

   Source documentation

   Appending a child multiplies the actual word period by that child's prime.

   theorem wordPeriod_append_child {m k : ℕ}
       (primes : Fin k → Fin m → ℕ) (i₀ i : Fin m) (p : List (Fin m))
       (hp : p.length < k) :
       wordPeriod primes i₀ (p ++ [i]) =
         wordPeriod primes i₀ p * primes ⟨p.length, hp⟩ i := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod

2. theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_coprime_level line 27

   Source documentation

   Prefix/current-level coprimality transported to the actual word period.

   theorem wordPeriod_coprime_level {m k : ℕ}
       (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (p : List (Fin m))
       (hp : p.length < k)
       (hinj : Function.Injective (fun z : Fin k × Fin m => primes z.1 z.2))
       (hprime : ∀ q i, Nat.Prime (primes q i)) (hodd : ∀ q i, primes q i ≠ 2) :
       Nat.Coprime (wordPeriod primes i₀ p)
         (FiniteVectors.levelProduct primes ⟨p.length, hp⟩) :=
   …

   Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct

3. theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_half_children line 40

   Source documentation

   At least half the actual children have a nonzero relative row shift. All prefixes, all legal row pairs (including equal rows), and every nonzero parent-period residue are included. No upper bound on primes is needed.

   theorem finiteWord_half_children {k : ℕ} (hk : 2 ≤ k)
       (primes : Fin k → Fin (20 * k) → ℕ) (i₀ : Fin (20 * k))
       (p : List (Fin (20 * k))) (hp : p.length < k)
       (hinj : Function.Injective
         (fun z : Fin k × Fin (20 * k) => primes z.1 z.2))
       (hprime : ∀ q i, Nat.Prime (primes q i))
       (hlarge : ∀ q i, k ^ 4 ≤ primes q i)
       (a b : Fin (k ^ (20 * k))) (t : ℤ)
       (ht : ¬ (wordPeriod primes i₀ p : ℤ) ∣ t) :
       20 * k ≤ 2 * (Finset.univ.filter fun i : Fin (20 * k) =>
         ¬ (wordPeriod primes i₀ (p ++ [i]) : ℤ) ∣
           (b : ℤ) - (a : ℤ) +
   …

   Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod