PPTSelectedGrid.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual finite comparison label after terminal selection.

lemma OAI.TotientAsymptotic.ppt_seed_tail_largest_le line 13

theorem OAI.TotientAsymptotic.ppt_terminal_retained_predecessor line 28

Source documentation

A retained prime above the vacant window has predecessor above the middle cutoff. This does not require any right-coordinate alignment.

theorem ppt_terminal_retained_predecessor : ∀ᶠ z : ℝ in atTop,
    ∀ (p H : ℕ) (S L U : ℝ), 3 ≤ p → 1 < S → 0 ≤ B S → S ≤ z →
      IsNormalPrime S p → (p-1 : ℕ) ≤ z → U < B p →
      (8*(H : ℝ)+20)*(2*((Real.log (B z))^5/Real.sqrt (B z)))*B z < (U-L)/4 →
      Real.exp (Real.exp ((L+U)/2)) ≤ (p-1 : ℕ) := by
…

Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime

theorem OAI.TotientAsymptotic.ppt_selected_grid_data line 65

Source documentation

The selected actual prefix yields a finite arithmetic label and the literal comparison data, including its strict exponent. All size, normality and geometric assumptions concern the original candidate and the chosen preimage; no bound for a residual family is assumed.

theorem ppt_selected_grid_data (d : ℕ) (hd : 0 < d) {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n N Q J H E r j : ℕ) (p : Fin N → ℕ) (q : Fin Q → ℕ)
      (v : Fin n → ℝ) (ι : Fin N ↪o Fin n) (budget g S L U V : ℝ),
      ∀ hJ : 0 < J, ∀ hJN : J ≤ N, ∀ hJQ : J ≤ Q,
      n ≤ m → N ≤ H → j ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      m-(ι ⟨0,hJ.trans_le hJN⟩).val ≤ H →
      v ∈ relaxedGeometricFamily m n budget g → (∀ i,v (ι i)=B (p i)) →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H : ℝ)^4 →
      V=Real.exp (Real.exp ((L+U)/2)) → S ≤ V → V ≤ z →
      (B z)^(2/3 : ℝ) ≤ L → L < U → U ≤ 2*(B z)^(2/3 : ℝ) →
      (largestPrimeFactor d : ℝ) ≤ S →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.largestPrimeFactor