PrimeStoppingSplit.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The first-bin identity with the actual selected divisor and its complement. The crossing test only sees the selected divisor, while inverse-binomial weighting restores every original squarefree term.

lemma OAI.CubicFirstMoment.stopping_bin_scalar_norm_le_one line 13
def OAI.CubicFirstMoment.stoppingSelected line 19
def OAI.CubicFirstMoment.stoppingRemainder line 23
lemma OAI.CubicFirstMoment.stoppingSelected_subset line 27
lemma OAI.CubicFirstMoment.stoppingSelected_surrogate line 35
lemma OAI.CubicFirstMoment.stoppingSelected_bin_count line 50
lemma OAI.CubicFirstMoment.stoppingRemainder_bin_count line 65
lemma OAI.CubicFirstMoment.stoppingSelected_bins_le line 80
lemma OAI.CubicFirstMoment.stoppingRemainder_bins_ge line 87
lemma OAI.CubicFirstMoment.stoppingSelected_earlier_prefix line 98
Source documentation
The failed first-stage test can be read entirely from the selected side at a later stopping bin. This is the extra ordinary-block predicate.
```
lemma stoppingSelected_earlier_prefix {s : Finset Eisenstein} {b : Eisenstein → ℕ}
    {j h : ℕ} (hhj : h ≤ j) {t : Finset Eisenstein} (ht : t ⊆ primeBin s b j) :
    (stoppingSelected s b j t).filter (fun p => b p < h) = primeBinPrefix s b h := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.primeBinPrefix
lemma OAI.CubicFirstMoment.cutoffMoebius_stoppingSelected line 112

theorem OAI.CubicFirstMoment.prime_bin_stopping_identity line 128

Source documentation

One original term is exactly the sum over all selections at its first stopping bin. All crossing predicates lie on the selected side.

theorem prime_bin_stopping_identity (s : Finset Eisenstein)
    (hs : ∀ p ∈ s, primaryPrime p) (b : Eisenstein → ℕ) (ell : ℕ → ℝ)
    {m : ℕ} (hb : ∀ p ∈ s, b p < m) (hell : ∀ j < m, 1 < ell j)
    {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (hend : Z ≤ R*primeSurrogate s b ell) (ψ : ℝ → ℝ) (w : ℝ) :
    ∃ j < m, ∃ k : ℕ, 1 ≤ k ∧ k ≤ (primeBin s b j).card ∧
      (∑ t ∈ (primeBin s b j).powersetCard k,
        if R*primeSurrogate (stoppingSelected s b j t) b ell/ell j < Z ∧
            Z ≤ R*primeSurrogate (stoppingSelected s b j t) b ell then
          ((primeBin s b j).card.choose k:ℂ)⁻¹ *
            (cutoffMoebius ψ w (∏ p ∈ stoppingSelected s b j t, p) *
             cutoffMoebius ψ w (∏ p ∈ stoppingRemainder s b j t, p))
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.stoppingRemainder