OAI/NumberTheory/Ostmann/Construction/SelectedFinalPermutation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Final parity permutations fix every top slot

Only the explicitly selected bulk slots are permuted among paths of equal parity. The remaining word slots, in particular the top labels, stay fixed.

  1. def OAI.Ostmann.selectedParityH line 13
  2. def OAI.Ostmann.selectedParityCoordinates line 25
  3. def OAI.Ostmann.selectedFinalPerm line 31
  4. theorem OAI.Ostmann.selectedFinalPerm_bulk line 37
  5. theorem OAI.Ostmann.selectedFinalPerm_other line 50
  6. theorem OAI.Ostmann.selectedParityH_origin line 58
  7. theorem OAI.Ostmann.selectedFinalPerm_fixed_of_origin line 64
  8. theorem OAI.Ostmann.selectedFinalPerm_injective line 76
  9. theorem OAI.Ostmann.selectedFinalPerm_origin line 87
  10. theorem OAI.Ostmann.selectedFinalPerm_product_prior line 101