CommonResidueLift.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One integer realizes all coordinates of a common residue configuration.

theorem OAI.TwoPointCorrelations.exists_common_integer_residue line 14

Source documentation

This is a simultaneous lift of the entire configuration. It is used after forming a hybrid, so different witness sites keep the same origin.

theorem exists_common_integer_residue {ι : Type*} [Fintype ι] [DecidableEq ι]
    (p : ι → ℕ) [∀ i, NeZero (p i)]
    (hcop : Pairwise (fun i j => (p i).Coprime (p j)))
    (r : ∀ i, ZMod (p i)) :
    ∃ n : ℤ, ∀ i, (n : ZMod (p i)) = r i := by
…

lemma OAI.TwoPointCorrelations.residue_offset_divisibility line 30

Source documentation

Prime divisibility at any offset is read from that same lifted origin.

lemma residue_offset_divisibility {p : ℕ} (r : ZMod p) (n offset : ℤ)
    (hn : (n : ZMod p) = r) :
    (p : ℤ) ∣ n + offset ↔ r = -(offset : ZMod p) := by
…

lemma OAI.TwoPointCorrelations.residue_product_divisibility line 37

Source documentation

The conjunction of all prime-power coordinate tests is exactly divisibility by their product. No independence across sites is required.

lemma residue_product_divisibility {ι : Type*} [Fintype ι] [DecidableEq ι]
    (p : ι → ℕ) (hcop : Pairwise (fun i j => (p i).Coprime (p j)))
    (r : ∀ i, ZMod (p i)) (n offset : ℤ) (hn : ∀ i, (n : ZMod (p i)) = r i)
    (S : Finset ι) :
    ((∏ i ∈ S, p i : ℕ) : ℤ) ∣ n + offset ↔
      ∀ i ∈ S, r i = -(offset : ZMod (p i)) := by
…