OAI/GroupTheory/PolycyclicRecognition/Analysis/MixedWordBoxModel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The concrete nilpotent box model of a cone ideal

The finite mixed words generate the ideal even as a vector space. Using them as an alphabet allows the existing box calculus to apply directly. Flattening this alphabet retains the original word and its exact width.

  1. def OAI.PolycyclicRecognition.substituteBracketWord line 20
  2. theorem OAI.PolycyclicRecognition.eval_substituteBracketWord line 25
  3. theorem OAI.PolycyclicRecognition.exponent_substituteBracketWord line 38
  4. theorem OAI.PolycyclicRecognition.bracketWordExponent_nonneg line 49
  5. theorem OAI.PolycyclicRecognition.bracketWordExponent_pos_of_mixed line 54
  6. theorem OAI.PolycyclicRecognition.CartanWordModel.coneMixedVector_generates line 72
  7. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordBound line 82
  8. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordBound_zero line 87
  9. abbrev OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordList line 94
  10. abbrev OAI.PolycyclicRecognition.CartanWordModel.ConeIdealBases line 97
  11. instance OAI.PolycyclicRecognition.CartanWordModel.(instance at line 100) line 100
  12. def OAI.PolycyclicRecognition.CartanWordModel.coneOriginalWord line 104
  13. theorem OAI.PolycyclicRecognition.CartanWordModel.coneOriginalWord_mixed line 108
  14. theorem OAI.PolycyclicRecognition.CartanWordModel.coneOriginalWord_eval line 115
  15. theorem OAI.PolycyclicRecognition.CartanWordModel.coneOriginalWord_mem_of_eval_ne_zero line 123
  16. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordCost line 131
  17. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordCost_eq_original line 135
  18. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordCost_pos line 140