CartanBoxDilation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact template shifts for actual Cartan boxes

The scalar action on generalized weight spaces is a genuine Lie automorphism. It takes each scaled word basis to the basis for the translated template. The finite Dynkin identity then integrates it to the needed group automorphism.

theorem OAI.PolycyclicRecognition.CartanWordModel.idealWeightDilation_word line 31
Source documentation
Every actual bracket word is scaled by the exponential of its total weight, even when its total weight is zero.
```
theorem idealWeightDilation_word (h : H) (w : FreeMagma (Fin M.letterCount)) :
    cartanIdealWeightDilation T H h (evalBracketWord M.letter w) =
      Real.exp (bracketWordExponent (fun i => M.weight i h) w) • evalBracketWord M.letter w := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.boxCost_translate line 47

Source documentation

Translation adds the total word weight to its box exponent.

theorem boxCost_translate {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (w : W) (z : M.wordList) :
    M.boxCost T hunimod eW ((fun x => x + w) '' E) z =
      M.boxCost T hunimod eW E z +
        bracketWordExponent (fun i => M.weight i (cartanHeightSection T H (eW.symm w))) z := by
…

Mentions: OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.cartanHeightSection

theorem OAI.PolycyclicRecognition.CartanWordModel.columnBasisWeight_boxCost_translate line 61

Source documentation

All word bases keep their determinant exponent under template translation.

theorem columnBasisWeight_boxCost_translate {E : Set W}
    (hE : IsCompact E) (hne : E.Nonempty) (w : W) (β : M.Bases) :
    columnBasisWeight (M.boxCost T hunimod eW ((fun x => x + w) '' E)) β.val =
      columnBasisWeight (M.boxCost T hunimod eW E) β.val := by
…

Mentions: OAI.PolycyclicRecognition.columnBasisWeight

theorem OAI.PolycyclicRecognition.CartanWordModel.maximizing_box_basis_translate line 69

Source documentation

Thus a maximizing basis remains maximizing after translation.

theorem maximizing_box_basis_translate
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (w : W) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val) :
    IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW ((fun x => x + w) '' E)) β.val := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.idealWeightDilation_boxBasis line 85

Source documentation

The scaled basis itself shifts exactly, with no loss in its radius.

theorem idealWeightDilation_boxBasis {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (w : W) (β : M.Bases) (r : ℝ) :
    (M.boxBasis T hunimod eW E β r).map
      (cartanIdealWeightDilation T H (r • cartanHeightSection T H (eW.symm w))).toLinearEquiv =
        M.boxBasis T hunimod eW ((fun x => x + w) '' E) β r := by
…

Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.cartanHeightSection

def OAI.PolycyclicRecognition.CartanWordModel.groupWeightDilation line 124
Source documentation
Exact weight dilation in the actual nilpotent group.
```
def groupWeightDilation (w : W) (r : ℝ) : N ≃* N :=
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.groupWeightDilation_box line 129

Source documentation

The exponential image of a coordinate cube shifts with its basis.

theorem groupWeightDilation_box {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (w : W) (β : M.Bases) (r R : ℝ) :
    M.groupWeightDilation T eW eN Exp hExp hbij dynkin w r ''
      M.groupBox T hunimod eW (Exp ∘ eN) E β r R =
        M.groupBox T hunimod eW (Exp ∘ eN) ((fun x => x + w) '' E) β r R := by
…