PPTComparisonBridge.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed-common-factor and fixed-left-tail arithmetic for Ford's comparison estimate. Fixing the left tail a includes its totient in D = d * φ(a), and the common prime product c supplies the divisor r = φ(c).

lemma OAI.TotientAsymptotic.ppt_totient_primeProduct line 17

lemma OAI.TotientAsymptotic.ppt_common_tail_totient line 31

Source documentation

The three factors are genuinely coprime; high primes are distinct.

lemma ppt_common_tail_totient {b c a : ℕ} (p : Fin b → ℕ)
    (hp : ∀ i, (p i).Prime) (hinj : Function.Injective p)
    (hca : c.Coprime a) (hcp : c.Coprime (∏ i, p i))
    (hap : a.Coprime (∏ i, p i)) :
    (c*a*∏ i, p i).totient = c.totient*a.totient*shiftedProduct p := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.shiftedProduct

theorem OAI.TotientAsymptotic.ppt_fixed_comparison_equation line 41

Source documentation

Canceling the totient of the actual common factor gives exactly the equation required by the l = 0 comparison theorem.

theorem ppt_fixed_comparison_equation {b d c a e : ℕ}
    (p q : Fin b → ℕ) (hc : 0 < c)
    (hp : ∀ i, (p i).Prime) (hq : ∀ i, (q i).Prime)
    (hpinj : Function.Injective p) (hqinj : Function.Injective q)
    (hca : c.Coprime a) (hcp : c.Coprime (∏ i, p i))
    (hap : a.Coprime (∏ i, p i))
    (hce : c.Coprime e) (hcq : c.Coprime (∏ i, q i))
    (heq : e.Coprime (∏ i, q i))
    (hvalue : (c*e*∏ i, q i).totient = d*(c*a*∏ i, p i).totient) :
    (d*a.totient)*shiftedProduct p = e.totient*shiftedProduct q := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.shiftedProduct

theorem OAI.TotientAsymptotic.ppt_fixed_comparison_size line 64

Source documentation

The scale controls the seed-multiplied totient. A bound on φ(n) alone is insufficient when the seed multiplier exceeds one.

theorem ppt_fixed_comparison_size {b d c a : ℕ} {z : ℝ}
    (p : Fin b → ℕ) (hc : 0 < c)
    (hp : ∀ i, (p i).Prime) (hpinj : Function.Injective p)
    (hca : c.Coprime a) (hcp : c.Coprime (∏ i, p i))
    (hap : a.Coprime (∏ i, p i))
    (hsize : ((d*(c*a*∏ i, p i).totient : ℕ) : ℝ) ≤ z) :
    (((d*a.totient)*shiftedProduct p : ℕ) : ℝ) ≤ z/c.totient := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.shiftedProduct

def OAI.TotientAsymptotic.pptFixedComparisonPair line 76
lemma OAI.TotientAsymptotic.pptFixedComparisonPair_equation line 79
lemma OAI.TotientAsymptotic.ppt_fixed_comparison_injective line 95
Source documentation
At fixed c,a, the actual candidate integer is recovered from the left high-prime list. No injectivity of the totient is used.
```
lemma ppt_fixed_comparison_injective {b c a : ℕ} (S : Finset ℕ)
    (p q : ℕ → Fin b → ℕ) (e : ℕ → ℕ)
    (hreal : ∀ n ∈ S, n = c*a*∏ i, p n i) :
    Set.InjOn (fun n => pptFixedComparisonPair (p n) (q n) (e n)) (S : Set ℕ) := by
…
```
Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.pptFixedComparisonPair

theorem OAI.TotientAsymptotic.ppt_fixed_comparison_count line 106

Source documentation

Direct unconditional use of the proved Ford comparison estimate on a fixed (c,a) block. All remaining hypotheses are the literal published comparison predicates.

theorem ppt_fixed_comparison_count :
    ∃ C z₀ : ℝ, 0 < C ∧ 1 < z₀ ∧
    ∀ (b d c a : ℕ) (z W : ℝ) (Y U : ℕ → ℝ),
      z₀ ≤ z → FordComparisonParameters b z W (d*a.totient) c.totient Y U →
      ∀ (S : Finset ℕ) (p q : ℕ → Fin b → ℕ) (e : ℕ → ℕ),
        (∀ n ∈ S, n = c*a*∏ i, p n i) →
        (∀ n ∈ S, FordComparisonConditions b z W (d*a.totient) c.totient Y U
          (pptFixedComparisonPair (p n) (q n) (e n))) →
        (S.card : ℝ) ≤ fordComparisonBound C b z W (d*a.totient) c.totient Y U := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.FordComparisonParameters, OAI.TotientAsymptotic.FordComparisonConditions, OAI.TotientAsymptotic.pptFixedComparisonPair, OAI.TotientAsymptotic.fordComparisonBound