RootSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Separation of square-root populations at split primes

At the end of §3, the squarefree kernels give equations for the two populations. A square root of their ratio rescales the second population. The prime-sum exclusion then forces the rescaled residue supports apart.

theorem OAI.Ostmann.disjoint_scaled_root_images line 18

Source documentation

The algebraic part of the split-prime support separation.

theorem disjoint_scaled_root_images {p : ℕ} [Fact p.Prime]
    (A₀ B₀ : Finset ℕ) (r s : ℕ → ℕ) (m u v h c : ZMod p)
    (hm : m ≠ 0) (hscale : u * c ^ 2 = v)
    (hA : ∀ a ∈ A₀, u * (r a : ZMod p) ^ 2 = m * (a : ZMod p) - h)
    (hB : ∀ b ∈ B₀, v * (s b : ZMod p) ^ 2 = m * (-(b : ZMod p)) - h)
    (havoid : ∀ a ∈ A₀, ∀ b ∈ B₀, ¬ p ∣ a + b) :
    Disjoint (A₀.image (fun a => (r a : ZMod p)))
      (B₀.image (fun b => c * (s b : ZMod p))) := by
…

theorem OAI.Ostmann.EventuallyPrimeSumset.disjoint_scaled_root_images line 41

Source documentation

Eventual prime sums supply the required exclusion at every smaller prime, with the same threshold for all root populations.

theorem EventuallyPrimeSumset.disjoint_scaled_root_images {A B : Set ℕ}
    (hprime : EventuallyPrimeSumset A B) :
    ∃ N, ∀ (p : ℕ) (_hp : p.Prime) (A₀ B₀ : Finset ℕ) (r s : ℕ → ℕ)
      (m u v h c : ZMod p),
      m ≠ 0 → u * c ^ 2 = v →
      (∀ a ∈ A₀, a ∈ A) → (∀ b ∈ B₀, b ∈ B) →
      (∀ a ∈ A₀, ∀ b ∈ B₀, N ≤ a + b ∧ p < a + b) →
      (∀ a ∈ A₀, u * (r a : ZMod p) ^ 2 = m * (a : ZMod p) - h) →
      (∀ b ∈ B₀, v * (s b : ZMod p) ^ 2 = m * (-(b : ZMod p)) - h) →
      Disjoint (A₀.image (fun a => (r a : ZMod p)))
        (B₀.image (fun b => c * (s b : ZMod p))) := by
…

Mentions: OAI.Ostmann.EventuallyPrimeSumset