Li–Liu’s (1+1.9) theorem

The mathematical structure of the formal Goldbach proof: the counted object, the analytic mechanisms, and the exact route from finite weights to the public theorems.

Jiamin Li and Jianya Liu’s weighted-sieve argument provides the mathematical starting point. The Lean development records finite carriers, uniform thresholds, paid exceptions and rational coefficient certificates.

The result and its normalization

There exists a natural K ≥ 4 such that every even natural N ≥ K has natural witnesses p,r,q with p ≤ N, p and q prime, r equal to 1 or prime, and

N = p + rq, r¹⁰ ≤ q⁹.

The last inequality is exactly equivalent to r ≤ q^9/10 over the reals. Thus the factor imbalance is part of the conclusion. The prime case is represented by r=1.

Define D19(N) as the number of distinct primes p ≤ N admitting such witnesses. Its finite carrier retains an existential pair r,q for each counted p. Write

C(N) = ∏_{ℓ>2 prime}(1 − 1/(ℓ−1)²) · ∏_{ℓ>2 prime, ℓ∣N}(ℓ−1)/(ℓ−2),
X_N = C(N)N/(log N)².

This C(N) is liuSingularSeries N. The normalization has no additional factor two. The quantitative interface proves

∃ K ∈ ℕ, K ≥ 4, ∀ N ≥ K, Even N ⇒ (1/2500)X_N < D19(N).

The stronger retained certificate gives, for each fixed real κ < 515093/800000000, a K ≥ 4 after that choice such that κX_N ≤ D19(N) for every even N ≥ K. This is a family of eventual bounds; the ceiling is excluded. Both statements have existential natural thresholds.

Mathematical proof structure

The finite counting argument, analytic estimates and final parameter choices have different responsibilities. Each stage below links to its mathematical exposition; compiled dependencies can be opened in place when a particular implication needs inspection.

Finite representations → weighted detection → sifted counts

The counting object is the set of eligible primes p, with the factor witnesses retained existentially. The finite detector connects positive weight to the constrained representation. The Buchstab decompositions keep the exact excluded prime factors and exceptional counts.

Finite weight detector · Twelve-term decomposition

Inspect dependencies

Li–Liu finite weight detector · compiled type and proof/definition references.

Inspect dependencies

Li–Liu twelve-term decomposition · compiled type and proof/definition references.

Distribution estimates → controlled sieve remainders

Ordinary Bombieri–Vinogradov controls prime progressions. Bounded-coefficient Pan controls the changing switched convolution with its coefficient sum inside the absolute value. Fouvry's estimate controls signed well-factorable bilinear errors. Each counting application retains the coefficient, residue and parameter uniformity it needs.

The three analytic contracts · Their analytic foundations

Local densities and integral bounds → main-term coefficients

The lower density at level six supplies the positive lower-sieve contribution. Upper density through six controls the corresponding upper-sieve terms. The corrected tenth count reaches its integral bound through the proved Pi10/I10 comparison; the remaining positive and negative terms have their own domains and error payments.

Inspect dependencies

The actual lower density at level six · compiled type and proof/definition references.

Inspect dependencies

Uniform upper density through six · compiled type and proof/definition references.

Inspect dependencies

The corrected tenth count bounded by I10 · compiled type and proof/definition references.

Density, switching and integral arguments

Two retained assemblies → existence and quantitative bounds

The earlier positive-margin assembly supplies natural-power witnesses and their equivalent real-exponent form. The author-G11 assembly retains the stronger signed coefficient budget used for the strict paper count and the fixed-coefficient family. The public interfaces below keep those routes separate.

Inspect dependencies

Public existence: exact natural powers · compiled type and proof/definition references.

Inspect dependencies

Public count: the strict paper bound · compiled type and proof/definition references.

Exact interfaces and the two assemblies

Four public interfaces, two actual proof exits

Import Goldbach.OnePlusOneNine. The four declarations expose two completed routes with different retained margins.

Public declaration	Actual exit	Contract
`Goldbach.one_plus_one_nine`	Existence / earlier margin goldbach_onePlusOneNine_nat_unconditional	Natural-power witnesses: r¹⁰ ≤ q⁹. Source
`Goldbach.one_plus_one_nine_real`	Existence / earlier margin goldbach_onePlusOneNine_unconditional	The same witnesses transported to the real exponent (19/10)−1. Source
`Goldbach.one_plus_one_nine_count`	Count / author-G11 ledger goldbach_D19_gt_paper_0004	Strict paper coefficient: (1/2500)X_N < D19(N). Source
`Goldbach.one_plus_one_nine_lower_bound`	Count / author-G11 ledger goldbach_D19_author_lower_of_coefficient_lt	Every fixed real κ < 515093/800000000, then an eventual threshold. Source

Existence: the earlier positive margin

LiLiuGoldbachOneNineUnconditional proves positivity of its own integral margin, bounded below by 126891/200000000. The actual-count ledger gives D19(N)>0, then extracts natural-power witnesses. The real-exponent theorem applies the proved equivalence. These two facades retain this earlier route.

Count: the author-G11 estimate

The stronger route applies the original-count pair lower bound, G9 upper bound, author-G11 upper bound and cross-G12 upper bound before closing its signed ledger. Its exact retained coefficient on 4D19 is

54233/10000 + 124341093/200000000 − 527231/100000 − 10191/100000 − 66821/100000 = 515093/200000000.

The internal order is ∀δ>0, ∃ε₀∈(0,2/15], ∀ε∈(0,ε₀), ∃N₀≥4, ∀N≥N₀ even. For the public coefficient theorem, first fix κ, then set δ = 515093/200000000 − 4κ and choose ε=ε₀/2. No epsilon remains in the public type. For the strict paper count the proof takes κ=1/2000 and uses X_N>0.

Paper stage → Lean declaration → comparison status

The fixed source is arXiv:2606.05224v1, Theorem (1+1.9) on the Goldbach Conjecture, by Jiamin Li and Jianya Liu. The numbered references below were read in that public HTML. Lean source links are pinned to revision 5c4ecc0 .

Literal refers to a fixed counting object or displayed expression; equivalent identifies a proved notation or integral bridge; replacement records the actual finite or analytic route used. The rows identify the implemented mathematical contracts and distinguish them from broader statements of the paper.

Fixed paper stage	Lean statement and source	Correspondence and exact boundary
Theorem 1.1; (4.4)	Goldbach.one_plus_one_nine_count `Goldbach/OnePlusOneNine.lean`, lines 29-35 D19 / IsOnePlusOneNineRepresentation `MathlibNt/SieveTheory/LiLiuGoldbachOnePlusOneNineFinite.lean`, lines 30-45	Literal target, equivalent encoding The counted variable is the distinct prime p. The factor restriction is encoded by natural powers; the scale is C(N)N/log²N. The strict paper coefficient is exactly 1/2500.
Representation (1.6)	oneNine_power_iff_source_exponent `MathlibNt/SieveTheory/LiLiuGoldbachOneNineLiteralExponent.lean`, lines 7	Proved equivalence The natural inequality r¹⁰ ≤ q⁹ is equivalent to (r : ℝ) ≤ (q : ℝ)^((19/10)−1). The real facade obtains its witnesses from the natural-power existence exit.
Proposition 4.1, (4.6)	goldbachBasic_finite_le_D19 `MathlibNt/SieveTheory/LiLiuGoldbachOnePlusOneNineFinite.lean`, lines 353-361	Specialized weight; eventual replacement The four integer-valued indicators retain Ω ≥ 2 and Ω ≥ 3. A fixed ε is chosen before a common eventual threshold; the development specializes the target to a=19/10. The explicit cutoff printed in the proposition is not the public Lean contract.
Proposition 4.2, (4.8)	goldbachbig_finite_lower_bound_eventually `MathlibNt/SieveTheory/LiLiuGoldbachFiniteBudget.lean`, lines 79-99	Specialized finite bound with explicit losses The six-term sign pattern is retained. The Lean bound pays the noncoprime, square, repeated-label and boundary pieces with 446N^(1−k), uniformly in 1/21 < k < σ ≤ 1/3 after fixing 0 < ε < 2/15.
Proposition 4.3, (4.18)	goldbachG10Corrected `MathlibNt/SieveTheory/LiLiuGoldbachG10Cofactor.lean`, lines 48-59 goldbachWeight_twelve_corrected_lower_bound_eventually `MathlibNt/SieveTheory/LiLiuGoldbachWeightTwelve.lean`, lines 59-67	Modified intermediate fibre; proved replacement bound The printed tenth term excludes primes dividing Nr; the implemented corrected fibre excludes primes dividing Nrs while sifting the original integer. Its signed bound pays 1334N^(1−a). This correspondence records the implemented change of object; an equality with the printed fibre remains a separate question.
Section 5.1, (5.11)–(5.16)	goldbachS1_levelSix_lowerDensitySix `MathlibNt/SieveTheory/LiLiuGoldbachS1LowerDensitySix.lean`, lines 107-116 goldbachS1_alphaFourFiftyThree_normalized_lower `MathlibNt/SieveTheory/LiLiuGoldbachS1AlphaNormalizedLower.lean`, lines 40-46	Replacement route to the retained coefficient The paper passes from f(53/8) to f(6). Lean directly constructs the actual lower Rosser density at level ⌈N^(4/53)⌉⁶. Its density threshold precedes ε; the normalized count threshold follows fixed δ,ε. The second positive term approaches 33/8 from a fixed ratio below it.
Section 5.2: G4 and G5	goldbach_upperRosserDensity_six `MathlibNt/SieveTheory/LiLiuGoldbachUpperDensitySix.lean`, lines 202-211 goldbachS3RosserMain_upper_six `MathlibNt/SieveTheory/LiLiuGoldbachS3RosserMainUpper.lean`, lines 62-85	Modern comparison; same limiting integral role The consumed upper-density theorem is uniform on [3/2,6], with a real level Δ and natural level floor(Δ)+1. The actual S3 consumer covers the limiting [53/24,45/8] range. This review checks that range and its consumption; the paper’s entire displayed chain of sieve-function identities has not been compared line by line.
(5.30) and (5.32): G6 + G7	goldbachG11Author_reused_pair_lower `MathlibNt/SieveTheory/LiLiuGoldbachG11AuthorReusedCounts.lean`, lines 10-41 goldbachG67IntegralConstant_lower_certified `MathlibNt/SieveTheory/LiLiuGoldbachOneNineUnconditional.lean`, lines 9-18	Original-count bound; alternative scalar certificate The pair count is bounded below through the actual integral C67. The retained certificate gives C67 ≥ 54233/10000 via a five-branch elementary integral. The combined lower bound has a small ε window chosen after δ. The individual decimal evaluations of g6 and g7 are not the certificate used here.
Section 5.3: switched distribution, (5.37)	liuMainPanCoprimeIntervalMaxL_boundedAggregate_log_saving `MathlibNt/SieveTheory/LiLiuPanBoundedAggregate.lean`, lines 91-106	Source-specific distribution contract The variable coefficient–prime convolution stays inside the absolute value. Constants precede the varying bounded coefficient and interval; the upper endpoint and logarithmic lower endpoint satisfy the explicit Pan geometry. The B10 consumer pays both endpoints. This is the needed specialization, separately tracked from the full WEH(1/2) formulation of Lemma 3.1.
(5.45): the ninth coefficient	goldbachB9PaperSplitIntegral / eq_singleIntegrals `MathlibNt/SieveTheory/LiLiuGoldbachB9SplitIntegralReduction.lean`, lines 45-60 goldbachS5Closed_normalized_upper_paperSplit `MathlibNt/SieveTheory/LiLiuGoldbachS5PaperSplitUpper.lean`, lines 16-38	Literal integral; proved reduction and count consumption The low branch retains 1/[uv(1−u−v)(1−u)]; its one-variable denominator is u(1−u)². The original finite count is partitioned strict-low / closed-high, then both bounds are consumed. The Fouvry low route and the ordinary-level high route remain separate.
(5.46): the tenth integral	goldbachPi10_I10_upper `MathlibNt/SieveTheory/LiLiuGoldbachPi10IntegralUpper.lean`, lines 8-24 goldbachG10Corrected_I10_upper `MathlibNt/SieveTheory/LiLiuGoldbachG10CorrectedIntegralUpper.lean`, lines 8-23 goldbachWeight_twelve_base_I10_consumed_eventually `MathlibNt/SieveTheory/LiLiuGoldbachWeightI10Consumer.lean`, lines 24-45	Same integral domain; corrected-count replacement For fixed δ>0 and 0<ε<1, G10corr ≤ [8(1−ε)I10+δ]X_N eventually. Labelled prime outputs, the auxiliary sift cutoff and the 880N^(1−b) switching loss are paid first. In the signed consumer the additional 1334N^(1−a) is paid; no positivity of the eleven-term base is assumed.
(5.48): author G11	goldbachG11PrimeIntegral_author_split `MathlibNt/SieveTheory/LiLiuGoldbachG11PrimeKernelReduction.lean`, lines 198-206 goldbachWeightG11_le_authorIntegral_direct `MathlibNt/SieveTheory/LiLiuGoldbachG11AuthorActualProducer.lean`, lines 10-28	Original-domain correspondence; certified majorant The ordered domain a≤u≤v≤w≤t≤b and the v² denominator are retained, with the first coordinate split at 1/10. The weight is 36/[5(1−u)] below the split and 8 above it. The Buchstab constant majorizes the full rough mother at its upper endpoint; the original fixed-ε count is bounded after the exceptional atoms and distribution costs are paid.
(5.49)–(5.50): G12	goldbachG12PrimeIntegral `MathlibNt/SieveTheory/LiLiuGoldbachG12PrimeKernel.lean`, lines 18-22 G12SharpWeight.factor / weight `MathlibNt/SieveTheory/LiLiuGoldbachG12SharpWeight.lean`, lines 5-7 goldbachG11Author_reused_cross_upper `MathlibNt/SieveTheory/LiLiuGoldbachG11AuthorReusedCounts.lean`, lines 44-60	Matched cross domain and branch constants The fourth coordinate ranges independently over [b,c]. The strict-low factor is 561990/10⁶, the closed-high factor 564383/10⁶. Both original-count exception payments are supplied. The fixed paper’s full proof of the global Buchstab majorants has not been audited line by line in this report.
Section 5.5, (5.51)	goldbachWeight_authorG11_numericLedger `MathlibNt/SieveTheory/LiLiuGoldbachG11AuthorQuantitative.lean`, lines 9-42 goldbach_D19_author_lower_of_coefficient_lt / goldbach_D19_gt_paper_0004 `MathlibNt/SieveTheory/LiLiuGoldbachG11AuthorQuantitative.lean`, lines 46-76	Alternative exact retained ledger; same strict conclusion The certified rational combination is 515093/200000000 on the scale 4D19. Fix κ below a quarter of that margin, then select δ, an ε window, one ε, and the threshold. The strict paper bound is obtained using κ=1/2000 and positivity of X_N.
Sections 2–3: general analytic statements	primeC2_goldbach_rectangle_kscale `MathlibNt/AnalyticNumberTheory/LargeSieve/LiLiuFouvryKGoldbachRectangle.lean`, lines 11-22	Specific contracts checked; full source audit open Ordinary BV, bounded-coefficient Pan and the Goldbach Fouvry rectangle are distinguished below. General statements outside these consumed contracts, the other distribution lemmas, and all original proofs’ individual transformations await separate line-by-line comparison.

Three distribution inputs, three counting objects

The level of distribution is only one part of an analytic input. The position of the absolute value, the varying coefficient, and the residue uniformity determine whether a theorem can pay a particular sieve remainder.

1. Ordinary Bombieri–Vinogradov: original prime progressions

The maximal prime-AP error is centered at L_*(y)/φ(q), where L_*(y)=2/log 2+∫₂ʸdt/log t for y>1 and the totalized endpoint convention gives L_*(0)=L_*(1)=2/log 2. Its sum over q ≤ floor(N^1/2/(log N)^B) has arbitrary inverse-log saving, with a maximum over integer prefixes and reduced residues. Principal, small-conductor Siegel–Walfisz, and large-conductor Vaughan/large-sieve estimates are assembled before the original-source S1 remainder is paid.

Read the Blueprint from Prime counting, Mertens estimates, and moving products through Inside the distribution proofs. The source entry is standardBombieriVinogradov and its low-conductor producer.

2. Bounded-coefficient Pan: changing switched convolutions

The discrepancy sums f(m) times a prime-progression error over m in (A1,A2], with (m,q)=1, inside the absolute value. Given a requested saving U>0, the constants C,B,N₀ precede all N≥N₀, the interval and f, under |f|≤1, A2≤N^2/3 and (log N)^2B≤A1. Primitive low/high conductor bounds, cofactor summation and a paid principal term give the aggregate. Switched S2 and B10 consume it; B10 pays both its upper and lower prefix endpoints.

The fixed Chen convolution and the varying Li–Liu coefficient have separate contracts. Read Switched distribution is an aggregate estimate, then inspect the bounded aggregate and the two-endpoint consumer.

3. Fouvry: signed well-factorable bilinear errors

The modulus coefficient remains signed while bilinear progression masses are centered by their coprime mass divided by φ(q). The Goldbach rectangle theorem fixes divisor orders, saving, Cscale≥1 and a gap ζ>0 before the rectangle and residue vary. It uses 4MT=x, T=x^ν, ζ≤ν≤1/10+ζ/10, 0<N≤Cscale·x and level x^{(5−5ν)/9−ζ}, with a divisor-bounded long coefficient and the literal prime short coefficient coprime to N.

The exact rectangle theorem is directly consumed by G12FlexibleRectangle.rectangle_C2_bound. The low-G9 and mixed-level G11 counting routes retain their own boundary and exception payments. The low-G9 kernel keeps the extra 1/(1−u); its finite split assigns equality at N^1/10 to the high branch.

These three contracts are proved ingredients of the displayed public theorem types. An EH or WEH assumption belongs to a different conditional result.

Sources, attribution and mathematical scope

The paper’s unconditional Goldbach Theorem 1.1 is the result exposed here. Its twin-prime Theorem 1.2 and Theorems 1.3–1.4 under WEH(0.999) are distinct results of the paper. The correspondence on this page concerns its unconditional Goldbach result. The abstract describes the conditional results in Elliott–Halberstam terms; their exact theorem statements use the weighted condition.

The correspondence distinguishes displayed mathematical objects, proved equivalences, and replacement arguments. The level-six density route and the corrected tenth fibre are identified explicitly in the ledger. The production chain uses the proved corrected inequality and its Pi10/I10 bridge.

The public Lean types have no unproved distribution, integral or positivity premise. The standard logical principles propext, Classical.choice and Quot.sound are distinct from mathematical assumptions such as WEH. Type comparison, build, transitive axiom inspection and independent replay are separate checks; their procedure is documented in the verification guide.

The Blueprint develops the mathematical arguments; Lean API documentation supplies exact declarations and source navigation. Dependency panels at individual results expand the actual compiled references on demand, in the context of the counted objects and analytic contracts.

Source provenance and licensing records upstream Lean contributions, the adapted PrimeNumberTheoremAnd closure and the retained Apache-2.0 source license. Existing copyright and author notices remain applicable; mathematical attribution to Li and Liu is preserved separately from the software provenance.