PPTRegularWitness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Build a counted grid witness from an actual regular totient preimage.

theorem OAI.TotientAsymptotic.ppt_large_head_above_terminal line 14
Source documentation
The large-head conclusion used by the comparison also places the first prime above every terminal window.
```
theorem ppt_large_head_above_terminal : ∀ᶠ z : ℝ in atTop,
    ∀ p : ℕ, z^(9/10:ℝ) ≤ p → 2*(B z)^(2/3:ℝ) < B p := by
…
```
Mentions: OAI.TotientAsymptotic.B
theorem OAI.TotientAsymptotic.ppt_prime_in_label_range line 39
Source documentation
The finite label cutoff contains every actual prime whose predecessor divides a value in the current comparison interval.
```
theorem ppt_prime_in_label_range : ∀ᶠ z : ℝ in atTop,
    ∀ p : ℕ, 3 ≤ p → (p-1:ℕ) ≤ z → p ≤ discardPrimeBound (B z) := by
…
```
Mentions: OAI.TotientAsymptotic.discardPrimeBound, OAI.TotientAsymptotic.B
lemma OAI.TotientAsymptotic.ppt_nonhead_product_succ line 52

theorem OAI.TotientAsymptotic.ppt_contracted_nonhead_product line 70

Source documentation

Every nonleading product in the actual contracting list is a small power of the local endpoint. This pays for the common canceled factor.

theorem ppt_contracted_nonhead_product {A : ℝ} (hA : 0 < A) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ z : ℝ in atTop,∀ (N H : ℕ) (p : Fin N → ℕ) (ω : ℝ),∀ hN : 0 < N,
      (∀ i,(p i).Prime) → (∀ i,3 ≤ p i) → 1 ≤ H → N ≤ H →
      (H:ℝ) ≤ A*Real.log (B z) → 1/(10*(H:ℝ)^3) ≤ ω → ω ≤ 1 →
      (∀ i:Fin N,0 < i.val → B (p i) ≤ B (p ⟨0,hN⟩)/(1+ω)) →
      (p ⟨0,hN⟩-1:ℕ) ≤ z →
      (((∏ i ∈ Finset.univ.filter (fun i:Fin N=>0 < i.val),p i):ℕ):ℝ) ≤ z^ε := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B

theorem OAI.TotientAsymptotic.ppt_regular_geometric_witness line 116

Source documentation

An actual regular alternative preimage produces the finite grid witness consumed by the counting theorem. This is the suffix case, in which the candidate head itself belongs to the geometric row.

theorem ppt_regular_geometric_witness (d : ℕ) (hd : 0 < d) {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n N H F r : ℕ) (p : Fin N → ℕ) (v : Fin n → ℝ)
      (ι : Fin N ↪o Fin n) (budget c S : ℝ),∀ hN : 0 < N,
      n ≤ m → N ≤ H → (H:ℝ) ≤ A*Real.log (B z) → m-(ι ⟨0,hN⟩).val ≤ H →
      v∈relaxedGeometricFamily m n budget c → (∀ i,v (ι i)=B (p i)) →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H:ℝ)^4 →
      (∀ i,IsNormalPrime S (p i)) → (∀ i,3 ≤ p i) → StrictAnti p →
      0 < F → F.totient=d*r.totient → r=∏ i,p i →
      (largestPrimeFactor d:ℝ) ≤ S → SquarefreeAbove F S → SquarefreeAbove F.totient S →
      (∀ q:ℕ,q.Prime → q∣F → IsNormalPrime S q) →
      largestPrimeFactor F≠p ⟨0,hN⟩ → (∀ i,(p i-1:ℕ) ≤ z) → (F.totient:ℝ) ≤ z →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.SquarefreeAbove

theorem OAI.TotientAsymptotic.ppt_regular_geometric_count line 238

Source documentation

Count an arbitrary finite subset of regular residual values using their actual chosen preimages and geometric prime lists. This form is independent of the ambient candidate family and applies to every dyadic layer of the regular suffix set.

theorem ppt_regular_geometric_count (d : ℕ) (hd : 0 < d) {A : ℝ} (hA : 0 < A) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n N H : ℕ) (budget c S : ℝ) (R : Finset ℕ)
      (F : ℕ→ℕ) (p : ℕ→Fin N→ℕ) (v : ℕ→Fin n→ℝ)
      (ι : ℕ→Fin N↪o Fin n),∀ hN : 0 < N,
      n ≤ m → N ≤ H → (H:ℝ) ≤ A*Real.log (B z) →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H:ℝ)^4 → (largestPrimeFactor d:ℝ) ≤ S →
      (∀ r∈R,m-(ι r ⟨0,hN⟩).val ≤ H) →
      (∀ r∈R,v r∈relaxedGeometricFamily m n budget c) →
      (∀ r∈R,∀ i,v r (ι r i)=B (p r i)) →
      (∀ r∈R,∀ i,IsNormalPrime S (p r i)) →
      (∀ r∈R,∀ i,3 ≤ p r i) → (∀ r∈R,StrictAnti (p r)) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.IsNormalPrime