OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationAllocationExecution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Executing the six binomial widths and eight background sizes

The binomial loop uses integer multiplication and exact division with constant state. Its bounded binary-log loop is followed by the fixed two-level integer allocation formulas. No real logarithm is evaluated by this routine.

  1. def OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.bits line 18
  2. theorem OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.bits_value line 23
  3. theorem OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.bits_work line 27
  4. def OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.run line 34
  5. theorem OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.value line 41
  6. theorem OAI.LowSpaceSubsetSum.RepresentationAllocationExecution.work line 46