OAI/Combinatorics/EditApproximation/Queries/QueryCellCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the actual cell scan at an accepted query scale. The scale-window test controls its count; the binary arithmetic controls its coordinate widths independently of the numeric target length.

  1. theorem OAI.EditApproximation.BinaryFraction.queryCellCoordinates_count line 12
  2. theorem OAI.EditApproximation.BinaryFraction.queryScalesWithWork_window line 34
  3. def OAI.EditApproximation.BinaryFraction.queryCellScanBitBudget line 43
  4. theorem OAI.EditApproximation.BinaryFraction.queryCellScan_bounds line 47