PPTBadWitness.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The injective choice of nontrivial preimages used in Ford, Section 5, p. 25, between (5.20) and (5.21). Candidate sets are partitioned by their totient value. A singleton fiber uses its given nontrivial preimage; on a larger fiber, a cyclic permutation followed by multiplication by a fixed seed preimage supplies distinct nontrivial preimages. The full fiber multiplicity is retained throughout this construction.

lemma OAI.TotientAsymptotic.ppt_finRotate_ne_self line 19
def OAI.TotientAsymptotic.pptFiniteRotation line 32
lemma OAI.TotientAsymptotic.pptFiniteRotation_ne_self line 35
lemma OAI.TotientAsymptotic.ppt_rough_eq_of_dvd_same_totient line 47
Source documentation
Two rough candidates of the same totient cannot properly divide one another. The only alternative in the general totient lemma is doubling, which roughness excludes.
```
lemma ppt_rough_eq_of_dvd_same_totient {d b c : ℕ} (hd : 0 < d)
    (hc : ∀ p : ℕ, p.Prime → p ∣ c → d+1 < p)
    (hφ : b.totient = c.totient) (hdiv : b ∣ c) : b = c := by
…
```
lemma OAI.TotientAsymptotic.ppt_rough_eq_of_dvd_seed_multiple line 56
lemma OAI.TotientAsymptotic.ppt_bad_witness_on_fiber line 64

theorem OAI.TotientAsymptotic.ppt_injective_bad_preimages_seed_branch line 121

Source documentation

The injective association retains its seed-multiple construction on every nonsingleton totient fiber. This is needed for normality exclusion.

theorem ppt_injective_bad_preimages_seed_branch {d q : ℕ} (hd : 0 < d)
    (hqpos : 0 < q) (hq : q.totient = d) (S : Finset ℕ)
    (hS : ∀ n ∈ S, 0 < n ∧ ∀ p : ℕ, p.Prime → p ∣ n → d+1 < p)
    (hbad : ∀ n ∈ S, ∃ u : ℕ, 0 < u ∧ u.totient = d*n.totient ∧ ¬n ∣ u) :
    ∃ F : ℕ → ℕ, Set.InjOn F (S : Set ℕ) ∧
      (∀ n ∈ S, 0 < F n ∧ (F n).totient = d*n.totient ∧ ¬n ∣ F n) ∧
      ∀ n ∈ S, (∃ m ∈ S, m ≠ n ∧ m.totient = n.totient) →
        ∃ c ∈ S, F n = c*q := by
…

Mentions: OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.ppt_injective_bad_preimages line 167

Source documentation

The bad-preimage association is injective even when many candidates share one totient. No injectivity of the totient function is assumed.

theorem ppt_injective_bad_preimages {d q : ℕ} (hd : 0 < d)
    (hqpos : 0 < q) (hq : q.totient = d) (S : Finset ℕ)
    (hS : ∀ n ∈ S, 0 < n ∧ ∀ p : ℕ, p.Prime → p ∣ n → d+1 < p)
    (hbad : ∀ n ∈ S, ∃ u : ℕ, 0 < u ∧ u.totient = d*n.totient ∧ ¬n ∣ u) :
    ∃ F : ℕ → ℕ, Set.InjOn F (S : Set ℕ) ∧
      ∀ n ∈ S, 0 < F n ∧ (F n).totient = d*n.totient ∧ ¬n ∣ F n := by
…

theorem OAI.TotientAsymptotic.ppt_injective_failed_candidates line 180

Source documentation

In particular, all failed candidates can be counted by distinct nontrivial target preimages. The only arithmetic hypothesis on the seed is that it is a positive totient.

theorem ppt_injective_failed_candidates {d : ℕ} (hd : IsTotient d) (S : Finset ℕ)
    (hS : ∀ n ∈ S, 0 < n ∧ ∀ p : ℕ, p.Prime → p ∣ n → d+1 < p)
    (hbad : ∀ n ∈ S, ¬FullFiber d n) :
    ∃ F : ℕ → ℕ, Set.InjOn F (S : Set ℕ) ∧
      ∀ n ∈ S, 0 < F n ∧ (F n).totient = d*n.totient ∧ ¬n ∣ F n := by
…

Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.FullFiber