BootstrapViolation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A power-saving two-coordinate exception, with fixed explicit cutoffs.

theorem OAI.TotientAsymptotic.bootstrap_regular_violation line 13
Source documentation
The regular part of Ford Lemma 4.2 at the single parameter needed to start the global counting bootstrap.
```
theorem bootstrap_regular_violation : ∃ C : ℝ,0 < C ∧ ∀ᶠ X : ℕ in atTop,
    ∀ Q : Finset ℕ,
    (∀ v ∈ Q,v ≤ X ∧ CountingRegular (loglogCutoff (bootstrapBottom (B X))) X v ∧
      ∃ n : ℕ,0 < n ∧ n.totient=v ∧
        (101/100:ℝ)*B X < a 1*fordPrimeCoordinate n 1+a 2*fordPrimeCoordinate n 2) →
    (Q.card:ℝ) ≤ C*X*(Real.log X)^(-201/200:ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.CountingRegular, OAI.TotientAsymptotic.loglogCutoff, OAI.TotientAsymptotic.bootstrapBottom, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.fordPrimeCoordinate