PPTLargePart.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The leading shift in the PPT construction satisfies the large-prime-part condition of Ford's comparison lemma directly from normality. The sharp bound Ω(p-1) ≤ 3 B(z) leaves a strict margin at the published cutoff Y₁ ≤ z^(1/(10 B(z))).

lemma OAI.TotientAsymptotic.ppt_prime_shift_log_strict line 18
lemma OAI.TotientAsymptotic.ppt_cutoff_log_cost line 39

theorem OAI.TotientAsymptotic.ppt_comparison_large_part line 51

Source documentation

The literal cutoff from Ford's comparison parameters suffices for the large-prime-part requirement on a leading candidate prime.

theorem ppt_comparison_large_part : ∀ᶠ z : ℝ in atTop,
    ∀ p : ℕ, ∀ Y : ℝ, p.Prime → z^(9/10 : ℝ) ≤ p →
      1 ≤ Y → Y ≤ z^(1/(10*B z)) →
      ((p-1).primeFactorsList.length : ℝ) ≤ 3*B z →
      Real.sqrt z < (partAbove (p-1) Y : ℝ) := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.partAbove

theorem OAI.TotientAsymptotic.ppt_normal_comparison_large_part line 67
Source documentation
Normality supplies the sharp total-factor bound uniformly below z. No separate smooth-divisor exclusion is needed for this conclusion.
```
theorem ppt_normal_comparison_large_part : ∀ᶠ z : ℝ in atTop,
    ∀ (p : ℕ) (S Y : ℝ), 1 < S → 0 ≤ B S → S ≤ z →
      IsNormalPrime S p → z^(9/10 : ℝ) ≤ p → (p-1 : ℕ) ≤ z →
      1 ≤ Y → Y ≤ z^(1/(10*B z)) →
      Real.sqrt z < (partAbove (p-1) Y : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.partAbove