OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedKernelWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complete prepared refinement kernel has a single arithmetic bound. All generated grids, guards, selected actions and the returned value are charged. The premises below describe only stored input words and numeric parameters; action geometry and output-list bounds are derived.

  1. structure OAI.EditApproximation.BinaryFraction.PreparedKernelInputBounds line 16
  2. def OAI.EditApproximation.BinaryFraction.preparedKernelBitBudget line 64
  3. def OAI.EditApproximation.BinaryFraction.preparedKernelWordBudget line 70
  4. theorem OAI.EditApproximation.BinaryFraction.physicalContinuationBitBudget_mono_counts line 73
  5. theorem OAI.EditApproximation.BinaryFraction.preparedLocalKernelWithWork_bounds line 80