OAI/Analysis/CircleDomains/Selection/ProgressiveJumpSystems.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Install all finite jump levels while retaining a common separation bound. Each stage is obtained from the proved jump-removal theorem, and every finite chain in the union is reduced to one finite stage.

  1. theorem OAI.CircleDomainRigidity.exists_progressive_barrier_jump_system line 23