PPTPointwiseGrid.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual residual lists determine one of the finite comparison grids. The hypotheses below are arithmetic and geometric properties of those lists; the published comparison conditions and parameters are conclusions.

lemma OAI.TotientAsymptotic.ppt_B_mono line 17
lemma OAI.TotientAsymptotic.ppt_factor_coordinate_upper line 22
Source documentation
A predecessor bounded by the comparison endpoint gives an upper bound on its normalized largest-factor coordinate.
```
lemma ppt_factor_coordinate_upper {p : ℕ} {z : ℝ}
    (hp : 3 ≤ p) (hB : 0 < B z) (hpz : (p-1 : ℕ) ≤ z) :
    B (largestPrimeFactor (p-1))/B z ≤ 1 := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor

lemma OAI.TotientAsymptotic.ppt_terminal_coordinate_padding line 33

Source documentation

The vacant terminal interval pays for normality alignment at every retained index, including the full bottom-grid padding.

lemma ppt_terminal_coordinate_padding {j H : ℕ} {t L U δ u v w : ℝ}
    (hj : j ≤ H) (ht : 0 < t) (hδ : 0 ≤ δ)
    (hhigh : U < w) (hfactor : w/t-δ ≤ u)
    (halign : |u-v| ≤ (2*(j : ℝ)+1)*δ)
    (hbudget : (8*(H : ℝ)+20)*δ*t < (U-L)/4) :
    (L+U)/(2*t)+3*δ < min u v := by
…

Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.w

lemma OAI.TotientAsymptotic.ppt_terminal_grid_bottom line 63

Source documentation

A terminal gap in the prime coordinates survives passage to the largest factors and supplies the full bottom padding of the paired grid.

lemma ppt_terminal_grid_bottom {b H : ℕ} {t L U δ : ℝ}
    (hb : 0 < b) (hbH : b ≤ H) (ht : 0 < t) (hδ : 0 ≤ δ)
    (u v w : Fin b → ℝ)
    (hhigh : U < w ⟨b-1,by omega⟩)
    (hfactor : w ⟨b-1,by omega⟩/t-δ ≤ u ⟨b-1,by omega⟩)
    (halign : |u ⟨b-1,by omega⟩-v ⟨b-1,by omega⟩| ≤
      (2*((b-1 : ℕ) : ℝ)+1)*δ)
    (hbudget : (8*(H : ℝ)+20)*δ*t < (U-L)/4) :
    (L+U)/(2*t)+3*δ < min (u ⟨b-1,by omega⟩) (v ⟨b-1,by omega⟩) := by
…

Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.w

theorem OAI.TotientAsymptotic.ppt_pair_alignment_in_mesh line 77

Source documentation

Normality aligns the actual lists after cancellation. Smoothness of both integer multipliers is used only below their retained predecessors.

theorem ppt_pair_alignment_in_mesh {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop, ∀ (b H D : ℕ) (S V : ℝ) (p : ShiftedPair b),
      (H : ℝ) ≤ A*Real.log (B z) →
      1 < S → 0 ≤ B S → B S ≤ (H : ℝ)^4 → S ≤ V → V ≤ z →
      0 < D → 0 < p.remainder →
      (∀ i, IsNormalPrime S (p.left i) ∧ IsNormalPrime S (p.right i)) →
      (∀ i, 3 ≤ p.left i ∧ 3 ≤ p.right i) →
      Antitone p.left → Antitone p.right →
      D*shiftedProduct p.left = p.remainder*shiftedProduct p.right →
      (largestPrimeFactor D : ℝ) ≤ V → (largestPrimeFactor p.remainder : ℝ) ≤ V →
      (∀ i, V ≤ (p.left i-1 : ℕ) ∧ V ≤ (p.right i-1 : ℕ)) →
      (∀ i, (p.left i-1 : ℕ) ≤ z ∧ (p.right i-1 : ℕ) ≤ z) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_pointwise_grid_realization line 109

Source documentation

All literal grid intervals, parameters, and comparison conditions for an actual residual pair. The first cutoff and the adjacent separation are the quantitative prime-row conclusions established before grouping.

theorem ppt_pointwise_grid_realization {A γ : ℝ} (hA : 0 < A) (hγ : 0 < γ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (b H D c : ℕ) (S V L U : ℝ) (p : ShiftedPair b), ∀ hb : 0 < b,
      b ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H : ℝ)^4 →
      V = Real.exp (Real.exp ((L+U)/2)) → S ≤ V → V ≤ z →
      0 < D → 0 < c → 0 < p.remainder →
      (D : ℝ) ≤ z^(1/100 : ℝ) → (c.totient : ℝ) ≤ z^(1/10 : ℝ) →
      (∀ i, IsNormalPrime S (p.left i) ∧ IsNormalPrime S (p.right i)) →
      (∀ i, 3 ≤ p.left i ∧ 3 ≤ p.right i ∧ p.left i ≠ p.right i) →
      Antitone p.left → Antitone p.right →
      D*shiftedProduct p.left = p.remainder*shiftedProduct p.right →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct