OAI/Analysis/CircleDomains/Selection/JumpBlockCountBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The positive toll floor gives one finite code space for every chain under a fixed budget, independent of its original code bound.

  1. theorem OAI.CircleDomainRigidity.exists_uniform_block_pattern_bound line 20
  2. def OAI.CircleDomainRigidity.reboundBlockPattern line 44
  3. def OAI.CircleDomainRigidity.reboundJumpBlock line 49
  4. theorem OAI.CircleDomainRigidity.reboundJumpBlock_valid line 54
  5. theorem OAI.CircleDomainRigidity.reboundJumpBlock_cost line 64