EventualFragmentBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Limiting fragment budgets only require each fixed finite collection to exist eventually; no artificial restrictions are imposed on early stages.

theorem OAI.CircleDomainRigidity.fragment_limit_budget_of_eventually line 15