PPTResidualComparison.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Pointwise comparison data for a residual PPT collision. The prime lists and shifted-product equation are the actual residual ones. Cancellation preserves that equation, normality supplies the paired-coordinate error, and the geometric candidate row supplies the strict comparison exponent. The squarefree target and the small integer residual remain explicit arithmetic hypotheses; no counting conclusion is assumed here.

lemma OAI.TotientAsymptotic.ppt_normalized_factor_interval line 23

theorem OAI.TotientAsymptotic.ppt_canceled_normalized_conditions line 41

Source documentation

Normalized intervals of the actual largest predecessor factors give the literal published comparison conditions after matching cancellation.

theorem ppt_canceled_normalized_conditions : ∀ᶠ z : ℝ in atTop,
    ∀ (k D E : ℕ) (p q : Fin k → ℕ) (S : ℝ) (ν μ : ℕ → ℝ),
      ∀ hk : 0 < k,
      0 < B z → 1 < S → 0 ≤ B S → S ≤ z →
      (∀ i, IsNormalPrime S (p i)) → (∀ i, IsNormalPrime S (q i)) →
      (∀ i, 3 ≤ p i) → (∀ i, 3 ≤ q i) →
      Function.Injective p → p ⟨0,hk⟩ ≠ q ⟨0,hk⟩ →
      0 < E → D*shiftedProduct p = E*shiftedProduct q →
      ((D*shiftedProduct p : ℕ) : ℝ) ≤ z →
      SquarefreeAbove (D*shiftedProduct p)
        (comparisonCutoffs z ν (pptUnequalCoordinates p q).card) →
      (largestPrimeFactor E : ℝ) ≤
…

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

theorem OAI.TotientAsymptotic.ppt_canceled_normalized_alignment line 87

Source documentation

Apply normality to the canceled lists themselves. Thus the error uses the surviving index, rather than its possibly larger original index.

theorem ppt_canceled_normalized_alignment {k D E : ℕ}
    (p q : Fin k → ℕ) {S z : ℝ}
    (hS : 1 < S) (hBS : 0 ≤ B S) (hB : 0 < B z) (hSz : S ≤ z)
    (hD : D ≠ 0) (hE : E ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (hpa : StrictAnti p) (hqa : StrictAnti q)
    (heq : D*shiftedProduct p = E*shiftedProduct q)
    (hp3 : ∀ i, 3 ≤ p i) (hq3 : ∀ i, 3 ≤ q i)
    (hpz : ∀ i, (p i-1 : ℕ) ≤ z) (hqz : ∀ i, (q i-1 : ℕ) ≤ z)
    (hDS : ∀ i : Fin (pptUnequalCoordinates p q).card,
      (largestPrimeFactor D : ℝ) ≤
        min ((p (pptCoordinateEmbedding p q i)-1 : ℕ) : ℝ)
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.pptUnequalCoordinates, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.pptCoordinateEmbedding

theorem OAI.TotientAsymptotic.ppt_local_alignment_in_paired_mesh line 122

Source documentation

The proved local normality height bound absorbs both terms of the actual alignment estimate in the doubled paired-grid mesh.

theorem ppt_local_alignment_in_paired_mesh {A : ℝ} (hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (h i : ℕ) (S u v : ℝ),
      (h : ℝ) ≤ A*Real.log t → 0 ≤ B S → B S ≤ (h : ℝ)^4 →
      |u-v| ≤ (2*(i : ℝ)+1)*Real.sqrt (B S/t)+Real.log (3*t)/t →
      |u-v| ≤ (2*(i : ℝ)+1)*(2*((Real.log t)^5/Real.sqrt t)) := by
…

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

lemma OAI.TotientAsymptotic.ppt_paired_grid_row_errors line 142
Source documentation
The actual paired label supplies both errors used by the row estimate, with one common bound. These are conclusions about the grid, not additional hypotheses on its rounded coordinates.
```
lemma ppt_paired_grid_row_errors {b : ℕ} {δ ζ θ : ℝ}
    (hδ : 0 < δ) (u v : Fin b → ℝ)
    (hu : ∀ i, 0 ≤ u i) (hv : ∀ i, 0 ≤ v i)
    (halign : ∀ i, |u i-v i| ≤ (2*(i.val : ℝ)+1)*δ) :
    let label := fun i => collisionGridIndex δ (u i) (v i)
…
```
Mentions: OAI.TotientAsymptotic.collisionGridIndex
lemma OAI.TotientAsymptotic.ppt_residual_inverse_log_saving line 166
Source documentation
Convert the concrete inverse-cube margin to the fixed inverse-log-cube saving used by the comparison-block sum.
```
lemma ppt_residual_inverse_log_saving {A t : ℝ} {H r : ℕ}
    (_hA : 0 < A) (_ht : 0 < Real.log t)
    (hrH : r+1 ≤ H) (hdim : (H : ℝ) ≤ A*Real.log t) :
    1/(80*A^3)/(Real.log t)^3 ≤ rowContractionError r/16 := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.rowContractionError

theorem OAI.TotientAsymptotic.ppt_local_residual_exponent line 185

Source documentation

On a late residual row, the actual candidate coordinates bound the rounded largest-factor coordinates. The fixed endpoint error and every mesh contribution are absorbed uniformly in the logarithmic local length.

theorem ppt_local_residual_exponent {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n k H : ℕ) (budget c S e w δ : ℝ)
      (p q : Fin k → ℕ) (v : Fin n → ℝ)
      (ι : Fin (pptUnequalCoordinates p q).card ↪o Fin n)
      (ν μ : ℕ → ℝ),
      ∀ hk : 0 < k, ∀ hb : 0 < (pptUnequalCoordinates p q).card,
      v ∈ relaxedGeometricFamily m n budget c →
      p ⟨0,hk⟩ ≠ q ⟨0,hk⟩ → (∀ i, 3 ≤ p i) →
      (p ⟨0,hk⟩-1 : ℕ) ≤ z →
      (∀ i, v (ι i) = B (p (pptCoordinateEmbedding p q i))) →
      1 ≤ H → (pptUnequalCoordinates p q).card ≤ H →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.pptUnequalCoordinates, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptCoordinateEmbedding