CollisionHeadSize.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The zero-index collision uses the original endpoint and a subpower tail.

lemma OAI.TotientAsymptotic.basic_remainder_subpower line 14
theorem OAI.TotientAsymptotic.collision_head_small_factors line 29
Source documentation
At the first differing head prime, both the fixed residual and every canceled shift already fit under the original endpoint to power 1/100.
```
theorem collision_head_small_factors (H : ℕ) : ∀ᶠ x : ℝ in atTop,
    ∀ k p q : ℕ, L x H < m x → k < L x H → p.Prime → p ≠ q →
    ∀ η ξ : RemainderDatum (L x H), IsBasicRemainder x H η →
    ((suffixPreimage η k).totient : ℝ) ≤ x^(1/100 : ℝ) ∧
    (collisionCanceledProduct p q η ξ 0 k : ℝ) ≤ x^(1/100 : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.collisionCanceledProduct