CartanWordLifts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Lifting actual ambient word paths to the Cartan factors

One compact set of factor increments lifts every word over a compact ambient increment set. The lift reproduces every prefix exactly, so height control can be applied to the actual ambient path.

theorem OAI.PolycyclicRecognition.map_wordPrefix line 17

theorem OAI.PolycyclicRecognition.exists_lifted_word_prefixes line 26

Source documentation

A fixed set of possible lifts supplies compatible lifts of every finite word, with all prefix equalities retained.

theorem exists_lifted_word_prefixes {A B : Type*} [Monoid A] [Monoid B]
    (f : A →* B) (C : Set A) (K : Set B) (hK : K ⊆ f '' C)
    (u : ℕ → B) (m : ℕ) (hu : ∀ i < m, u i ∈ K) :
    ∃ v : ℕ → A, (∀ i < m, v i ∈ C) ∧
      ∀ j ≤ m, f (wordPrefix v j) = wordPrefix u j := by
…

Mentions: OAI.PolycyclicRecognition.wordPrefix

theorem OAI.PolycyclicRecognition.exists_compact_cartan_word_lifts line 56

Source documentation

The actual ambient compact increments lift into one compact factor set, uniformly over word length. All intermediate positions are reproduced.

theorem exists_compact_cartan_word_lifts {K : Set G} (hK : IsCompact K) :
    ∃ C : Set (F.N.carrier × F.D.carrier), IsCompact C ∧
      ∀ (u : ℕ → G) (m : ℕ), (∀ i < m, u i ∈ K) →
      ∃ (v : ℕ → F.N.carrier) (w : ℕ → F.D.carrier),
        (∀ i < m, (v i, w i) ∈ C) ∧
        ∀ j ≤ m, F.inclusionN
            (wordPrefix (fun i => (⟨v i, w i⟩ : F.N.carrier ⋊[F.action] F.D.carrier)) j).left *
          F.inclusionD (wordPrefix w j) = wordPrefix u j := by
…

Mentions: OAI.PolycyclicRecognition.wordPrefix