OAI/Combinatorics/UniformKServer/LevelSerial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The source edit order: first heavy, then tiers in order. Each tier ledger retains its higher-priority shadow and its old lower-priority suffix.

  1. def OAI.UniformKServer.LevelMap.Data.serialEdit line 20
  2. def OAI.UniformKServer.LevelMap.Data.tierPotential line 25
  3. theorem OAI.UniformKServer.LevelMap.Data.serial_ledger line 28
  4. theorem OAI.UniformKServer.LevelMap.Data.serial_stationary line 62
  5. theorem OAI.UniformKServer.LevelMap.Data.serial_mover line 73
  6. theorem OAI.UniformKServer.LevelMap.Data.actual_shadow line 84
  7. theorem OAI.UniformKServer.LevelMap.Data.key_edit_bound line 90