CartanBridgeGeometry.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual thickened lifts across the bridge between probe sheets

The first factor comes from the second sheet's controlled path. The short ambient bridge is factored by its metric length. Their semidirect product has one ideal-coordinate restriction and one Cartan-coordinate restriction for its entire fixed right cell.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_thickened_bridge_lifts line 46

Source documentation

A single choice of bridge lift controls every point of the compact right cell. The ideal bound is subexponential once δ is sufficiently small; the Cartan bound is subexponential for the same lift.

theorem exists_sequence_thickened_bridge_lifts
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ₀ : M.Bases) {cell : Set (F.N.carrier × F.D.carrier)} (hcell : IsCompact cell)
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
      hbijN dynkinN
      (cartanLog H F.D.equiv F.ExpD
        hbijD 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|)
    {Kπ : ℝ} (hKπ : 0 ≤ Kπ)
    (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ Kπ * dist x y)
…

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