noncomputable def G12LowHighOutput.globalLinkedAtoms (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

The physical original carrier, with the original coprimality and strict product endpoint. No output primality is assumed in this carrier.

Equations

• G12LowHighOutput.globalLinkedAtoms N ε = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ×ˢ Finset.range (N + 1) | Nat.Prime p.2 ∧ p.2.Coprime N ∧ ↑N ^ (4 / 53) < ↑p.2 ∧ p.2 ≤ p.1.minFac ∧ ε * ↑N < ↑p.2 * ↑p.1 ∧ p.2 * p.1 < N}

noncomputable def G12LowHighOutput.low (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

Equations

• G12LowHighOutput.low N ε = {p ∈ G12LowHighOutput.globalLinkedAtoms N ε | ↑p.2 < ↑N ^ (1 / 10)}

noncomputable def G12LowHighOutput.high (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

Equations

• G12LowHighOutput.high N ε = {p ∈ G12LowHighOutput.globalLinkedAtoms N ε | ↑N ^ (1 / 10) ≤ ↑p.2}

noncomputable def G12LowHighOutput.outputCount (N : ℕ) (S : Finset (ℕ × ℕ)) : ℝ

Equations

• G12LowHighOutput.outputCount N S = 400 * ∑ p ∈ S, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12LowHighOutput.low_eq_mother (N : ℕ) (ε : ℝ) : low N ε = G12LowRectangle.mother N ε

theorem G12LowHighOutput.partition (N : ℕ) (ε : ℝ) : Disjoint (low N ε) (high N ε) ∧ low N ε ∪ high N ε = globalLinkedAtoms N ε

theorem G12LowHighOutput.boundary_in_high (N : ℕ) (ε : ℝ) (p : ℕ × ℕ) (hp : p ∈ globalLinkedAtoms N ε) (he : ↑p.2 = ↑N ^ (1 / 10)) : p ∈ high N ε ∧ p ∉ low N ε

theorem G12LowHighOutput.weighted_partition (N : ℕ) (ε : ℝ) (f : ℕ × ℕ → ℝ) : 400 * ∑ p ∈ globalLinkedAtoms N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p = 400 * ∑ p ∈ low N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p + 400 * ∑ p ∈ high N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

Exact real weighted splitting, without subtracting inequalities.

theorem G12LowHighOutput.output_partition (N : ℕ) (ε : ℝ) : outputCount N (globalLinkedAtoms N ε) = outputCount N (low N ε) + outputCount N (high N ε)

theorem G12LowHighOutput.original_low_count (N : ℕ) (ε : ℝ) : outputCount N (low N ε) = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m) * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | ↑r < ↑N ^ (1 / 10)}.card

The low summand consumes the established original-fibre identity literally.

theorem G12LowHighOutput.global_output_iff (N m r : ℕ) (ε : ℝ) : (m, r) ∈ globalLinkedAtoms N ε ∧ Nat.Prime (N - r * m) ↔ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m

The physical carrier has exactly the original output-prime fibres.

theorem G12LowHighOutput.original_filtered_count (N : ℕ) (ε : ℝ) (P : ℕ → Prop) [DecidablePred P] : outputCount N ({p ∈ globalLinkedAtoms N ε | P p.2}) = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m) * ↑(Finset.filter P (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m)).card

An exact finite identity for any first-prime test. This is not a Siegel--Walfisz inheritance assertion for arbitrary filters.

theorem G12LowHighOutput.original_high_count (N : ℕ) (ε : ℝ) : outputCount N (high N ε) = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m) * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | ↑N ^ (1 / 10) ≤ ↑r}.card

theorem G12LowHighOutput.original_total_partition (N : ℕ) (ε : ℝ) (hN : 2 ≤ N) : ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) = outputCount N (low N ε) + outputCount N (high N ε)

Exact splitting of the original integer G12 total, with coefficient/400 normalization restored on both physical output-prime summands.

noncomputable def G12LowHighOutput.sourceLow (N : ℕ) (ε : ℝ) : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom

The ungated distribution carrier is kept separate from the original coprime-gated physical output carrier.

Equations

• G12LowHighOutput.sourceLow N ε = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε | ↑p.snd < ↑N ^ (1 / 10)}

noncomputable def G12LowHighOutput.sourceHigh (N : ℕ) (ε : ℝ) : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom

Equations

• G12LowHighOutput.sourceHigh N ε = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε | ↑N ^ (1 / 10) ≤ ↑p.snd}

theorem G12LowHighOutput.source_partition (N : ℕ) (ε : ℝ) : Disjoint (sourceLow N ε) (sourceHigh N ε) ∧ sourceLow N ε ∪ sourceHigh N ε = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε

theorem G12LowHighOutput.source_weighted_partition (N : ℕ) (ε : ℝ) (f : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom → ℝ) : 400 * ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.fst * f p = 400 * ∑ p ∈ sourceLow N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.fst * f p + 400 * ∑ p ∈ sourceHigh N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.fst * f p

The original distribution atoms themselves split exactly for every real weight test; this does not claim that a distribution bound splits.