PPTCoordinateAlignment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Apply the unequal-list count to the actual ordering by prime size. This proves existence of a right prime at the required index, and then compares the largest factors of the two prime predecessors. The additive log K is the explicit cost of passing from a predecessor to its largest factor when its total number of prime factors is at most K.

theorem OAI.TotientAsymptotic.ppt_ordered_right_index line 17
theorem OAI.TotientAsymptotic.ppt_ordered_alignment_side line 40

theorem OAI.TotientAsymptotic.ppt_ordered_coordinate_alignment line 88

Source documentation

Ordered prime lists need not have equal total lengths. Once index j exists on both sides, normality aligns their largest predecessor factors with an explicit additive error.

theorem ppt_ordered_coordinate_alignment {k l D E j : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hjk : j < k) (hjl : j < l)
    {S ε K : ℝ} (hS : 1 < S) (hBS : 0 ≤ B S) (hK : 0 < K)
    (hD : D ≠ 0) (hE : E ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (hpa : Antitone p) (hqa : Antitone q)
    (heq : D*shiftedProduct p = E*shiftedProduct q)
    (hp3 : 3 ≤ p ⟨j,hjk⟩) (hq3 : 3 ≤ q ⟨j,hjl⟩)
    (hDS : (largestPrimeFactor D : ℝ) ≤
      min ((p ⟨j,hjk⟩-1 : ℕ) : ℝ) ((q ⟨j,hjl⟩-1 : ℕ) : ℝ))
    (hES : (largestPrimeFactor E : ℝ) ≤
      min ((p ⟨j,hjk⟩-1 : ℕ) : ℝ) ((q ⟨j,hjl⟩-1 : ℕ) : ℝ))
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_normalized_coordinate_alignment line 117

Source documentation

Normality supplies the factor-count and square-root error bounds. The remaining logarithmic error is explicit after normalization by B z.

theorem ppt_normalized_coordinate_alignment {k l D E j : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hjk : j < k) (hjl : j < l)
    {S z : ℝ} (hS : 1 < S) (hBS : 0 ≤ B S) (hBz : 0 < B z) (hSz : S ≤ z)
    (hD : D ≠ 0) (hE : E ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (hpa : Antitone p) (hqa : Antitone q)
    (heq : D*shiftedProduct p = E*shiftedProduct q)
    (hp3 : 3 ≤ p ⟨j,hjk⟩) (hq3 : 3 ≤ q ⟨j,hjl⟩)
    (hpz : (p ⟨j,hjk⟩-1 : ℕ) ≤ z) (hqz : (q ⟨j,hjl⟩-1 : ℕ) ≤ z)
    (hDS : (largestPrimeFactor D : ℝ) ≤
      min ((p ⟨j,hjk⟩-1 : ℕ) : ℝ) ((q ⟨j,hjl⟩-1 : ℕ) : ℝ))
    (hES : (largestPrimeFactor E : ℝ) ≤
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor