theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Mother_output_eq {N : ℕ} {e : ℝ} {a : (_ : ℕ × ℕ) × ℕ} (ha : a ∈ goldbachB9LowPositivePrefixAtoms N e) : (↑N - ↑(a.fst.2 * a.snd) * ↑a.fst.1).natAbs = goldbachPi10Output N a

Integer absolute difference equals the original natural output on the mother, not on arbitrary overhanging rectangles.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes_eq_siftingPrimes (N : ℕ) (z : ℝ) : fouvryG9SievePrimes N z = JurkatRichert1965ChenGammaOneQOne.siftingPrimes N z

Identical strict prime carriers in the original literal sieve and the new rectangles.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherSifted_eq_original (N : ℕ) (e z : ℝ) : fouvryG9MotherSifted N e (fouvryG9SievePrimes N z) = ↑(goldbachB9LowPositivePrefixSiftedCount N e z)

Exact literal-H identification, with the natural output and original labels retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherPrimeOutput_eq_original (N : ℕ) (e : ℝ) : fouvryG9MotherPrimeOutput N e = ↑(goldbachB9LowPositivePrefixPrimeAtoms N e).card

Exact prime-output count identification; no small outputs are silently removed.