OAI/NumberTheory/Ostmann/Construction/FinalReassignments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.ParityPathSum line 12
2. def OAI.Ostmann.parityPathValue line 14
3. theorem OAI.Ostmann.parityPathValue_injective line 18
4. def OAI.Ostmann.parityPathSumEquiv line 30
5. def OAI.Ostmann.paritySlotPerm line 37
6. theorem OAI.Ostmann.paritySlotPerm_preserves_parity line 44
7. theorem OAI.Ostmann.paritySlotPerm_preserves_position line 52
8. theorem OAI.Ostmann.paritySlotPerm_injective line 55
9. theorem OAI.Ostmann.distinct_reassignments_change_code line 71

   Source documentation

   Distinct members of the constructed reassignment family move some prime to a path with a different anchor code, while retaining its final parity.

   theorem distinct_reassignments_change_code {n m : ℕ}
       (α : Fin (n + 1) → ℤ) (hα : ∀ j, α j = 1 ∨ α j = -1)
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ x : ParityPathSum n × Fin m,
         finiteAnchorCode α (parityPathValue (paritySlotPerm e x).1) ≠
           finiteAnchorCode α (parityPathValue (paritySlotPerm f x).1) := by
   …

   Mentions: OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.ParityPathSum, OAI.Ostmann.finiteAnchorCode, OAI.Ostmann.parityPathValue, OAI.Ostmann.paritySlotPerm