OAI/Combinatorics/LowSpaceSubsetSum/Storage/MixerWeightCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Constructing the shared half-mixer weight arrays

Subset masks are index lists. Their weights are evaluated by actual membership scans, then consumed by a tail accumulator. Sorting retains only the bounded half-family, never the Cartesian stream of sums.

  1. def OAI.LowSpaceSubsetSum.MixerWeightCells.sumIndices line 19
  2. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.sumIndices_value line 28
  3. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.sumIndices_cells line 35
  4. def OAI.LowSpaceSubsetSum.MixerWeightCells.weight line 44
  5. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.weight_value line 48
  6. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.weight_cells line 51
  7. def OAI.LowSpaceSubsetSum.MixerWeightCells.weightsAcc line 58
  8. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.weightsAcc_value line 66
  9. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.weightsAcc_cells line 73
  10. def OAI.LowSpaceSubsetSum.MixerWeightCells.raw line 87
  11. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.raw_value line 93
  12. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.raw_cells line 97
  13. def OAI.LowSpaceSubsetSum.MixerWeightCells.compare line 114
  14. def OAI.LowSpaceSubsetSum.MixerWeightCells.sortedWeights line 116
  15. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.sortedWeights_value line 121
  16. theorem OAI.LowSpaceSubsetSum.MixerWeightCells.sortedWeights_cells line 126