OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalScalarCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bit costs for the three physical source guards. Bounds use only the words in the request, not the size of the ambient source set.

  1. theorem OAI.EditApproximation.queryScalePresentWithWork_cost line 10
  2. theorem OAI.EditApproximation.queryRangeValidWithWork_cost line 34
  3. theorem OAI.EditApproximation.queryCellValidWithWork_cost line 44