CartanNegativeChainAsymptotics.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Negative source chains give equality in the actual ray quotient

This combines the actual metric factorization, the compact-lift property, and the proved ray contraction. Only the sublinear height comparison of the coarse map remains a geometric premise.

theorem OAI.PolycyclicRecognition.CartanWordModel.negative_chain_quotient_difference_tendsto_one line 42

Source documentation

Polynomially many unit steps in a negative halfspace have asymptotic images in the actual ray quotient under a coarse map with sublinear height error. No contraction or metric-factor estimate is assumed here.

theorem negative_chain_quotient_difference_tendsto_one
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ₀ : M.Bases)
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
      (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
      (cartanLog H F.D.equiv F.ExpD
        (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) d))
    (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
      ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
        dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
    {Kheight : ℝ} (hKheight : 0 ≤ Kheight)
    (hLip : ∀ x y, ‖(height x).toAdd - (height y).toAdd‖ ≤ Kheight * dist x y)
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog