PPTResidualFamily.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed residual families in the PPT pruning argument. Their members are actual integers recovered from a common prime product, a small left tail, and the surviving left prime list. The counting conclusion retains both reciprocal totient weights for the subsequent prefix and suffix sums.

lemma OAI.TotientAsymptotic.ppt_squarefreeAbove_mono line 19
lemma OAI.TotientAsymptotic.ppt_squarefree_residual_target line 26
Source documentation
After excluding squares above a smaller cutoff, both the actual preimage and its target totient are squarefree at the comparison cutoff.
```
lemma ppt_squarefree_residual_target {u D : ℕ} {K S Y : ℝ}
    (hKS : K ≤ S) (hKY : K ≤ Y)
    (hu : SquarefreeAbove u K) (hφ : SquarefreeAbove u.totient K)
    (hD : D ∣ u.totient) : SquarefreeAbove u S ∧ SquarefreeAbove D Y :=
…
```
Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.SquarefreeAbove

theorem OAI.TotientAsymptotic.ppt_normalized_pair_conditions line 36

Source documentation

The literal pointwise comparison conditions for an already canceled pair follow from its arithmetic equation and normalized factor bands. The large-part condition is proved from the actual left head.

theorem ppt_normalized_pair_conditions : ∀ᶠ z : ℝ in atTop,
    ∀ (b D r : ℕ) (S : ℝ) (ν μ : ℕ → ℝ) (t : ShiftedPair b),
      ∀ hb : 0 < b,
      0 < B z → 1 < S → 0 ≤ B S → S ≤ z →
      (∀ i, IsNormalPrime S (t.left i)) →
      (∀ i, IsNormalPrime S (t.right i)) →
      (∀ i, 3 ≤ t.left i) → (∀ i, 3 ≤ t.right i) →
      (∀ i, t.left i ≠ t.right i) →
      0 < t.remainder → D*shiftedProduct t.left = t.remainder*shiftedProduct t.right →
      ((D*shiftedProduct t.left : ℕ) : ℝ) ≤ z/r →
      SquarefreeAbove (D*shiftedProduct t.left) (comparisonCutoffs z ν b) →
      (largestPrimeFactor t.remainder : ℝ) ≤ comparisonCutoffs z ν b →
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_geometric_pair_exponent line 78

Source documentation

The exponent of an already canceled pair is controlled by its actual embedding in the constructed geometric candidate family.

theorem ppt_geometric_pair_exponent {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n b H : ℕ) (budget c S e w δ : ℝ)
      (t : ShiftedPair b) (v : Fin n → ℝ) (ι : Fin b ↪o Fin n) (ν μ : ℕ → ℝ),
      ∀ hb : 0 < b,
      v ∈ relaxedGeometricFamily m n budget c → (∀ i, 3 ≤ t.left i) →
      (t.left ⟨0,hb⟩-1 : ℕ) ≤ z → (∀ i, v (ι i) = B (t.left i)) →
      1 ≤ H → b ≤ H → m-((ι ⟨0,hb⟩).val+1)+1 ≤ H →
      (H : ℝ) ≤ A*Real.log (B z) →
      0 ≤ δ → δ ≤ 2*((Real.log (B z))^5/Real.sqrt (B z)) →
      e ≤ (2*(b : ℝ)+4)*δ → w ≤ (4*(b : ℝ)+3)*δ → Real.sqrt (B S/B z) ≤ δ →
      (∀ i : Fin b, 0 < i.val → ν i ≤ B (largestPrimeFactor (t.left i-1))/B z+e) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_normal_tail_fixed_block_decay line 126

Source documentation

The published comparison bound on a fixed residual family has an arbitrary inverse-power saving, with both fixed-factor weights retained. There is no assumed estimate for the family cardinality.

theorem ppt_normal_tail_fixed_block_decay (d : ℕ) (hd : 0 < d)
    {A γ : ℝ} (hA : 0 ≤ A) (hγ : 0 < γ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (b h c a : ℕ) (W V : ℝ) (Y U : ℕ → ℝ)
      (tail : Fin h → ℕ) (T : Finset ℕ) (t : ℕ → ShiftedPair b),
      1 ≤ b → (b : ℝ) ≤ A*Real.log (B z) → (h : ℝ) ≤ A*Real.log (B z) →
      1 < W → 0 ≤ B W → W ≤ V → 1 < Y b →
      B (Y b) ≤ 2*(B z)^(2/3 : ℝ) → 0 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      a = ∏ i, tail i → Function.Injective tail →
      (∀ i, IsNormalPrime W (tail i)) →
      (∀ i, (largestPrimeFactor (tail i-1) : ℝ) ≤ V) →
      -2+(∑ j ∈ Finset.Icc 1 (b-1), TotientAsymptotic.a j*(B (Y j)/B z))+
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_geometric_residual_block_decay line 193
Source documentation
A finite late-prefix residual family has the saved comparison bound from its actual prime lists and geometric rows. The explicit arithmetic conditions are supplied after the square and nonnormal preimages have been removed. No comparison-condition or exponent conclusion is an assumption of this application theorem.
```
theorem ppt_geometric_residual_block_decay (d : ℕ) (hd : 0 < d)
    {A : ℝ} (hA : 0 < A) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m N b h H c a : ℕ) (budget g W V e w δ : ℝ) (ν μ : ℕ → ℝ)
      (tail : Fin h → ℕ) (T : Finset ℕ) (t : ℕ → ShiftedPair b),
      1 ≤ b → 1 ≤ H → b ≤ H → h ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      1 < W → 0 ≤ B W → W ≤ V → W ≤ z →
      B (comparisonCutoffs z ν b) ≤ 2*(B z)^(2/3 : ℝ) →
      0 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      a = ∏ i, tail i → Function.Injective tail →
      (∀ i, IsNormalPrime W (tail i)) →
      (∀ i, (largestPrimeFactor (tail i-1) : ℝ) ≤ V) →
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor