theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight_eq_low_mother {N : ℕ} (hN : 4 ≤ N) {ε : ℝ} {p : ℕ × ℕ} (hp : p ∈ G12FlexibleRectangle.mother N ε) : goldbachG12AuthorPrimeWeight N p.2 = 36 / (5 * (1 - Real.log ↑p.2 / Real.log ↑N))

The author's rational low branch on every literal low-mother atom.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowMotherMass_eq_rational {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : goldbachG12AuthorLowMotherMass N ε = ∑ p ∈ G12FlexibleRectangle.mother N ε, goldbachG12NormalizedCoefficient N p.1 * (36 / (5 * (1 - Real.log ↑p.2 / Real.log ↑N)))

Expanded finite mother mass; no output-primality predicate was inserted.