OAI/Combinatorics/EditApproximation/Refinement/ComputedSourceReadBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-degree source-read bounds for a refinement entry. These hold on all stored initial values, including outcomes outside accuracy events.

  1. theorem OAI.EditApproximation.computed_source_key_budget line 12