OAI/Analysis/CircleDomains/Selection/PositiveJumpCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform finite cost and a positive floor bound the number of jumps. This supplies the finite pattern extraction in jump-level removal.

  1. theorem OAI.CircleDomainRigidity.exists_uniform_jump_count_bound line 13