PublishedComparison.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The published comparison input for the conditional collision proof.

Kevin Ford, The distribution of totients, Ramanujan J. 2 (1998), 67–151, revised arXiv:1104.3264v2 (14 July 2013), Lemma 5.1, pp. 21–22. The published statement permits k ≥ 1, including a single surviving prime. The author-hosted copy also makes this endpoint explicit: https://www.ford126.web.illinois.edu/wwwpapers/totients.pdf (Lemma 5.1). We use its specialization with no auxiliary factors (l = 0) and with the entire left shifted product squarefree above the terminal cutoff. The latter is already part of the application’s good-witness conditions. All its cutoff, small-remainder, small-cancelled-product and separation hypotheses are retained here. Its larger smooth-factor exponent is sufficient for the application; we do not assume the new comparison proposition of the manuscript.

def OAI.TotientAsymptotic.omegaIn line 26
def OAI.TotientAsymptotic.IsNormalPrime line 30
Source documentation
Ford's Definition 1, equations (2.1)–(2.2).
```
def IsNormalPrime (S : ℝ) (p : ℕ) : Prop :=
…
```
def OAI.TotientAsymptotic.SquarefreeAbove line 35
def OAI.TotientAsymptotic.partAbove line 38
structure OAI.TotientAsymptotic.ShiftedPair line 41
def OAI.TotientAsymptotic.shiftedProduct line 46
def OAI.TotientAsymptotic.FordComparisonConditions line 48
def OAI.TotientAsymptotic.FordComparisonParameters line 67
Source documentation
The cutoff and size restrictions of Ford's published lemma.
```
def FordComparisonParameters (b : ℕ) (y S : ℝ) (D r : ℕ) (Y U : ℕ → ℝ) : Prop :=
…
```
Mentions: OAI.TotientAsymptotic.D
def OAI.TotientAsymptotic.comparisonError line 77
def OAI.TotientAsymptotic.fordComparisonBound line 82
def OAI.TotientAsymptotic.FordLemma51Input line 90
lemma OAI.TotientAsymptotic.squarefreeAbove_of_dvd line 98
lemma OAI.TotientAsymptotic.shifted_factor_dvd line 103
lemma OAI.TotientAsymptotic.squarefree_shifts_of_common_product line 107