CollisionDyadicSize.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Dyadic endpoints for actual shifted-prime suffixes.

lemma OAI.TotientAsymptotic.dyadic_shift_log_bound line 14
theorem OAI.TotientAsymptotic.collision_suffix_dyadic_size line 40
Source documentation
The first prime in every actual positive-index suffix lies above y^0.9 at its dyadic counting endpoint. The endpoint has the same Ford band scale, uniformly over every retained index.
```
theorem collision_suffix_dyadic_size : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → i+2 ≤ L x H → L x H < m x →
    ∀ η : RemainderDatum (L x H), IsBasicRemainder x H η → ∀ y : ℝ,
    y/2 < ((remainderPrime η i-1)*(suffixPreimage η i).totient : ℕ) →
    (((remainderPrime η i-1)*(suffixPreimage η i).totient : ℕ) : ℝ) ≤ y →
    y^(9/10 : ℝ) ≤ remainderPrime η i ∧
    (87/100 : ℝ)*fordBandScale x i ≤ B y ∧ B y ≤ (113/100 : ℝ)*fordBandScale x i := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.remainderPrime, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.B