PPTSeedNormality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed seed introduces no nonnormal prime factors in the rotated-fiber branch of Ford's construction. For a fixed prime, the interval part of normality is eventually vacuous and the small-factor bound follows from B(S) → ∞. This is the elementary seed step in exclusion (vi), p. 27.

lemma OAI.TotientAsymptotic.ppt_normal_prime_of_small_shift line 19
lemma OAI.TotientAsymptotic.ppt_fixed_prime_eventually_normal line 31
theorem OAI.TotientAsymptotic.ppt_seed_prime_factors_eventually_normal line 40
Source documentation
All prime divisors of one fixed positive seed preimage are eventually normal for the same parameter.
```
theorem ppt_seed_prime_factors_eventually_normal {c : ℕ} (hc : 0 < c) :
    ∀ᶠ S : ℝ in atTop, ∀ p : ℕ, p.Prime → p ∣ c → IsNormalPrime S p := by
…
```
Mentions: OAI.TotientAsymptotic.IsNormalPrime
theorem OAI.TotientAsymptotic.ppt_seed_products_eventually_normal line 51
Source documentation
Multiplying an already normal candidate by the fixed seed preserves normality of every prime divisor, uniformly in the candidate.
```
theorem ppt_seed_products_eventually_normal {c : ℕ} (hc : 0 < c) :
    ∀ᶠ S : ℝ in atTop, ∀ n : ℕ,
      (∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime S p) →
      ∀ p : ℕ, p.Prime → p ∣ c*n → IsNormalPrime S p := by
…
```
Mentions: OAI.TotientAsymptotic.IsNormalPrime