SelectedPrimeCanonical.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the selected-bin largest-prime role. The largest prime of the full product is used throughout; its occurrence in the selected divisor is proved equivalent to the free-prime row test.

lemma OAI.CubicFirstMoment.primaryPrimeFactors_mul_union line 14
lemma OAI.CubicFirstMoment.largestPrimeChoice_dvd_right_iff line 28
lemma OAI.CubicFirstMoment.selected_largest_free_prime_iff line 48

theorem OAI.CubicFirstMoment.selected_largest_sum_reindex line 75

Source documentation

Reindexing the selected-bin role retains the original divisor support and introduces exactly the full-complement largest-prime test.

theorem selected_largest_sum_reindex (r : Eisenstein) (hr : primary r)
    (D : Finset Eisenstein) (B : ℝ)
    (hD : ∀ d ∈ D, primary d ∧ Squarefree (r*d) ∧ norm d ≤ B)
    (hne : ∀ d ∈ D, (primaryPrimeFactors d).Nonempty)
    (F : Eisenstein → ℂ) :
    (∑ d ∈ D, if largestPrimeChoice (r*d) ∣ d then F d else 0) =
      ∑ t ∈ ((primeCutoff B) ×ˢ (primaryElementBall B)).filter
        (fun t => t.1*t.2 ∈ D ∧ ¬t.1 ∣ t.2 ∧
          largestPrimePredicate primeTieCode (primaryPrimeFactors t.2) t.1),
        if largestPrimePredicate primeTieCode (primaryPrimeFactors (r*t.2)) t.1
          then F (t.1*t.2) else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.largestPrimeChoice, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.largestPrimePredicate, OAI.CubicFirstMoment.primeTieCode