OAI/Combinatorics/EditApproximation/Queries/QuerySourceBuffers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Source words are decoded only by counted buffer lookups, natural floor and remainder routines. The resulting draws are exactly the draws used by the semantic adaptive query, for every stored answer list.

  1. theorem OAI.EditApproximation.queryGroupKeyEqualWithWork_value line 16
  2. theorem OAI.EditApproximation.queryOnlineKeyEqualWithWork_value line 38
  3. theorem OAI.EditApproximation.BinaryFraction.queryGroupDrawReadWithWork_value line 47
  4. theorem OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadWithWork_value line 61