ActualFordData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

All Ford hypotheses for a block of actual good tuple pairs.

structure OAI.TotientAsymptotic.GoodCollisionBlock line 17
Source documentation
The arithmetic data of a good collision in a single counting block. The positive-index block endpoints will be supplied by dyadic subdivision.
```
structure GoodCollisionBlock (x t : ℝ) (H i : ℕ) (y : ℝ)
    (q : TotientTuple (R x H) × TotientTuple (R x H)) : Prop where
…
```
Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R
theorem OAI.TotientAsymptotic.actual_ford_data line 33
Source documentation
The finite grid, all published parameter and pointwise restrictions, and the full strict exponent saving are consequences of the actual good data.
```
theorem actual_ford_data : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, i ≤ R x H → L x H < m x → R x H < L x H → ∀ t y : ℝ,
    1 < y → 0 < B y → (87/100 : ℝ)*fordBandScale x i ≤ B y →
    B y ≤ 2*fordBandScale x i →
    ∀ q : TotientTuple (R x H) × TotientTuple (R x H), GoodCollisionBlock x t H i y q →
    let η := chosenRemainder x H q.1.tail
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.GoodCollisionBlock, OAI.TotientAsymptotic.chosenRemainder