PPTNormalWitness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite singleton-fiber reduction in Ford's exclusion (vi). If the candidate primes and the fixed seed primes are normal, a chosen preimage with a nonnormal prime can only come from a singleton candidate-totient fiber. The exceptional candidates therefore give distinct target totients, retaining the multiplicities elsewhere in the construction.

theorem OAI.TotientAsymptotic.ppt_nonnormal_witness_totient_injective line 20

Source documentation

A nonnormal chosen preimage cannot lie in the seed-multiple branch of the injective witness construction.

theorem ppt_nonnormal_witness_totient_injective {S Q : Finset ℕ}
    {F : ℕ → ℕ} {q : ℕ} {W : ℝ} (hQS : Q ⊆ S)
    (hS : ∀ n ∈ S, ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime W p)
    (hq : ∀ p : ℕ, p.Prime → p ∣ q → IsNormalPrime W p)
    (hbranch : ∀ n ∈ S,
      (∃ m ∈ S, m ≠ n ∧ m.totient = n.totient) →
        ∃ c ∈ S, F n = c*q)
    (hbad : ∀ n ∈ Q, ∃ p : ℕ, p.Prime ∧ p ∣ F n ∧ ¬IsNormalPrime W p) :
    Set.InjOn Nat.totient (Q : Set ℕ) := by
…

Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.ppt_nonnormal_witness_target_injective line 40

Source documentation

The corresponding seed-scaled target totients are distinct as well.

theorem ppt_nonnormal_witness_target_injective {S Q : Finset ℕ}
    {F : ℕ → ℕ} {d q : ℕ} {W : ℝ} (hd : 0 < d) (hQS : Q ⊆ S)
    (hS : ∀ n ∈ S, ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime W p)
    (hq : ∀ p : ℕ, p.Prime → p ∣ q → IsNormalPrime W p)
    (hbranch : ∀ n ∈ S,
      (∃ m ∈ S, m ≠ n ∧ m.totient = n.totient) →
        ∃ c ∈ S, F n = c*q)
    (hbad : ∀ n ∈ Q, ∃ p : ℕ, p.Prime ∧ p ∣ F n ∧ ¬IsNormalPrime W p) :
    Set.InjOn (fun n : ℕ => d*n.totient) (Q : Set ℕ) := by
…

Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.ppt_nonnormal_witness_count line 56

Source documentation

Counting nonnormal chosen preimages reduces to counting their actual distinct target totients. The analytic exceptional-value estimate is a separate input to this finite reduction.

theorem ppt_nonnormal_witness_count {S Q T : Finset ℕ}
    {F : ℕ → ℕ} {d q : ℕ} {W : ℝ} (hd : 0 < d) (hQS : Q ⊆ S)
    (hS : ∀ n ∈ S, ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime W p)
    (hq : ∀ p : ℕ, p.Prime → p ∣ q → IsNormalPrime W p)
    (hbranch : ∀ n ∈ S,
      (∃ m ∈ S, m ≠ n ∧ m.totient = n.totient) →
        ∃ c ∈ S, F n = c*q)
    (hbad : ∀ n ∈ Q, ∃ p : ℕ, p.Prime ∧ p ∣ F n ∧ ¬IsNormalPrime W p)
    (hT : ∀ n ∈ Q, d*n.totient ∈ T) :
    Q.card ≤ T.card := by
…

Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.m