OAI/NumberTheory/Ostmann/Construction/ScheduleWordSlots.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Ostmann.copyScheduleVertexFintype line 10
2. theorem OAI.Ostmann.copySchedulePath_injective line 18
3. theorem OAI.Ostmann.surviving_word_is_path line 38
4. abbrev OAI.Ostmann.SurvivingWordSlot line 62
5. def OAI.Ostmann.survivingWordEquiv line 65
6. theorem OAI.Ostmann.surviving_word_card line 83

   Source documentation

   The schedule has exactly 2^n independently sampled copies of each initial word slot. No outside or discarded pivot label contributes to this count.

   theorem surviving_word_card {I : Type*} [Fintype I] (role : I → CopyScheduleRole)
       (n : ℕ) :
       Nat.card (SurvivingWordSlot role n) =
         2 ^ n * Nat.card {i : I // role i = .word} := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingWordSlot