CartanGroupConjugation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Group-box bounds for Cartan actions

The finite Dynkin identity integrates the residual Lie automorphism. Its polynomial box bound and exact weight dilation yield a shifted-box bound.

def OAI.PolycyclicRecognition.CartanWordModel.residualGroupAutomorphism line 29
Source documentation
The actual group automorphism induced by the Cartan residual derivation.
```
def residualGroupAutomorphism (h : H) : N ≃* N :=
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_residual_groupBox_bound line 39

Source documentation

Residual group actions have a polynomial coordinate bound uniform over all templates, maximizing bases and scales.

theorem exists_residual_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) (R : ℝ),
      M.residualGroupAutomorphism T eN Exp hExp hbij dynkin h ''
        M.groupBox T hunimod eW (Exp ∘ eN) E β r R ⊆
        M.groupBox T hunimod eW (Exp ∘ eN) E β r
          (A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p * R) := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_shifted_groupBox_bound line 62

Source documentation

Adding the exact scalar action shifts the template, while the residual action costs only a polynomial factor in the Cartan parameter.

theorem exists_shifted_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) (R : ℝ) (g : N),
      g ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R →
      M.groupWeightDilation T eW eN Exp hExp hbij dynkin w r
        (M.residualGroupAutomorphism 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