FordCoordinateBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete bounds and nondegeneracy of the two coordinates in the bootstrap.

lemma OAI.TotientAsymptotic.first_two_a_bounds line 10
lemma OAI.TotientAsymptotic.prime_preimage_B_bound line 19
lemma OAI.TotientAsymptotic.ford_coordinate_upper line 43
lemma OAI.TotientAsymptotic.two_coordinate_failure_second_lower line 69
lemma OAI.TotientAsymptotic.two_coordinate_failure_large_second line 84
Source documentation
A violating pair has a genuinely large third prime factor. This also rules out padded coordinates before applying the two-band estimate.
```
lemma two_coordinate_failure_large_second {x ω : ℝ} {n : ℕ} (hx : 4 ≤ x)
    (hBx : 12 ≤ B x) (hω : 0 ≤ ω) (hn : 0 < n) (hφ : (n.totient:ℝ) ≤ x)
    (hbad : (1+ω)*B x < a 1*fordPrimeCoordinate n 1+a 2*fordPrimeCoordinate n 2) :
    4 < primeDoubleLog n 2 ∧ 3 ≤ n.primeFactorsList.length := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.fordPrimeCoordinate, OAI.TotientAsymptotic.primeDoubleLog