PPTMaximalSuffix.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The maximal common-prefix step in Ford, Section 5, between (5.19) and (5.20). The ordering of the candidate primes, rather than a bound for the whole residual product, rules out a repeated leading prime. Choosing the last possible common prefix then forces every nontrivial residual preimage to have a different largest prime.

lemma OAI.TotientAsymptotic.ppt_not_dvd_totient_of_prime_bound line 19
Source documentation
A prime larger than every prime of a cannot divide its totient.
```
lemma ppt_not_dvd_totient_of_prime_bound {p a : ℕ} (hp : p.Prime)
    (hsmall : ∀ q : ℕ, q.Prime → q ∣ a → q < p) : ¬p ∣ a.totient := by
…
```
Mentions: OAI.TotientAsymptotic.a

lemma OAI.TotientAsymptotic.ppt_remove_common_largest line 36

Source documentation

Cancel a common largest prime from a nontrivial preimage. Since the prime does not divide the target totient, it occurs only once.

lemma ppt_remove_common_largest {d p a n : ℕ} (hp : p.Prime)
    (hcop : p.Coprime a) (hnot : ¬p ∣ d*a.totient)
    (hn : 0 < n) (hφ : n.totient = d*(p*a).totient)
    (hbad : ¬p*a ∣ n) (hpn : p ∣ n)
    (hsmall : ∀ q : ℕ, q.Prime → q ∣ n → q ≤ p) :
    ∃ m : ℕ, 0 < m ∧ m.totient = d*a.totient ∧ ¬a ∣ m ∧
      (∀ q : ℕ, q.Prime → q ∣ m → q < p) ∧ n = p*m := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.m

def OAI.TotientAsymptotic.pptSuffixProduct line 73
Source documentation
The concrete suffix of a finite ordered candidate-prime list.
```
def pptSuffixProduct (p : ℕ → ℕ) (N j : ℕ) : ℕ :=
…
```
Mentions: OAI.TotientAsymptotic.N
lemma OAI.TotientAsymptotic.ppt_suffix_product_succ line 76
lemma OAI.TotientAsymptotic.ppt_suffix_product_pos line 80
lemma OAI.TotientAsymptotic.ppt_suffix_prime_lt line 84
def OAI.TotientAsymptotic.PPTPrefixWitness line 96
Source documentation
A residual nontrivial preimage whose prime factors fit after the already removed prefix. At index zero there is no preceding bound.
```
def PPTPrefixWitness (d : ℕ) (p : ℕ → ℕ) (N j : ℕ) : Prop :=
…
```
Mentions: OAI.TotientAsymptotic.N
lemma OAI.TotientAsymptotic.ppt_largest_prime_data line 101

theorem OAI.TotientAsymptotic.ppt_maximal_prefix_mismatch line 125

Source documentation

The last possible common prefix gives the precise largest-prime mismatch used before Ford's injective bad-preimage association. The assumptions are only primeness, decreasing order, and primes above d.

theorem ppt_maximal_prefix_mismatch {d N : ℕ} (hd : 0 < d) (p : ℕ → ℕ)
    (hprime : ∀ i < N, (p i).Prime)
    (horder : ∀ i k : ℕ, i < k → k < N → p k < p i)
    (hlarge : ∀ i < N, d < p i)
    (hbad : ∃ n : ℕ, 0 < n ∧ n.totient = d*(pptSuffixProduct p N 0).totient ∧
      ¬pptSuffixProduct p N 0 ∣ n) :
    ∃ j < N, PPTPrefixWitness d p N j ∧
      ∀ n : ℕ, 0 < n → n.totient = d*(pptSuffixProduct p N j).totient →
        ¬pptSuffixProduct p N j ∣ n → largestPrimeFactor n ≠ p j := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptSuffixProduct, OAI.TotientAsymptotic.PPTPrefixWitness, OAI.TotientAsymptotic.largestPrimeFactor