OAI/Combinatorics/UniformKServer/LevelAnchorContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cross-time witnesses for a literal fixed-alphabet key. Tier labels cannot be reassigned on consecutive supported maps; only retained heavy labels move.

  1. theorem OAI.UniformKServer.LevelMap.Data.key_tier_witness line 19
  2. theorem OAI.UniformKServer.LevelMap.Data.supported_transition line 40
  3. theorem OAI.UniformKServer.LevelMap.Data.supported_distance line 55