PPTLeadingMismatch.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Transport the actual largest-prime mismatch into the ordered high-prime list used in the comparison equation. Retaining the canonical low part is essential here: smoothness of its totient alone would not suffice.

lemma OAI.TotientAsymptotic.ppt_largestPrimeFactor_mono_dvd line 16
lemma OAI.TotientAsymptotic.ppt_preimage_largest_above_normal_shift line 25
Source documentation
A normal shifted prime dividing the target forces an actual prime above the low cutoff as soon as its interval has positive normality mass.
```
lemma ppt_preimage_largest_above_normal_shift {n r : ℕ} {S T : ℝ}
    (hn : 0 < n) (hr : IsNormalPrime S r) (hdiv : r-1 ∣ n.totient)
    (hST : S < T) (hTr : T ≤ (r-1 : ℕ))
    (hgap : Real.sqrt (B S*B T) < B T-B S) :
    S < (largestPrimeFactor n : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor
lemma OAI.TotientAsymptotic.ppt_actual_preimage_largest_above_of_gap line 40
lemma OAI.TotientAsymptotic.ppt_partBelow_largest_le line 53
lemma OAI.TotientAsymptotic.ppt_leading_prime_of_split line 62

theorem OAI.TotientAsymptotic.ppt_preimage_split_largest line 88

Source documentation

An actual preimage with a prime above S has a nonempty high list, and its first entry is its largest prime.

theorem ppt_preimage_split_largest {n : ℕ} {S : ℝ} (hn : 0 < n) (hS : 1 ≤ S)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime S p)
    (hlarge : S < (largestPrimeFactor n : ℝ)) :
    ∃ (l : ℕ) (hl : 0 < l) (q : Fin l → ℕ) (s : ℕ),
      0 < s ∧ n = s*∏ i, q i ∧
      (largestPrimeFactor s.totient : ℝ) ≤ S ∧ StrictAnti q ∧
      (∀ i, IsNormalPrime S (q i) ∧ S < (q i : ℝ)) ∧
      n.totient = s.totient*shiftedProduct q ∧
      largestPrimeFactor n = q ⟨0, hl⟩ := by
…

Mentions: OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.shiftedProduct

theorem OAI.TotientAsymptotic.ppt_actual_preimage_leading_mismatch line 116

Source documentation

The mismatch supplied by the maximal common-prefix argument now holds for the first displayed high prime in the literal comparison equation, rather than being an additional assumption about that list.

theorem ppt_actual_preimage_leading_mismatch {k d n r : ℕ} (p : Fin k → ℕ)
    {S : ℝ} (hn : 0 < n) (hS : 1 ≤ S)
    (hp : ∀ i, (p i).Prime) (hpinj : Function.Injective p)
    (hvalue : n.totient = d*(∏ i, p i).totient)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ q : ℕ, q.Prime → q ∣ n → IsNormalPrime S q)
    (hlarge : S < (largestPrimeFactor n : ℝ))
    (hmismatch : largestPrimeFactor n ≠ r) :
    ∃ (l : ℕ) (hl : 0 < l) (q : Fin l → ℕ) (E : ℕ),
      0 < E ∧ (largestPrimeFactor E : ℝ) ≤ S ∧ StrictAnti q ∧
      (∀ i, IsNormalPrime S (q i) ∧ S < (q i : ℝ)) ∧
      d*shiftedProduct p = E*shiftedProduct q ∧ q ⟨0, hl⟩ ≠ r := by
…

Mentions: OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.shiftedProduct

theorem OAI.TotientAsymptotic.ppt_actual_preimage_leading_mismatch_of_gap line 140

Source documentation

Version with the high-prime existence derived from the concrete normality gap on one candidate shift.

theorem ppt_actual_preimage_leading_mismatch_of_gap {k d n r : ℕ}
    (p : Fin k → ℕ) (j : Fin k) {S T : ℝ} (hn : 0 < n) (hS : 1 ≤ S)
    (hp : ∀ i, (p i).Prime) (hpinj : Function.Injective p)
    (hvalue : n.totient = d*(∏ i, p i).totient)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ q : ℕ, q.Prime → q ∣ n → IsNormalPrime S q)
    (hj : IsNormalPrime S (p j)) (hST : S < T) (hTj : T ≤ (p j-1 : ℕ))
    (hgap : Real.sqrt (B S*B T) < B T-B S)
    (hmismatch : largestPrimeFactor n ≠ r) :
    ∃ (l : ℕ) (hl : 0 < l) (q : Fin l → ℕ) (E : ℕ),
      0 < E ∧ (largestPrimeFactor E : ℝ) ≤ S ∧ StrictAnti q ∧
      (∀ i, IsNormalPrime S (q i) ∧ S < (q i : ℝ)) ∧
…

Mentions: OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor