PPTGridMargins.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The quantitative margins for the actual PPT paired grid. The last retained coordinates have size at least t^(-1/3); their inverse-cube relative gaps dominate the normality mesh when the dimension is logarithmic in t.

lemma OAI.TotientAsymptotic.ppt_paired_gap_of_left_gap line 21
Source documentation
A left-coordinate gap survives both alignment errors and the stated grid padding.
```
lemma ppt_paired_gap_of_left_gap {u v u' v' A B padding : ℝ}
    (hprev : |u-v| ≤ A) (hnext : |u'-v'| ≤ B)
    (hgap : u'+A+B+padding < u) :
    max u' v'+padding < min u v := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B

lemma OAI.TotientAsymptotic.ppt_adaptive_head_edge line 32

Source documentation

A genuine head-to-tail gap supplies an adaptive lower endpoint.

lemma ppt_adaptive_head_edge {first u v : ℝ}
    (hgap : first < min u v) (htop : max u v ≤ 1) :
    ∃ θ : ℝ, first < θ ∧ θ ≤ min u v ∧ θ < 1 := by
…

lemma OAI.TotientAsymptotic.ppt_contraction_gap line 41

theorem OAI.TotientAsymptotic.ppt_log_dimension_separation line 55

Source documentation

The entire grid-padding cost is smaller than a fixed fraction of the last retained coordinate's inverse-cube gap, uniformly in the dimension.

theorem ppt_log_dimension_separation {C : ℝ} (_hC : 0 < C) :
    ∀ᶠ t : ℝ in atTop, ∀ H : ℕ,
      1 ≤ H → (H : ℝ) ≤ C*Real.log t →
      (8*(H : ℝ)+20)*(2*(Real.log t)^5/Real.sqrt t) <
        1/(40*(H : ℝ)^3*t^(1/3 : ℝ)) := by
…

theorem OAI.TotientAsymptotic.ppt_logarithmic_alignment_error line 103
Source documentation
The additive logarithmic factor-count error can be included by doubling the square-root mesh.
```
theorem ppt_logarithmic_alignment_error :
    ∀ᶠ t : ℝ in atTop,
      Real.log (3*t)/t ≤ (Real.log t)^5/Real.sqrt t := by
…
```

theorem OAI.TotientAsymptotic.ppt_grid_error_absorbed_two_mesh line 133

Source documentation

The doubled mesh also fits in the inverse-cube exponent margin.

theorem ppt_grid_error_absorbed_two_mesh {C : ℝ} (hC : 0 < C) :
    ∀ᶠ t : ℝ in atTop, ∀ (b H r : ℕ) (e w η δ : ℝ),
      1 ≤ H → b ≤ H → r+1 ≤ H → (H : ℝ) ≤ C*Real.log t →
      0 ≤ δ → δ ≤ 2*((Real.log t)^5/Real.sqrt t) →
      e ≤ (2*(b : ℝ)+4)*δ → w ≤ (4*(b : ℝ)+3)*δ → η ≤ δ →
      e*(∑ j ∈ Finset.Icc 1 (b-1), a j)+2*(b-1 : ℕ)*w+
        η*(∑ i ∈ Finset.Icc 2 b, ((i : ℝ)*Real.log i+i)) ≤
          rowContractionError r/16 := by
…

Mentions: OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.rowContractionError

theorem OAI.TotientAsymptotic.ppt_local_normality_error_mesh line 173
Source documentation
The indexed local choice B S = h^4 fits the same PPT mesh whenever the remaining length is logarithmic in the comparison double logarithm. The cutoff itself is a parameter, so no global normality transfer is used.
```
theorem ppt_local_normality_error_mesh {A : ℝ} (_hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (h : ℕ) (S : ℝ),
      (h : ℝ) ≤ A*Real.log t → 0 ≤ B S → B S ≤ (h : ℝ)^4 →
      Real.sqrt (B S/t) ≤ (Real.log t)^5/Real.sqrt t := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B
theorem OAI.TotientAsymptotic.ppt_local_normality_height_bound line 208
Source documentation
The fourth-power indexed normality height is below the terminal two-thirds-power height throughout the same logarithmic length range.
```
theorem ppt_local_normality_height_bound {A : ℝ} (_hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ h : ℕ,
      (h : ℝ) ≤ A*Real.log t → (h : ℝ)^4 ≤ t^(2/3 : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.A
theorem OAI.TotientAsymptotic.ppt_local_normality_terminal_cutoff line 234
Source documentation
If B S ≤ h^4 and the terminal cutoff has double logarithm at least t^(2/3), the literal Ford condition S ≤ Y follows.
```
theorem ppt_local_normality_terminal_cutoff {A : ℝ} (hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (h : ℕ) (S Y : ℝ),
      (h : ℝ) ≤ A*Real.log t → 1 < S → 1 < Y →
      B S ≤ (h : ℝ)^4 → t^(2/3 : ℝ) ≤ B Y → S ≤ Y := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B