FiniteSeparation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Geometric separation for the concrete finite tree

The prime construction supplies the half-child condition in the geometric induction.

def OAI.TreeEdit.BinaryLower.FiniteTree.finiteBlocks line 22
Source documentation
Literal row/block array of a concrete node word.
```
def finiteBlocks {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (T h : ℕ) (p : List (Fin m)) (x : State (wordPeriods primes)) :
    Fin T → Fin m → Word (Symbol (wordPeriods primes)) ((m * T) ^ h) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.FiniteTree.Symbol
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_succ_eq_rows line 28

def OAI.TreeEdit.BinaryLower.FiniteTree.finiteRowShift line 42

Source documentation

The relative coefficient comparing two rows in a child.

def finiteRowShift {m k T : ℕ} (primes : Fin k → Fin m → ℕ)
    (p : List (Fin m)) (hp : p.length < k) (a b : Fin T) (t : ℤ) : ℤ :=
…

def OAI.TreeEdit.BinaryLower.FiniteTree.separatedChildren line 48

Source documentation

Children whose prescribed period does not divide the relative coefficient.

def separatedChildren {m k T : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (p : List (Fin m)) (hp : p.length < k) (a b : Fin T) (t : ℤ) :
    Finset (Fin m) :=
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_separation_of_half_children line 56

Source documentation

Ordered-tag alignment and half-child nondivisibility imply separation for arbitrary common-subsequence matchings.

theorem finiteWord_separation_of_half_children {m k T : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (hm : 2 ≤ m) (hT : 0 < T)
    (hhalf : ∀ p (hp : p.length < k) (a b : Fin T) (t : ℤ),
      ¬ (wordPeriod primes i₀ p : ℤ) ∣ t →
      m ≤ 2 * (separatedChildren primes i₀ p hp a b t).card)
    (h : ℕ) (p : List (Fin m)) (hlen : p.length + h = k)
    (x : State (wordPeriods primes)) (t : ℤ)
    (ht : ¬ (wordPeriod primes i₀ p : ℤ) ∣ t) :
    (((m * T) ^ h : ℕ) : ℝ) / (4 : ℝ) ^ h ≤
      (deficit ((m * T) ^ h) (finiteWord primes i₀ T h p x)
        (finiteWord primes i₀ T h p (x + t • wordW primes i₀ p)) : ℝ) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod, OAI.TreeEdit.BinaryLower.FiniteTree.separatedChildren, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_root_deficit_of_half_children line 123

Source documentation

Uniform separation of the root half-period shift.

theorem finiteWord_root_deficit_of_half_children {m k T : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (hm : 2 ≤ m) (hT : 0 < T)
    (hhalf : ∀ p (hp : p.length < k) (a b : Fin T) (t : ℤ),
      ¬ (wordPeriod primes i₀ p : ℤ) ∣ t →
      m ≤ 2 * (separatedChildren primes i₀ p hp a b t).card)
    (x : State (wordPeriods primes)) :
    (((m * T) ^ k : ℕ) : ℝ) / (4 : ℝ) ^ k ≤
      (deficit ((m * T) ^ k) (finiteWord primes i₀ T k [] x)
        (finiteWord primes i₀ T k [] (x + wordW primes i₀ [])) : ℝ) := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_separation line 137

Source documentation

Source finite-tree separation for the actual prime periods and words.

theorem finiteWord_separation {k : ℕ} (hk : 2 ≤ k)
    (primes : Fin k → Fin (20 * k) → ℕ) (i₀ : Fin (20 * 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)
    (h : ℕ) (p : List (Fin (20 * k))) (hlen : p.length + h = k)
    (x : State (wordPeriods primes)) (t : ℤ)
    (ht : ¬ (wordPeriod primes i₀ p : ℤ) ∣ t) :
    (((20 * k * k ^ (20 * k)) ^ h : ℕ) : ℝ) / (4 : ℝ) ^ h ≤
      (deficit ((20 * k * k ^ (20 * k)) ^ h)
        (finiteWord primes i₀ (k ^ (20 * k)) h p x)
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_root_deficit line 158

Source documentation

Distinct large primes give the uniform root deficit for the prescribed half-period shift.

theorem finiteWord_root_deficit {k : ℕ} (hk : 2 ≤ k)
    (primes : Fin k → Fin (20 * k) → ℕ) (i₀ : Fin (20 * 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)
    (x : State (wordPeriods primes)) :
    (((20 * k * k ^ (20 * k)) ^ k : ℕ) : ℝ) / (4 : ℝ) ^ k ≤
      (deficit ((20 * k * k ^ (20 * k)) ^ k)
        (finiteWord primes i₀ (k ^ (20 * k)) k [] x)
        (finiteWord primes i₀ (k ^ (20 * k)) k []
          (x + wordW primes i₀ [])) : ℝ) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW