PPTHeadEdge.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A single lower endpoint for all leading prime factors in a local PPT comparison block. It depends only on the comparison scale, so the finite grid count does not require any continuously varying labels.

def OAI.TotientAsymptotic.pptUniformHeadEdge line 18
theorem OAI.TotientAsymptotic.ppt_normal_head_uniform_edge line 22
Source documentation
Every normal large head lies above the same normalized endpoint. The hypotheses are local to z, including the normality cutoff.
```
theorem ppt_normal_head_uniform_edge : ∀ᶠ z : ℝ in atTop,
    ∀ (p : ℕ) (S : ℝ), 1 < S → 0 ≤ B S → S ≤ z →
      IsNormalPrime S p → z^(9/10 : ℝ) ≤ p → (p-1 : ℕ) ≤ z →
      pptUniformHeadEdge (B z) ≤ B (largestPrimeFactor (p-1))/B z ∧
      B (largestPrimeFactor (p-1))/B z ≤ 1 := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.pptUniformHeadEdge, OAI.TotientAsymptotic.largestPrimeFactor
lemma OAI.TotientAsymptotic.ppt_uniform_head_edge_lt_one line 70
lemma OAI.TotientAsymptotic.ppt_aligned_heads_uniform_edge line 81
Source documentation
Only the left head needs a large-prime size estimate. Alignment places both heads above one common endpoint without imposing that size estimate separately on the arbitrary right preimage.
```
lemma ppt_aligned_heads_uniform_edge {t u v η : ℝ}
    (ht : 1 ≤ t) (hu : pptUniformHeadEdge t ≤ u) (halign : |u-v| ≤ η) :
    pptUniformHeadEdge t-η ≤ min u v ∧ pptUniformHeadEdge t-η < 1 := by
…
```
Mentions: OAI.TotientAsymptotic.pptUniformHeadEdge
theorem OAI.TotientAsymptotic.ppt_first_cutoff_below_uniform_head line 93
Source documentation
The uniform head loss is smaller than every fixed inverse-log-cube margin, so the same lower edge works for every pair in a grid class.
```
theorem ppt_first_cutoff_below_uniform_head {γ : ℝ} (hγ : 0 < γ) :
    ∀ᶠ t : ℝ in atTop, ∀ ν : ℝ,
      ν ≤ 1-γ/(Real.log t)^3 → ν < pptUniformHeadEdge t := by
…
```
Mentions: OAI.TotientAsymptotic.pptUniformHeadEdge
theorem OAI.TotientAsymptotic.ppt_first_cutoff_below_aligned_head line 121
Source documentation
The same head endpoint still lies above the first cutoff after the uniform alignment allowance used by the doubled PPT mesh.
```
theorem ppt_first_cutoff_below_aligned_head {γ : ℝ} (hγ : 0 < γ) :
    ∀ᶠ t : ℝ in atTop, ∀ ν η : ℝ,
      ν ≤ 1-γ/(Real.log t)^3 →
      η ≤ 2*((Real.log t)^5/Real.sqrt t) →
      ν < pptUniformHeadEdge t-η := by
…
```
Mentions: OAI.TotientAsymptotic.pptUniformHeadEdge