WordInteriorSlack.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior slack from actual finite word coefficients

A larger choice of the manuscript's free interior constant lets the uniform nilpotent operator estimate absorb the enlarged suffix. No coordinate growth estimate is assumed: both estimates follow from the finite word expansions and maximizing-basis exchange.

theorem OAI.PolycyclicRecognition.rescaled_word_conjugation_tendsto_zero line 30

Source documentation

The logarithm of the conjugate tends to zero in every maximizing rescaled basis. This applies to the actual exponential product through the faithful realization, with no new conjugation identity assumed.

theorem rescaled_word_conjugation_tendsto_zero
    [Nonempty (Fin (finrank ℝ L))]
    (X : I → L) {m k₀ c₀ : ℕ}
    (hk : lowerCentralSeries ℝ L L k₀ = ⊥)
    (hnil : lowerCentralSeries ℝ L L (m + 1) = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (s : I → ℝ)
    (β : ℝ → WordBasisSelections X (boundedBracketWords k₀))
    (hβ : ∀ r, IsMaximizingColumnBasis
      (wordListCoordinates X (boundedBracketWords k₀) b₀)
      (fun w => bracketWordExponent s w) (β r).val)
    (Exp : L → G) (hinj : Function.Injective Exp)
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent