ModularFilters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nested filters and enumeration of parent residue classes

The congruence and finite-loop facts used by both trials. No coprimality of the low modulus and the additional prime is required.

theorem OAI.LowSpaceSubsetSum.nested_second_child_filter line 16

Source documentation

A passing parent and first child force the second child's low filter.

theorem nested_second_child_filter {p p0 x1 x2 w rho : ℤ}
    (hdiv : p ∣ p0) (hparent : x1 + x2 ≡ w [ZMOD p0])
    (hchild : x1 ≡ rho [ZMOD p]) : x2 ≡ w - rho [ZMOD p] := by
…

theorem OAI.LowSpaceSubsetSum.lift_low_residue line 24
Source documentation
Every lifted class has the prescribed low residue.
```
theorem lift_low_residue {p rho z : ℕ} (hrho : rho < p) :
    (rho + p * z) % p = rho := by
…
```
theorem OAI.LowSpaceSubsetSum.lift_lt_product line 29
Source documentation
The program's lift lies within the product modulus.
```
theorem lift_lt_product {p q rho z : ℕ} (hrho : rho < p) (hz : z < q) :
    rho + p * z < p * q := by
…
```
theorem OAI.LowSpaceSubsetSum.lift_residue_exists_unique line 37
Source documentation
All product-modulus residues with a given low base occur exactly once in the loop over z < q, including when q and p have a common factor.
```
theorem lift_residue_exists_unique {p q rho r : ℕ}
    (hp : 0 < p) (hr : r < p * q) (hbase : r % p = rho) :
    ∃! z : ℕ, z < q ∧ r = rho + p * z := by
…
```

theorem OAI.LowSpaceSubsetSum.complementary_residue_injective line 50

Source documentation

Complementing the target gives a bijection of the product residue ring.

theorem complementary_residue_injective {P t : ℤ} {x y : ℤ}
    (hx : 0 ≤ x ∧ x < P) (hy : 0 ≤ y ∧ y < P)
    (h : (t - x) % P = (t - y) % P) : x = y := by
…