theorem G12RectangleWF.sieve_totalMass (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) : (sieve N hEven ε Z M T).totalMass = mass N ε M T

The output pushforward has exactly the physical rectangle mass.

theorem G12RectangleWF.sieve_test (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) (P : ℕ → Prop) [DecidablePred P] : ∑ n ∈ (sieve N hEven ε Z M T).support with P n, (sieve N hEven ε Z M T).weights n = ∑ p ∈ G12LowRectangle.rectangle N ε M T, if P (N - p.2 * p.1) then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0

theorem G12RectangleWF.sieve_rem (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) {d : ℕ} (hd : d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = residue N ε M T d

theorem G12RectangleWF.restricted_common_identity (N : ℕ) (ε Z : ℝ) (M T : ℕ) (c : ℕ → ℝ) : ∑ d ∈ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z).divisors, c d * residue N ε M T d = G12LowRectangle.discrepancy N (G12LowRectangle.rectangle N ε M T) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z).divisors c - gate N (G12LowRectangle.rectangle N ε M T) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z).divisors c

On its original primorial carrier the signed remainder is exactly C2 minus the explicit gcd gate, with no other correction.

theorem G12RectangleWF.smallOutput_eq_original (N : ℕ) (ε Z : ℝ) (M T : ℕ) : smallOutput N ε Z M T = 400 * ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if N - p.2 * p.1 < ⌈Z⌉₊ then 1 else 0

A literal repeated-label small-output count, not a manufactured error term.

theorem G12RectangleWF.exists_rectangle_full_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (N : ℕ), Even N → ∀ (ε Z : ℝ) (M T : ℕ), 2 ≤ Z → Z ≤ √Q → have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have V := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (d : ℕ) => (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) d) ∧ (400 * ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ (400 * mass N ε M T * V * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + 400 * ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, have c := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t; G12LowRectangle.discrepancy N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑c - gate N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑c - outsidePrimorial N ε Z Q M T ⇑c) + smallOutput N ε Z M T

The final finite output sieve and full-interval C2 bridge use one and the same constructed external family. The signed transport term is retained, not silently dropped or replaced by a squarefree mask.

theorem G12RectangleWF.family_C2_bound (A : ℕ) {Cscale ζ : ℝ} (hCscale : 1 ≤ Cscale) (hζ : 0 < ζ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℕ), 1 ≤ M → 1 ≤ T → ∀ (ν : ℝ), 4 * ↑M * ↑T = x → ζ ≤ ν → ν ≤ 1 / 10 + ζ / 10 → ↑T = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (ε η Z : ℝ) (t : List ℕ), have Q := x ^ ((5 - 5 * ν) / 9 - ζ); have c := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t; MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable c Q → |G12LowRectangle.discrepancy N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑c| ≤ x / Real.log x ^ A

The full-interval discrepancy of each actual external member consumes C2 directly. This does not assert payment of either explicit gate.