OAI/Combinatorics/LowSpaceSubsetSum/Streams/WeightEncoding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Exact fixed-width keys for weights and top masks

Weights use a sign bit followed by 2u magnitude bits. Representation keys append the entire indexed mask, using one bit per input index. Every key has the same width, even on an outcome where its numerical value is not used. The input magnitude bounds guarantee injectivity for all actual weights.

  1. def OAI.LowSpaceSubsetSum.WeightEncoding.natBits line 19
  2. theorem OAI.LowSpaceSubsetSum.WeightEncoding.natBits_length line 22
  3. theorem OAI.LowSpaceSubsetSum.WeightEncoding.natBits_injective line 25
  4. def OAI.LowSpaceSubsetSum.WeightEncoding.signedBits line 38
  5. theorem OAI.LowSpaceSubsetSum.WeightEncoding.signedBits_length line 41
  6. theorem OAI.LowSpaceSubsetSum.WeightEncoding.signedBits_injective line 44
  7. def OAI.LowSpaceSubsetSum.WeightEncoding.maskBits line 62
  8. theorem OAI.LowSpaceSubsetSum.WeightEncoding.maskBits_length line 65
  9. theorem OAI.LowSpaceSubsetSum.WeightEncoding.maskBits_injective line 68
  10. def OAI.LowSpaceSubsetSum.WeightEncoding.weightWidth line 76
  11. def OAI.LowSpaceSubsetSum.WeightEncoding.entryWidth line 77
  12. def OAI.LowSpaceSubsetSum.WeightEncoding.weightKey line 79
  13. def OAI.LowSpaceSubsetSum.WeightEncoding.entryKey line 82
  14. theorem OAI.LowSpaceSubsetSum.WeightEncoding.weightKey_length line 85
  15. theorem OAI.LowSpaceSubsetSum.WeightEncoding.entryKey_length line 88
  16. def OAI.LowSpaceSubsetSum.WeightEncoding.BoundedWeight line 91
  17. theorem OAI.LowSpaceSubsetSum.WeightEncoding.boundedWeight_bits line 94
  18. theorem OAI.LowSpaceSubsetSum.WeightEncoding.weightKey_injective line 99
  19. theorem OAI.LowSpaceSubsetSum.WeightEncoding.weightKey_eq_iff line 104
  20. theorem OAI.LowSpaceSubsetSum.WeightEncoding.entryKey_injective line 109
  21. theorem OAI.LowSpaceSubsetSum.WeightEncoding.signed_weight_bounded line 120
  22. theorem OAI.LowSpaceSubsetSum.WeightEncoding.signed_target_bounded line 124
  23. theorem OAI.LowSpaceSubsetSum.WeightEncoding.raw_signed_weight_bounded line 128
  24. theorem OAI.LowSpaceSubsetSum.WeightEncoding.widths_le line 134

    Source documentation

    The exact number of encoded bits is linear in the original input scale.

    theorem widths_le {n : ℕ} (I : Instance n) :
    weightWidth I ≤ 2 * inputScale I + 1 ∧ entryWidth I ≤ 3 * inputScale I + 1 := by
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.WeightEncoding.weightWidth, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.WeightEncoding.entryWidth

  25. theorem OAI.LowSpaceSubsetSum.WeightEncoding.weight_lookup_steps line 139
  26. theorem OAI.LowSpaceSubsetSum.WeightEncoding.entry_lookup_steps line 144
  27. theorem OAI.LowSpaceSubsetSum.WeightEncoding.entry_insert_nodes line 152