OAI/Combinatorics/UniformKServer/TierLabeledEdits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The one-edit noncoverage ledger uses the actual recycled labels. Old records preserve their labels; the proof does not assume eternal identifiers.

  1. theorem OAI.UniformKServer.TierLabeledKeys.old_map line 20
  2. theorem OAI.UniformKServer.TierLabeledKeys.uncovered_map line 40
  3. theorem OAI.UniformKServer.TierLabeledKeys.changed_map line 43
  4. theorem OAI.UniformKServer.TierLabeledKeys.stationary line 48
  5. theorem OAI.UniformKServer.TierLabeledKeys.mover line 67