CollisionCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting the residual tuple data forgotten by Ford's comparison map.

abbrev OAI.TotientAsymptotic.RecoveredPair line 14
lemma OAI.TotientAsymptotic.recovered_pair_fiber_bound line 16

theorem OAI.TotientAsymptotic.ford_comparison_with_recovery line 64

Source documentation

Ford's comparison counts prime lists and one residual integer. Restoring both missing prefix tails costs only their prime-occurrence allocations.

theorem ford_comparison_with_recovery (hford : FordLemma51Input) :
    ∃ C y₀ : ℝ, 0 < C ∧ 1 < y₀ ∧
    ∀ (b n K : ℕ) (y S : ℝ) (D r : ℕ) (Y U : ℕ → ℝ),
      y₀ ≤ y → FordComparisonParameters b y S D r Y U →
      ∀ Q : Finset (RecoveredPair b n),
        (∀ q ∈ Q, FordComparisonConditions b y S D r Y U q.1) →
        (∀ q ∈ Q, q.1.remainder.primeFactorsList.length ≤ K) →
        (∀ q ∈ Q, (∀ i, 1 ≤ q.2.1.primes i) ∧ (∀ i, 1 ≤ q.2.2.primes i)) →
        (∀ q ∈ Q, q.2.1.d * (∏ i, (q.2.1.primes i-1)) = D ∧
          q.2.2.d * (∏ i, (q.2.2.primes i-1)) = q.1.remainder) →
        (Q.card : ℝ) ≤ (n+1 : ℝ)^(D.primeFactorsList.length+K) *
          fordComparisonBound C b y S D r Y U := by
…

Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.FordComparisonParameters, OAI.TotientAsymptotic.RecoveredPair, OAI.TotientAsymptotic.FordComparisonConditions, OAI.TotientAsymptotic.fordComparisonBound