OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingRootHolonomy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous holonomy for the full Gaussian root induction

One common null set controls every lexicographic elimination step. At each step the remaining subgroup is normal and the selected root leaf is constant along its cosets, with the exact root displacement retained.

  1. def OAI.DukePrimeDegree.InitialRootStep line 19
  2. def OAI.DukePrimeDegree.InitialRootStep.processed line 27
  3. def OAI.DukePrimeDegree.InitialRootStep.root line 28
  4. def OAI.DukePrimeDegree.InitialRootStep.remaining line 29
  5. lemma OAI.DukePrimeDegree.InitialRootStep.initial line 31
  6. lemma OAI.DukePrimeDegree.InitialRootStep.mem_remaining line 32
  7. lemma OAI.DukePrimeDegree.InitialRootStep.least line 33
  8. lemma OAI.DukePrimeDegree.InitialRootStep.positive line 34
  9. lemma OAI.DukePrimeDegree.InitialRootStep.distinct line 36
  10. lemma OAI.DukePrimeDegree.InitialRootStep.remaining_positive line 37
  11. lemma OAI.DukePrimeDegree.InitialRootStep.remaining_closed line 39
  12. theorem OAI.DukePrimeDegree.InitialRootStep.next_normal line 43
  13. theorem OAI.DukePrimeDegree.InitialRootStep.exists_nullset_holonomy line 51
  14. theorem OAI.DukePrimeDegree.exists_nullset_all_initial_root_holonomy line 70