PPTTruncatedCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Preserve the actual terminal-prefix coordinates through cancellation.

lemma OAI.TotientAsymptotic.ppt_canceled_prefix_coordinates line 16
Source documentation
The two surviving lists use the same retained original index. In particular all terminal-cutoff inequalities pass to both lists directly.
```
lemma ppt_canceled_prefix_coordinates {k l J E : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hJp : J ≤ k) (hJq : J ≤ l) :
    let P := pptPrimePrefix p hJp
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.pptPrimePrefix
lemma OAI.TotientAsymptotic.ppt_canceled_prefix_terminal_bounds line 27

lemma OAI.TotientAsymptotic.ppt_canceled_prefix_factor_le_tail line 50

Source documentation

The common canceled factor contains no leading prime. Its size is bounded by the actual nonleading prime product, before any asymptotic estimate.

lemma ppt_canceled_prefix_factor_le_tail {k l J : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hJp : J ≤ k) (hJq : J ≤ l)
    (hJ : 0 < J) (hp : ∀ i, 1 ≤ p i)
    (hfirst : p ⟨0,hJ.trans_le hJp⟩ ≠ q ⟨0,hJ.trans_le hJq⟩) :
    pptCanceledPrimeProduct (pptPrimePrefix p hJp) (pptPrimePrefix q hJq) ≤ 
      ∏ i ∈ Finset.univ.filter (fun i : Fin k => 0 < i.val), p i := by
…

Mentions: OAI.TotientAsymptotic.pptCanceledPrimeProduct, OAI.TotientAsymptotic.pptPrimePrefix

lemma OAI.TotientAsymptotic.ppt_canceled_prefix_geometric_embedding line 84
Source documentation
The canceled prefix inherits the actual geometric row through one explicit order embedding into the original candidate coordinate vector.
```
lemma ppt_canceled_prefix_geometric_embedding {n k l J E : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hJp : J ≤ k) (hJq : J ≤ l)
    (ι : Fin k ↪o Fin n) (v : Fin n → ℝ)
    (hcoords : ∀ i, v (ι i) = B (p i)) :
    let P := pptPrimePrefix p hJp
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.pptPrimePrefix

theorem OAI.TotientAsymptotic.ppt_regular_preimage_terminal line 101

Source documentation

Choose the finite terminal-window label and the actual unequal-list preimage prefix together. This is applied to a regular chosen preimage; it does not posit an alternative factorization or a comparison count.

theorem ppt_regular_preimage_terminal {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (N H d F : ℕ) (p : Fin N → ℕ) (S : ℝ), ∀ hN : 0 < N,
      0 < d → 0 < F → N ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      2 ≤ S → 0 ≤ B S → B S ≤ (H : ℝ)^4 →
      (∀ i, IsNormalPrime S (p i)) → (∀ i, 3 ≤ p i) → StrictAnti p →
      F.totient = d*(∏ i, p i).totient → (largestPrimeFactor d : ℝ) ≤ S →
      SquarefreeAbove F S →
      (∀ q : ℕ, q.Prime → q ∣ F → IsNormalPrime S q) →
      largestPrimeFactor F ≠ p ⟨0,hN⟩ →
      (∀ i, (p i-1 : ℕ) ≤ z) → (F.totient : ℝ) ≤ z →
      2*(B z)^(2/3 : ℝ) < B (p ⟨0,hN⟩) →
…

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