PPTHeadWitness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Original-head witnesses use the geometric tail and its actual head cap.

lemma OAI.TotientAsymptotic.ppt_large_head_doublelog line 13

theorem OAI.TotientAsymptotic.ppt_original_pair_contraction line 28

Source documentation

The cap on the constructed tail joins its internal geometric contraction to the original large head.

theorem ppt_original_pair_contraction : ∀ᶠ z : ℝ in atTop,
    ∀ (m n N H : ℕ) (p : Fin N→ℕ) (v : Fin n→ℝ)
      (ι : Fin (N-1)↪o Fin n) (budget c : ℝ),∀ hN : 0 < N,
      n ≤ m → m+1 ≤ H →
      v∈relaxedGeometricFamily m n budget c →
      (∀ i:Fin (N-1),v (ι i)=B (p ⟨i.val+1,by omega⟩)) →
      (∀ i:Fin N,0 < i.val → B (p i) ≤ (4/5:ℝ)*B z) →
      z^(9/10:ℝ) ≤ p ⟨0,hN⟩ →
      ∀ i j:Fin N,i < j → B (p j) ≤ B (p i)/(1+1/(10*(H:ℝ)^3)) := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B

theorem OAI.TotientAsymptotic.ppt_regular_head_witness line 80

Source documentation

Build an actual counted witness for the original-head branch.

theorem ppt_regular_head_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-1) ↪o Fin n) (budget c S : ℝ),∀ hN : 0 < N,
      n ≤ m → N ≤ H → (H:ℝ) ≤ A*Real.log (B z) → m+1 ≤ H → budget ≤ B z+1 →
      v∈relaxedGeometricFamily m n budget c →
      (∀ i:Fin (N-1),v (ι i)=B (p ⟨i.val+1,by omega⟩)) →
      (∀ i:Fin N,0 < i.val → B (p i) ≤ (4/5:ℝ)*B z) →
      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 →
…

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_head_count line 204

Source documentation

Count arbitrary finite sets in the original-head branch from their actual regular preimages and tail geometry.

theorem ppt_regular_head_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-1)↪o Fin n),∀ hN : 0 < N,
      n ≤ m → N ≤ H → (H:ℝ) ≤ A*Real.log (B z) → m+1 ≤ H → budget ≤ B z+1 →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H:ℝ)^4 → (largestPrimeFactor d:ℝ) ≤ S →
      (∀ r∈R,v r∈relaxedGeometricFamily m n budget c) →
      (∀ r∈R,∀ i:Fin (N-1),v r (ι r i)=B (p r ⟨i.val+1,by omega⟩)) →
      (∀ r∈R,∀ i:Fin N,0 < i.val → B (p r i) ≤ (4/5:ℝ)*B z) →
      (∀ 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