CartanChartSlack.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior slack for actual scaled Cartan chart positions

theorem OAI.PolycyclicRecognition.CartanWordModel.chart_suffix_conjugation_tendstoUniformly line 29

Source documentation

The conjugation parameter for a fixed normal-factor move tends to zero uniformly over the bounded interior chart samples, even after the enlarged deterministic suffix. The chart action and both word expansions are derived from the actual Lie algebra.

theorem chart_suffix_conjugation_tendstoUniformly
    [Nonempty (Fin (finrank ℝ (cartanRootIdeal H)))]
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (β γ : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val)
    {δ c lo hi : ℝ} (hδ : 0 < δ) (hc : 0 ≤ c) (hhi : 0 ≤ hi)
    (ht : 0 ≤ 1 - c * δ)
    (hcost : ∀ w : M.wordList,
      lo ≤ M.boxCost T hunimod eW E w ∧ M.boxCost T hunimod eW E w ≤ hi)
    (hgap : (M.bound : ℝ) * hi < c * lo)
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates