OAI/Combinatorics/EditApproximation/Coarse/CoarseWorkEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual coarse first-request factor times the width budget remains almost linear. This bound does not assume any seed-correctness event.

  1. theorem OAI.EditApproximation.computed_coarse_widthWork_near_linear line 13