noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowMotherMass (N : ℕ) (ε : ℝ) : ℝ

The physical low mother, before ANY output-primality condition.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowMotherMass N ε = ∑ p ∈ G12FlexibleRectangle.mother N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight N p.2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowSourceMass (N : ℕ) (ε : ℝ) : ℝ

This source low window is ungated, unlike the physical mother.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowSourceMass N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ∑ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m with ↑r < ↑N ^ (1 / 10), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight N r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowMother_le_source (N : ℕ) (ε : ℝ) : goldbachG12AuthorLowMotherMass N ε ≤ goldbachG12AuthorLowSourceMass N ε

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight_eq_high {N r : ℕ} (hN : 4 ≤ N) (_hr : Nat.Prime r) (hcut : ↑N ^ (1 / 10) ≤ ↑r) : goldbachG12AuthorPrimeWeight N r = 8

The closed high cutoff maps to the high branch, including equality.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorSource_split {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : goldbachG12WeightedSource N ε (goldbachG12AuthorPrimeWeight N) = goldbachG12AuthorLowSourceMass N ε + 8 * G12ClippedWindow.highMass N ε

Exact author source split. High mass is the ORIGINAL UNGATED source window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowHigh_le_source {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : goldbachG12AuthorLowMotherMass N ε + 8 * G12ClippedWindow.highMass N ε ≤ goldbachG12WeightedSource N ε (goldbachG12AuthorPrimeWeight N)

The physical low plus the original UNGATED high is bounded by the same weighted source. No product value is treated as a unique body label.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowHigh_integral_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), Real.log ↑N / ↑N * (400 * (goldbachG12AuthorLowMotherMass N ε + 8 * G12ClippedWindow.highMass N ε)) ≤ 564383 / 1000000 * goldbachG12PrimeIntegral goldbachG11AuthorWeight + δ

Actual low physical weighted mother plus ungated high mass; the cutoff is uniform in every later epsilon. This is a raw-mother, ONE-logarithm bound.