OAI/Analysis/CircleDomains/Selection/FixedPatternJumpRemoval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Remove all new shrinking jumps from a fixed finite old-jump pattern. All blocks use one common subsequence, so the total budget is retained.

  1. theorem OAI.CircleDomainRigidity.exists_old_chain_of_shrinking_blocks line 21