OAI/Combinatorics/BinaryEdit/FiniteVectors.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Concrete vectors for the finite tree (finite-tree.tex, finite-vectors). A prefix is represented by its depth and any full leaf path extending it. All definitions ignore the unused tail of that representative. No primality assumption is needed for the annihilation and recursive vector identities.

  1. abbrev OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf line 16
  2. def OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees line 18
  3. instance OAI.TreeEdit.BinaryLower.FiniteVectors.(instance at line 21) line 21
  4. def OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct line 24
  5. def OAI.TreeEdit.BinaryLower.FiniteVectors.suffixScale line 26
  6. def OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod line 29
  7. def OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod line 32
  8. abbrev OAI.TreeEdit.BinaryLower.FiniteVectors.State line 35
  9. def OAI.TreeEdit.BinaryLower.FiniteVectors.w line 38

    Source documentation

    Distinguished subtree vector, with the common suffix coefficient.

    def w (p : Fin k → Fin m → ℕ) (j : ℕ) (a : Leaf m k) : State p :=
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.State

  10. def OAI.TreeEdit.BinaryLower.FiniteVectors.u line 42

    Source documentation

    Cheap row-advancing vector.

    def u (p : Fin k → Fin m → ℕ) (j : ℕ) (a : Leaf m k) : State p :=
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.State

  11. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_zero line 45
  12. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.suffixScale_top line 48
  13. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.suffixScale_succ line 54
  14. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod_dvd line 73

    Source documentation

    The full leaf modulus divides its prefix period times the suffix scale.

    lemma leafPeriod_dvd (p : Fin k → Fin m → ℕ) (j : ℕ) (a b : Leaf m k)
    (hab : Agrees j a b) : leafPeriod p b ∣ prefixPeriod p j a * suffixScale p j := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.suffixScale

  15. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_nsmul_w line 89

    Source documentation

    Every node vector is annihilated by its prescribed prefix period.

    theorem prefixPeriod_nsmul_w (p : Fin k → Fin m → ℕ) (j : ℕ) (a : Leaf m k) :
    prefixPeriod p j a • w p j a = 0 := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.w

  16. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.w_eq_level_nsmul_u line 100

    Source documentation

    Multiplication of the cheap vector by the current level product gives w.

    theorem w_eq_level_nsmul_u (p : Fin k → Fin m → ℕ) (j : ℕ) (hj : j < k)
    (a : Leaf m k) : w p j a = levelProduct p ⟨j, hj⟩ • u p j a := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.w, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct, OAI.TreeEdit.BinaryLower.FiniteVectors.u

  17. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_child_iff line 110
  18. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.u_eq_sum_child_w line 129

    Source documentation

    The cheap vector is exactly the sum of the children's distinguished vectors.

    theorem u_eq_sum_child_w (p : Fin k → Fin m → ℕ) (j : ℕ) (hj : j < k)
    (a : Leaf m k) :
    u p j a = ∑ i : Fin m, w p (j + 1) (Function.update a ⟨j, hj⟩ i) := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.u, OAI.TreeEdit.BinaryLower.FiniteVectors.w

  19. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_top_iff line 138
  20. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.w_leaf line 147

    Source documentation

    At a leaf, the distinguished vector is the coordinate unit vector.

    theorem w_leaf (p : Fin k → Fin m → ℕ) (a b : Leaf m k) :
    w p k a b = if b = a then 1 else 0 := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.w

  21. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_refl line 151
  22. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_symm line 155
  23. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_trans line 159
  24. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.agrees_iff_of_agrees line 164
  25. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_eq_of_agrees line 168
  26. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.w_eq_of_agrees line 176
  27. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.u_eq_of_agrees line 181
  28. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_child line 186
  29. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_top line 214
  30. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod_pos line 218
  31. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_pos line 226
  32. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.state_finite line 235

    Source documentation

    Positive leaf moduli make the manuscript's parameter group finite.

    theorem state_finite (p : Fin k → Fin m → ℕ) (hp : ∀ q i, 0 < p q i) :
    Finite (State p) := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.State

  33. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_eq_prod_cast line 242

    Source documentation

    Prefix products agree with the usual dependent Fin j path product.

    lemma prefixPeriod_eq_prod_cast (p : Fin k → Fin m → ℕ) (j : ℕ) (hj : j ≤ k)
    (a : Leaf m k) : prefixPeriod p j a =
      2 * ∏ q : Fin j, p (Fin.castLE hj q) (a (Fin.castLE hj q)) := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod

  34. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_le line 261

    Source documentation

    The source's period upper bound, on the concrete vector prefix periods.

    lemma prefixPeriod_le (p : Fin k → Fin m → ℕ) (hp : ∀ q i, p q i ≤ k ^ 5)
    (j : ℕ) (hj : j ≤ k) (a : Leaf m k) : prefixPeriod p j a ≤ 2 * k ^ (5 * j) := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod

  35. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_coprime_level line 272

    Source documentation

    Distinct odd depth/child primes make the prefix period coprime to the current level. This is a specialization to the concrete vector API of the prime-product coprimality calculation in lem:orders.

    lemma prefixPeriod_coprime_level (p : Fin k → Fin m → ℕ)
    (hinj : Function.Injective (fun z : Fin k × Fin m => p z.1 z.2))
    (hprime : ∀ q i, Nat.Prime (p q i)) (hodd : ∀ q i, p q i ≠ 2)
    (j : ℕ) (hj : j < k) (a : Leaf m k) :
    Nat.Coprime (prefixPeriod p j a) (levelProduct p ⟨j, hj⟩) := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct

  36. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.prefixPeriod_zsmul_w line 294
  37. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.zsmul_w_eq_mul_u line 298
  38. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.leaf_shift_eq_iff line 308

    Source documentation

    The leaf coordinate changes under exactly the nonzero period residues, including negative translations. This is the base case of separation.

    lemma leaf_shift_eq_iff (p : Fin k → Fin m → ℕ) (a : Leaf m k)
    (x : State p) (t : ℤ) :
    (x + t • w p k a) a = x a ↔ (leafPeriod p a : ℤ) ∣ t := by
…

    Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.State, OAI.TreeEdit.BinaryLower.FiniteVectors.w, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod

  39. lemma OAI.TreeEdit.BinaryLower.FiniteVectors.leaf_shift_ne_iff line 314