CartanFactorHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Canonical height of the constructed Cartan factors

The nilpotent root factor has zero height. The Cartan logarithm records the height of every lifted prefix exactly, not just up to bounded error.

theorem OAI.PolycyclicRecognition.CartanFactorModel.inclusionN_height_eq_one line 30
Source documentation
The root ideal lies in the canonical height kernel, hence so does its entire integrated group.
```
theorem inclusionN_height_eq_one
    (hbij : Function.Bijective F.ExpN) (n : F.N.carrier) :
    π (F.inclusionN n) = 1 := by
…
```
theorem OAI.PolycyclicRecognition.CartanFactorModel.inclusionD_height line 44
Source documentation
Cartan logarithmic coordinates recover the actual ambient height.
```
theorem inclusionD_height
    (hbij : Function.Bijective F.ExpD) (d : F.D.carrier) :
    (π (F.inclusionD d)).toAdd = q (heightProjection T.character
      (cartanLog H F.D.equiv F.ExpD hbij d : GroupLieAlgebra (𝓘(ℝ, EG)) G)) := by
…
```
Mentions: OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanLog

theorem OAI.PolycyclicRecognition.CartanFactorModel.lifted_prefix_height line 54

Source documentation

A lifted prefix has precisely the same height as its Cartan coordinate.

theorem lifted_prefix_height
    (hbijN : Function.Bijective F.ExpN) (hbijD : Function.Bijective F.ExpD)
    (u : ℕ → G) (v : ℕ → F.N.carrier) (w : ℕ → F.D.carrier) (j : ℕ)
    (hlift : 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) :
    q (heightProjection T.character
      (cartanLog H F.D.equiv F.ExpD hbijD (wordPrefix w j) :
        GroupLieAlgebra (𝓘(ℝ, EG)) G)) = (π (wordPrefix u j)).toAdd := by
…

Mentions: OAI.PolycyclicRecognition.wordPrefix, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanLog