Magnitudes.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Input bit lengths and exact signed-weight bounds

The bit parameter is the manuscript's ceiling logarithm, computed on the original nonnegative input. These bounds include raw occurrences that repeat indices, so hashing before a local-overlap test is covered.

def OAI.LowSpaceSubsetSum.inputMaximum line 19
def OAI.LowSpaceSubsetSum.inputBits line 22
def OAI.LowSpaceSubsetSum.inputScale line 25
theorem OAI.LowSpaceSubsetSum.inputBits_pos line 27
theorem OAI.LowSpaceSubsetSum.inputMaximum_lt_two_pow_bits line 30
theorem OAI.LowSpaceSubsetSum.value_lt_two_pow_bits line 37
theorem OAI.LowSpaceSubsetSum.target_lt_two_pow_bits line 43
theorem OAI.LowSpaceSubsetSum.weight_natAbs_le line 47
theorem OAI.LowSpaceSubsetSum.flip_natAbs line 58
def OAI.LowSpaceSubsetSum.occurrenceWeight line 63
Source documentation
The list retains repeated index occurrences in a raw tuple.
```
def occurrenceWeight {ι : Type*} (a : ι → ℤ) (xs : List ι) : ℤ :=
…
```
theorem OAI.LowSpaceSubsetSum.occurrenceWeight_natAbs_le line 66
theorem OAI.LowSpaceSubsetSum.signed_weight_natAbs_le line 77
theorem OAI.LowSpaceSubsetSum.signed_target_natAbs_le line 84
theorem OAI.LowSpaceSubsetSum.raw_signed_weight_natAbs_le line 96
theorem OAI.LowSpaceSubsetSum.relevant_magnitude_lt line 106
theorem OAI.LowSpaceSubsetSum.relevant_difference_bits line 123
Source documentation
Every hash difference between valid or raw signed quantities of the stated size meets the concrete prime-hashing bit hypothesis.
```
theorem relevant_difference_bits {n : ℕ} (I : Instance n) {x y : ℤ}
    (hx : x.natAbs ≤ (2 * n + 1) * 2 ^ inputBits I)
    (hy : y.natAbs ≤ (2 * n + 1) * 2 ^ inputBits I) :
    (x - y).natAbs < 2 ^ (2 * inputScale I) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.inputBits, OAI.LowSpaceSubsetSum.inputScale