CartanActualConjugation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual Cartan conjugation and shifted boxes

The full Lie action integrates to the nilpotent group. A faithful compatible representation identifies this automorphism with ambient conjugation. The resulting box estimate retains the polynomial residual factor and the exact canonical-height translation.

def OAI.PolycyclicRecognition.CartanWordModel.adjointGroupAutomorphism line 31
Source documentation
Integration of the complete adjoint action, including its residual part.
```
def adjointGroupAutomorphism (h : H) : N ≃* N :=
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.adjointGroupAutomorphism_eq_conjugation line 43

Source documentation

Compatibility of exponentials in a faithful representation identifies the constructed automorphism with actual ambient conjugation.

theorem adjointGroupAutomorphism_eq_conjugation
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (ι : N →* G) (d : H → G)
    (hN : ∀ x : cartanRootIdeal H, ρ (ι (Exp (eN x))) = algebraExpUnit (j x))
    (hd : ∀ h, ρ (d h) = algebraExpUnit (j h)) (h : H) (g : N) :
    ι (M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g) =
      d h * ι g * (d h)⁻¹ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit

theorem OAI.PolycyclicRecognition.CartanWordModel.adjointGroupAutomorphism_factor line 69

Source documentation

Canonical height determines the scalar factor of the actual action.

theorem adjointGroupAutomorphism_factor (h : H) (w : W) (r : ℝ)
    (hh : eW (heightProjection T.character (h : L)) = r • w) (g : N) :
    M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g =
      M.groupWeightDilation T eW eN Exp hExp hbij dynkin w r
        (M.residualGroupAutomorphism T eN Exp hExp hbij dynkin h g) := by
…

Mentions: OAI.PolycyclicRecognition.heightProjection

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_adjoint_groupBox_bound line 95

Source documentation

The actual adjoint action translates the template by canonical height, with a polynomial loss in the Cartan logarithm only.

theorem exists_adjoint_groupBox_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ (h : H) (w : W),
      eW (heightProjection T.character (h : L)) = r • w →
      ∀ (R : ℝ) (g : N), g ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R →
      M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g ∈
        M.groupBox T hunimod eW (Exp ∘ eN) ((fun x => x + w) '' E) β r
          (A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p * R) := by
…

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