OAI/Combinatorics/EditApproximation/Binary/BinaryCachedContinuation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cache insertion compresses the actual continuation result by executed Boolean multiplication and division. Its cost is part of the return counter; no rational normalization operation is assigned unit cost.

  1. theorem OAI.EditApproximation.BinaryFraction.finishCachedWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.finishCachedWithWork_bounds line 23
  3. def OAI.EditApproximation.BinaryFraction.cachedPhysicalContinuationWithWork line 35
  4. theorem OAI.EditApproximation.BinaryFraction.cachedPhysicalContinuationWithWork_value line 46