GeneratorWordPadding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed-length generator words and their consecutive prefixes

theorem OAI.PolycyclicRecognition.generatorGroupWord_zero_padding line 15

Source documentation

Appending zero-amplitude letters changes no prefix product.

theorem generatorGroupWord_zero_padding
    (hzero : Exp 0 = 1)
    (i₀ : I) (u : List (I × ℝ)) (n j : ℕ) :
    generatorGroupWord X Exp ((u ++ List.replicate n (i₀, 0)).take j) =
      generatorGroupWord X Exp (u.take j) := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.exists_fixed_length_generator_word line 25

Source documentation

A bounded-length generator word can be padded to one prescribed length, preserving its amplitude bound and all previous prefix products.

theorem exists_fixed_length_generator_word
    (hzero : Exp 0 = 1)
    (i₀ : I) (u : List (I × ℝ)) {N : ℕ} (hlen : u.length ≤ N)
    {C : ℝ} (hC : 0 ≤ C) (hamp : ∀ z ∈ u, |z.2| ≤ C) :
    ∃ v : List (I × ℝ), v.length = N ∧ (∀ z ∈ v, |z.2| ≤ C) ∧
      generatorGroupWord X Exp v = generatorGroupWord X Exp u ∧
      ∀ j, generatorGroupWord X Exp (v.take j) = generatorGroupWord X Exp (u.take j) := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.generatorGroupWord_take_succ line 45

Source documentation

Consecutive prefix products differ by precisely the next generator.

theorem generatorGroupWord_take_succ
    (u : List (I × ℝ)) (j : ℕ) (hj : j < u.length) :
    generatorGroupWord X Exp (u.take (j + 1)) =
      generatorGroupWord X Exp (u.take j) * Exp (u[j].2 • X u[j].1) := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.generator_prefix_log_chain line 54

Source documentation

Logarithms of the actual prefixes have the required endpoints and edges.

theorem generator_prefix_log_chain
    (hinj : Function.Injective Exp) (hzero : Exp 0 = 1)
    (u : List (I × ℝ)) {N : ℕ} (hu : u.length = N)
    (k : ℕ → L) (hk : ∀ j, Exp (k j) = generatorGroupWord X Exp (u.take j))
    (v : L) (hend : generatorGroupWord X Exp u = Exp v) :
    k 0 = 0 ∧ k N = v ∧ ∀ j (hj : j < u.length),
      Exp (k (j + 1)) = Exp (k j) * Exp (u[j].2 • X u[j].1) := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord