OAI/GroupTheory/PolycyclicRecognition/Algebra/ConeIdealBasisExchange.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bracketWordExponent_eq_zero_of_pure line 13
2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdeal_leaf_mem_of_ne_zero line 29
3. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdeal_width_le_of_coordinate_ne_zero line 41

   Source documentation

   Exchange applies to every original mixed word, even though the ideal box is built using the nested finite alphabet.

   theorem coneIdeal_width_le_of_coordinate_ne_zero
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (s : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C b₀ s β) (w : M.coneMixedWords C)
       (j : Fin (finrank ℝ (M.coneWordIdeal C)))
       (hj : (WordBasisSelections.basis (M.coneMixedVector C) (M.coneIdealWordList C) β).repr
         (M.coneMixedVector C w) j ≠ 0) :
       bracketWordExponent s w.val.val ≤ M.coneIdealWordCost C s (β.val j) := by
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.bracketWordExponent