OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSectionProbeBox.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ideal_probe_box line 26

   Source documentation

   In the adapted maximal basis an intrinsic ideal box is contained in the ambient word box with exactly the same radius and exponents.

   theorem exists_ideal_probe_box
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (E : Set W) (hs : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport E i)
       (hzero : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
         (M.supportIn T hunimod eW).weightSupport E i = 0)
       (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI
         ((M.supportIn T hunimod eW).weightSupport E) β) :
       ∃ γ : M.Bases,
         IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList bN)
           (M.boxCost T hunimod eW E) γ.val ∧
   …

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

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_section_probe_box line 56

   Source documentation

   Completing a maximal ideal basis by pure quotient words places every unit ideal-section probe in one fixed-radius full word box. The radius is uniform in the scale, by the actual finite Dynkin product formula.

   theorem exists_section_probe_box
       (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
       (ExpN : GroupLieAlgebra (𝓘(ℝ, EN)) N → N) (hExpN : IsGroupExponential ExpN)
       (dynkinN : NilpotentDynkinExpansionInput EN N)
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (E : Set W) (hs : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport E i)
       (hzero : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
         (M.supportIn T hunimod eW).weightSupport E i = 0)
       (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI
         ((M.supportIn T hunimod eW).weightSupport E) β) :
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput