OAI/NumberTheory/Ostmann/Construction/SurvivingSlotCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sharp slot counts after erasing each pivot

Only surviving positions matter. Each position is either doubled or retained, so the growth factor is two even though the ambient label type grows by three.

  1. theorem OAI.Ostmann.copyScheduleAtoms_succ_card line 15
  2. theorem OAI.Ostmann.copyScheduleAtoms_partition_card line 22
  3. theorem OAI.Ostmann.copyScheduleAtoms_card_sharp line 29
  4. theorem OAI.Ostmann.copyScheduleH_card_sharp line 41
  5. theorem OAI.Ostmann.scheduledNonbulkH_card_sharp line 48