OAI/NumberTheory/Ostmann/Construction/ScheduledFinalPairReindex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledFinalRelativePerm line 11
2. theorem OAI.Ostmann.scheduledFinalRelativePerm_matching line 16
3. theorem OAI.Ostmann.scheduledFinalRelativePerm_origin line 22
4. theorem OAI.Ostmann.scheduled_final_relative_interaction line 33

   Source documentation

   The witness is the actual shorter anchor and a moved bulk prime slot.

   theorem scheduled_final_relative_interaction {I : Type*} (role : I → CopyScheduleRole)
       (pivot : ℕ → I) (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
       (anchor : Fin (n + 1) → I) (ha : ∀ j, role (anchor j) = .anchor j)
       (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ (h : CopyScheduleH role (n + 1)) (j : Fin (n + 1)) (sign : Bool),
         let a := scheduledRetainedEmbedding role (n + 1)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledRetainedEmbedding

5. theorem OAI.Ostmann.scheduled_final_relative_nonprincipal line 56
6. theorem OAI.Ostmann.scheduled_final_pair_reindex line 79