OAI/Combinatorics/EditApproximation/Geometry/EarlierInputBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit wide-history cover fits the polynomial earlier-input budget used in the dependency-path count.

  1. def OAI.EditApproximation.localEarlierBudget line 11
  2. theorem OAI.EditApproximation.queryEarlierInputCover_le_budget line 15
  3. theorem OAI.EditApproximation.localEarlierBudget_poly line 31