OAI/NumberTheory/Ostmann/Construction/SelectedAnchorBudget.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The selected-bulk normalization includes the top slots exactly once per path
- theorem
OAI.Ostmann.eventual_selected_anchor_nonbulk_costline 11