4 Li–Liu: two factors with a prescribed imbalance

4.1 Li–Liu’s asymmetric Goldbach theorem

The assertion is not merely that an even integer is a prime plus an almost prime. The two factors in the almost prime must have a prescribed imbalance. This chapter follows the implemented finite counts through sieving, switching, integral estimates, and the final choice of parameters. There are two implemented exits: a qualitative existence proof and a stronger counting proof using the author’s two-branch estimate for the eleventh term.

Reading this chapter with the paper.

The mathematical source is Jiamin Li and Jianya Liu, Theorem \((1+1.9)\) on the Goldbach Conjecture, arXiv:2606.05224v1. Theorem 1.1 and equation (4.4) give the public result and the distinct-prime count. Propositions 4.1–4.3 organize the finite argument; Sections 5.1–5.5 organize its analytic estimates and final assembly. The report page supplies a stage-by-stage paper/Lean correspondence ledger. This chapter and its graph are a selected mathematical exposition; the structure browser supplies the full project-module and declaration-reference views. The API provides the complete statement at each named declaration.

Three useful comparison conventions.

An exact count or identity is compared literally after its notation is fixed. An equivalent formulation carries an explicit bridge, such as the rational exponent conversion below. A replacement proof records its actual intermediate objects: the level-six lower sieve and the factor-excluded tenth fibre are examples. These distinctions preserve the authors’ weighted-sieve contribution while making the implemented route reproducible.

4.1.1 The counted object and the meaning of the exponent

For natural numbers \(N,p\), write \(\mathcal R(N,p)\) for

The final inequality is equivalent to \(r\le q^{9/10}\), with real powers on the right. Clearing the rational exponent avoids rounding and retains both factors; an unrestricted two-almost-prime predicate would be weaker.

As in the overview, define \(D_{1,19/10}(N)=\# \{ p\le N:\mathcal R(N,p)\} \). This counts distinct primes \(p\), not triples \((p,r,q)\), and \(D_{1,19/10}(N){\gt}0\) is equivalent to the existence of the displayed witnesses.

Fix \(\varepsilon {\gt}0\) and put

Every \(n\in \mathcal A\) satisfies \(n{\gt}\varepsilon N\). From now on take \(N\) sufficiently large that \(\varepsilon N{\gt}1\); then every \(n\in \mathcal A\) is at least two. This pays the domain condition before we use its least prime factor. For a real exponent \(a\) use the exact natural cutoff \(z_a=\lceil N^a\rceil \): for a prime \(\ell \), \(z_a\le \ell \) if and only if \(N^a\le \ell \). Let \(P^-(n)\) be the least prime factor of \(n\ge 2\), and let \(\Omega (n)\) count prime factors with multiplicity. The integer-valued basic weight is

Its positive values are at most one. A positive value forces \(n\) to be prime, or \(n=rq\) with prime factors and \(r{\lt}N^\tau \). For all sufficiently large \(N\), uniformly in \(a\) and \(p\),

The last implication cancels the positive integer \(r^9\); it is the arithmetic reason for the particular exponent \(9/19\) in the cutoff.

The prime case uses \(r=1\). Thus \(w_a(N-p)\le \mathbf1_{\mathcal R(N,p)}\). The map \(p\mapsto N-p\) is injective on the carrier, so summing gives

Here the threshold follows \(\varepsilon \) but precedes \(a\) and \(p\). This is an eventual theorem, not the explicit threshold printed in the paper.

4.1.2 Literal sieve fibres and the six-term decomposition

Define the finite fibre

The sieve filters the original integer \(n\), not the quotient \(n/d\). In the sums below every prime label is coprime to \(N\); repeated prime labels are permitted whenever the weak inequalities permit them. With \(A=\mathcal A\) understood, define

Buchstab’s identity partitions survivors by their smallest newly admitted prime. Apply the basic inequality at two cutoffs, expand \(S_1(y)\) down to \(z\), and split \(S_4(z)\) at \(y\). The difference of the resulting double sums supplies the positive triple term \(S_6(z,y)\). This is an exact finite partition before endpoint losses are paid. The loss is \(E=2X+Q+R+B_6\): \(X\) counts noncoprime differences, \(Q=\sum _{z\le r{\lt}y}H(A,N,r^2;r)\) counts the square diagonal, \(R\) is the triple sum with \(t{\lt}y\) and \(r=s\) or \(s=t\), and \(B_6\) is the triple sum with \(t=y\). Fix \(0{\lt}\varepsilon {\lt}2/15\). One threshold \(N_0(\varepsilon )\) works for every \(1/21{\lt}k{\lt}\sigma \le 1/3\): with \(z=N^k\), \(y=N^\sigma \), all even \(N\ge N_0\) satisfy the actual finite bound

The uniform bound \(0\le E\le 446N^{1-k}\) is proved from the four counts, not stipulated as a big-\(O\) premise.

4.1.3 The twelve terms and a factor-excluded tenth fibre

Now fix

These satisfy \(1/18{\lt}a{\lt}b{\lt}(1-3b)/3{\lt}c{\lt}1/3\). Set \(G_1=S_1(z)\), \(G_2=S_1(B)\), \(G_3=S_2(T)\), \(G_4=S_3(z,N^{1/3})\), \(G_5=S_3(z,C)\), and

For the tenth term the implementation uses

The excluded modulus is \(Nrs\): both chosen prime factors are exempted from further sifting, because the sieve acts on \(n\) itself. The following finite comparison uses this explicitly defined intermediate fibre. After removing noncoprime and square-divisible exceptional atoms, the cofactor \(q=n/(rs)\) is prime: its least prime factor is at least \(\sqrt{N/(rs)}\), while \(q{\lt}N/(rs)\). The injection preserves the pair labels and sends the surviving atom to

Let \(\Pi _{10}\) count these labelled triples. Use the six-term bound at \((k,\sigma )=(a,1/3)\) and \((b,c)\); the first \(S_4(N^{1/3})\) vanishes. Three selected triple regions inside \(S_6(z,N^{1/3})\), with a paid upper-endpoint overlap, account for the pair gains and quadruple subtractions. The remaining \(S_5(B,C)\) is covered by the corrected tenth fibre and the third triple region. Combining these inequalities and paying all finite exceptions gives the corrected twelve-term inequality actually consumed below. Fix \(0{\lt}\varepsilon {\lt}2/15\); for all sufficiently large even \(N\),

The source threshold is even uniform over exponents satisfying \(1/18{\lt}a{\lt}b{\lt}(1-3b)/3{\lt}c{\lt}1/3\); here we use the displayed fixed triple. There is also an auxiliary switched inequality: replacing \(-G_{10}^{\rm corr}-1334N^{1-a}\) by \(-\Pi _{10}-2214N^{1-a}\) preserves the conclusion. It is not the twelve-term input used by the production assembly. Neither signed left side has yet been proved positive. See corrected and switched finite bounds.

Sifting the output while retaining the labels

For output sifting, let \(\mathcal B_{10}(Z)\) keep the same \((r,s,q)\) labels and the strict cofactor window, but replace primality of \(N-rsq\) by the literal output condition

This sieves the output \(N-rsq\), not its prime cofactor \(q\); the excluded modulus here is \(N\), in contrast to \(Nrs\) in the original corrected fibre. For \(N\ge 2\), \(\varepsilon {\gt}0\), \(b{\gt}1/18\) and \(Z\ge 1\), the finite bound

pays for small prime outputs without identifying different labels. The source permits any real second cutoff \(C\); no small-epsilon window or evenness assumption is needed for this finite comparison. See literal output fibres and finite comparison. As an auxiliary error-payment observation, for fixed \(0\le \theta {\lt}1\) and \(\delta {\gt}0\), the power losses with \(1\le Z\le N^\theta \) are eventually at most \(\delta N/\log ^2N\), with the threshold preceding the varying \(Z\). The actual analytic route chooses and eliminates the auxiliary cutoff inside the bound for \(\Pi _{10}\); it does not require an entire sifted replacement of the twelve-term expression.

4.1.4 Normalization and the first positive and negative estimates

Use the author’s normalization, without an additional factor two:

Products here run over primes. The universal product is positive and bounds \(\mathfrak S_{\mathrm{Liu}}(N)\) below; in particular \(\mathcal X_N{\gt}0\) for \(N\ge 4\). Let \(\gamma \) denote Euler’s constant. The lower and upper Jurkat–Richert functions \(f,F\) have \(f(u)=0\) and \(F(u)=2e^{\gamma }/u\) for \(0{\lt}u\le 2\), and satisfy \((uf(u))'=F(u-1)\), \((uF(u))'=f(u-1)\) for \(u{\gt}2\). For the lower factor on \([4,6]\) the implementation uses explicitly

For every fixed \(\delta {\gt}0\) and \(0{\lt}\varepsilon {\lt}1\), a threshold \(N_0(\delta ,\varepsilon )\ge 4\) gives \(((1-\varepsilon )L-\delta )\mathcal X_N\le 3G_1+G_2\) for every even \(N\ge N_0\), where

The multiplicities three and one are already included in \(L\). The first factor \(f_*(6)\) uses a separate level-six lower-density producer, not the beta-cutoff theorem near \(33/8\). level-six lower density proves that, for each \(\rho {\gt}0\), the actual lower Rosser density is at least \((f_*(6)-\rho )\) times the local sieve product once \(N\) is large; this density threshold precedes \(0{\lt}\varepsilon {\lt}1\). Its real consumer, alpha normalization at level six, combines that density with the main-mass/product lower bound and the paid level-six remainder. The resulting count threshold follows the fixed \(\varepsilon \). For the second factor, continuity first selects a fixed ratio \(s{\lt}33/8\); the fixed-ratio sieve theorem is applied only afterwards. Thus the endpoint value \(f_*(33/8)\) is obtained with a paid error, not by assuming uniform validity of a sieve theorem at its limiting ratio.

In the fixed public paper, equations (5.11)–(5.13) first use \(f(53/8)\) and then its lower comparison with \(f(6)\). The implementation obtains the needed \(f(6)\) coefficient directly at natural level \(\lceil N^{4/53}\rceil ^6\). This is a replacement lower-sieve route to the retained coefficient.

For the following \(G_3,G_4,G_5\) upper bounds, fix \(\delta {\gt}0\) and \(0{\lt}\varepsilon {\lt}2/15\); each bound holds for every sufficiently large even \(N\), with its threshold following those fixed parameters. The negative term \(G_3\) is bounded above by \([8\log ((1-\tau )/\tau )+\delta ]\mathcal X_N\); its external multiplicity is four. For \(d=1/3,3/11\), put

Here \(F_S\) is the implemented Suzuki upper factor. On the required range \(53/24\le s\le 45/8\), its exact exp-free formulas are

Thus the third-interval correction is not discarded. A formula for \(F_S\) alone would not justify this use beyond four. The separate S3 upper Rosser comparison through six proves, for every \(\rho {\gt}0\), one cutoff threshold such that the actual upper Rosser main sum is at most \((F_S(s)+\rho )\) times its sieve product for every \(3/2\le s=\log \Delta /\log z\le 6\) and \(\Delta {\gt}0\). It obtains the genuine local-product witness internally from upper density through six. The proof in actual S3 normalized consumer uses this comparison at the moving finite-level ratios, then passes to the limiting integral above. This covers \(G_4,G_5\) and the entire \([53/24,45/8]\) range; the narrower upper comparison through four is not being silently extended.

The actual bounds are \(G_4\le [(1-\varepsilon )A_3(1/3)+\delta ]\mathcal X_N\) and \(G_5\le [(1-\varepsilon )A_3(c)+\delta ]\mathcal X_N\).

Switching \(G_8,G_9\) creates the labelled \(\mathcal B_8^+,\mathcal B_9^+\): \((r,s,q)\) with the respective original pair constraints, prime \(q\), and \(rsq{\lt}N\); their output is \(N-rsq\). Good original atoms inject into the prime-output atoms; noncoprime, square, and small-output exceptions are paid separately before upper sifting. The logarithmic prime coordinates \(u=\log r/\log N\), \(v=\log s/\log N\) produce the density \(K(u,v)=1/[uv(1-u-v)]\). Define the fixed integrals

The corrected tenth count first satisfies \(G_{10}^{\rm corr}\le \Pi _{10}+880N^{1-b}\) eventually. Pi10 after output sifting and cutoff elimination bounds the actual \(\Pi _{10}\) count, not \(\mathcal B_{10}(Z)\) for arbitrary \(Z\). Then corrected tenth count bounded by I10 pays the \(880N^{1-b}\) error. Precisely, for every \(\delta {\gt}0\) and every fixed \(0{\lt}\varepsilon {\lt}1\), some \(N_0(\delta ,\varepsilon )\ge 4\) gives

To see the actual signed consumption, put

The corrected twelve-term input reads \(\mathcal T_{11}-(G_{10}^{\rm corr}+1334N^{1-a})\le 4D_{1,19/10}(N)\). For fixed \(\delta {\gt}0\) and \(0{\lt}\varepsilon {\lt}2/15\), use the preceding bound with loss \(\delta /2\) and pay \(1334N^{1-a}\le (\delta /2)\mathcal X_N\). Because the subtracted cost is at most \([8(1-\varepsilon )I_{10}+\delta ]\mathcal X_N\), this gives

For comparison, Proposition 4.3 in the fixed public paper writes the excluded prime set as \(\mathscr P(Nr)\) in its tenth term. The present \(G_{10}^{\rm corr}\) explicitly uses \(Nrs\) while sifting the original integer. The proved corrected inequality and the following consumption bridge establish this implementation’s route; an equality with the printed tenth fibre is a separate comparison question. This is exactly the input of the subsequent count ledger: corrected twelve-term I10 consumer. Its threshold follows \(\delta ,\varepsilon \) but is uniform in \(1/18{\lt}a{\lt}b\) with \(b=4/33,c=3/11\) fixed. The resulting upper coefficients are \(8I_8\) for \(G_8\) and \(8(1-\varepsilon )I_{10}\) for the tenth-term cost after output sifting and cutoff elimination. The external factor two makes the total eighth-term cost \(16I_8\). The standard inputs are actual prime-progression remainder bounds, Rosser upper/lower sieves, Euler-product normalization, and logarithmic prime-sum limits; they are applied to these carriers, not supplied as hypotheses on \(D_{19}\). With \(R_5=G_6+G_7-G_9-G_{11}-G_{12}\), the retained endpoint certificates and continuity at \(\varepsilon =0\) give the following local contract: for every \(\delta {\gt}0\), there is \(\varepsilon _0\in (0,2/15]\) such that, for each fixed \(0{\lt}\varepsilon {\lt}\varepsilon _0\), some \(N_0(\delta ,\varepsilon )\ge 4\) works for every even \(N\ge N_0\) in

Indeed \(c_0\le L-32\log (10/9)-A_3(1/3)-A_3(c)-8I_{10}-16I_8\). The retained bounds are \(A_3(1/3)\le 236056871187/10^{10}\), \(A_3(c)\le 195190815363/10^{10}\), \(8I_{10}\le 540995781/10^8\), and \(8I_8\le 60961168/10^8\).

4.1.5 The ninth term and the positive pair integrals

Split the original \(G_9\) labels by \(r{\lt}N^{1/10}\) and \(r\ge N^{1/10}\). The strict-low and closed-high pieces partition the entire count. For every fixed \(\delta {\gt}0\) and \(0{\lt}\varepsilon {\lt}2/15\), the low Fouvry route and the ordinary high route give, for all sufficiently large even \(N\) (with \(N_0\ge 4\) depending on these fixed parameters),

There are two inner integrals, both for \(a\le u\le 1/3\):

Thus the low single-integral kernel retains the extra \(1/(1-u)\); only the high piece uses the first identity without that extra factor. See weighted and unweighted G9 reductions. Primitive and rational logarithm bounds certify \(C_9\le 527231/100000\).

For the positive pair terms define

The lower Rosser sums retain \(1/\varphi (rs)\) even on the square diagonal. Passing to \(1/(rs)\) is a one-sided comparison, not an equality. Symmetry gives the half-square integral for \(G_6\); \(G_7\) gives the rectangle. Truncation by \(\eta \) costs at most \(\eta \) times their logarithmic masses. After paying the prime-progression remainder, the actual result has this order of choices: for every \(\delta {\gt}0\), first choose \(\varepsilon _0\in (0,2/15]\); for each fixed \(0{\lt}\varepsilon {\lt}\varepsilon _0\), choose \(N_0(\delta ,\varepsilon )\ge 4\). Then every even \(N\ge N_0\) satisfies \(G_6+G_7\ge (C_{67}-\delta )\mathcal X_N\). The small epsilon window absorbs the source-mass loss; increasing \(N\) alone would not remove it for an arbitrary fixed epsilon. See actual pair lower bound and its epsilon window.

For certification the source moves to \(s=u+v\) and the elementary lower profile

The denominator and logarithm argument are positive throughout this actual sum-coordinate domain. Set \(d_*=1/2-2a\); the profile vanishes on \([d_*,b+c]\). The square splits at \(a+b\), and the rectangle at \(2b,a+c\). Define the five fixed integrals, including the half-square multiplicity, by

This is exactly the source’s five-branch elementary integral, not a renaming of \(C_{67}\): elementary profile and its domain, five fixed branches and actual pair comparison. Five centered polynomial integrations, with total loss \(21/4240000\), certify

The second inequality is a proved elementary-to-actual integral comparison; it is this inequality that will also enter the older ledger. No floating-point quadrature value is used as a premise.

4.1.6 The original eleventh-term domain and the cross term

The four logarithmic variables for \(G_{11}\) satisfy \(a\le u\le v\le w\le t\le b\). For a literal label \((r,q,s,t)\), the actual cofactor \(m\) lies in the strict window \(\varepsilon N/(rqst){\lt}m{\lt}N/(rqst)\). After the exceptional atoms are paid, the rough-cofactor comparison uses the second prime \(q\) as its sieve cutoff. The upper-bound proof enlarges this window to the full rough mother up to \(x=N/(rqst)\), discarding its positive lower endpoint. It is the upper endpoint of this mother count that has Buchstab parameter

This is not the parameter \(\log m/\log q\) of each actual cofactor; that parameter is not equal to the displayed endpoint ratio. The enlargement is also why no factor \(1-\varepsilon \) survives in the \(G_{11}\) coefficient, unlike the window-sensitive tenth-term bound. See full rough mother and loss of the window factor and canonical upper-endpoint geometry. Write \(\omega _{\mathrm B}\) for Buchstab’s function, with \(u\omega _{\mathrm B}(u)=1\) on \([1,2]\) and \((u\omega _{\mathrm B}(u))'=\omega _{\mathrm B}(u-1)\) for \(u{\gt}2\). Its proved bound on this interval is \(W=561522/10^6\). Here take \(N\ge 4\) with \(N^a\ge 4\). A used cell has ratio \(1{\lt}\rho \le 5/4\) and first lower endpoint \(\rho ^j\); the finite level comparison imposes no separate restriction on \(\varepsilon \) beyond membership in the source’s used-cell set. For a fixed level loss \(0\le \eta {\lt}1/4\), its actual level is

The buffered low cell and the ordinary high cell both give the required bound for every short prime \(p\) in that cell. The associated limiting exponent is \(\lambda (u)=(5/9)(1-\min \{ u,1/10\} )\). Consequently the upper-sieve weight is

This weight is derived at every short prime in each grid cell from the buffered low level and the ordinary high level; it is not a replacement of an already paid scalar eight by a smaller number.

Define \(I_{11}(h)\) by integrating \(h(u)/(uv^2wt)\) over the ordered domain. This is exactly the author’s two integrals: split the first coordinate at \(1/10\), retain \(u\le v\le w\le t\le b\), and retain \(v^2\) in the denominator. The source’s nested label is \((t,w,u,v)\), which explains the coordinate order in the finite kernel. Integrating the last three variables gives

Thus \(I_{11}(h)=\frac{36}{5}\int _a^{1/10}K_{11}(u)/(1-u)\, du +8\int _{1/10}^bK_{11}(u)\, du\), the original-domain match needed here.

A finite geometric majorant for \(1/(1-u)\), exact primitives, and certified bounds for \(\log (53/33)\) and \(\log (40/33)\) prove \(W I_{11}(h)\le 10191/100000\).

The actual-count producer also pays for the switched exceptional atoms, both distribution remainders, grid ordering collars, and newly admitted prime divisors of \(N\). With mesh \(\rho =1+t\), it uses the bounded weight \(h+t\le 9\); the collar costs \(O(t)\) and the divisor tail is bounded by \(16800\cdot 9\log N/N^a\) on the normalized mother scale. Continuity first chooses \(0{\lt}t\le 1/8\) to fit the requested loss, then one maximum of the thresholds pays this tail and the \(5N/\log ^3N\) error. Only after these steps does it conclude: for every fixed \(\delta {\gt}0\) and \(0{\lt}\varepsilon \le 1\), there exists \(N_0(\delta ,\varepsilon )\ge 4\) such that every even \(N\ge N_0\) satisfies \(G_{11}\le (10191/100000+\delta )\mathcal X_N\). This is a fixed-epsilon result, not one requiring epsilon to shrink with delta.

For \(G_{12}\) the original domain is \(a\le u\le v\le w\le b\), with the fourth coordinate independently in \(b\le t\le c\). At the full rough upper endpoint \(x=N/(rqst)\), its Buchstab parameter is still \(\log x/\log q=(1-u-v-w-t)/v\). The cross domain guarantees this ratio is at least three; on the strict low branch \(u{\lt}1/10\), the improved lower bound is \(79/25\). The two constants are pointwise majorants of the actual Buchstab function:

They have no upper cutoff. The geometric implication and their use at actual labels are proved in cross-domain Buchstab geometry; the pointwise analytic bounds are in two Buchstab majorants. Thus these constants enter before integration, rather than being outputs of a quadrature calculation. Put \(h_{12}(u)=h(u)\, 561990/10^6\) for \(u{\lt}1/10\), and \(h_{12}(u)=h(u)\, 564383/10^6\) for \(u\ge 1/10\), and define

The original quadruple count passes through rough cofactors and product-prime output fibres. Both exception payments are retained; a clipped low/high grid then gives the actual contract: for every fixed \(\delta {\gt}0\) and \(0{\lt}\varepsilon \le 2/15\), some \(N_0(\delta ,\varepsilon )\ge 4\) works for all even \(N\ge N_0\) in \(G_{12}\le (C_{12}+\delta )\mathcal X_N\). The low branch remains strict and the high branch includes \(u=1/10\); no boundary labels or exception payments are dropped.

A rational envelope, integration by primitives, and endpoint logarithm bounds certify \(C_{12}\le 66821/100000\) on this cross domain.

4.1.7 One common error budget and the two completed exits

First substitute the \(G_9\) and actual author-\(G_{11}\) upper bounds into \(R_5\), allocating thirds of a requested loss to the three input estimates. Here, too, the local contract is: for every \(\delta {\gt}0\), first choose \(\varepsilon _0\in (0,2/15]\); for each fixed \(0{\lt}\varepsilon {\lt}\varepsilon _0\), choose \(N_0(\delta ,\varepsilon )\ge 4\). Then every even \(N\ge N_0\) satisfies

Next substitute the original pair lower bound and cross upper bound. The scalar certificates give exactly

For every \(\delta {\gt}0\) the implementation proves \(\exists \varepsilon _0\in (0,2/15]\), \(\forall \varepsilon \in (0,\varepsilon _0)\), \(\exists N_0\ge 4\), \(\forall N\ge N_0\) even: \((m_{\rm author}-\delta )\mathcal X_N\le 4D_{1,19/10}(N)\). It takes minima of the epsilon windows and maxima of all natural thresholds. There is no threshold asserted uniformly over all small positive epsilon.

Fix any real \(\kappa {\lt}515093/800000000\) before choosing the threshold. Take \(\delta =m_{\rm author}-4\kappa {\gt}0\), then \(\varepsilon =\varepsilon _0/2\). The result is \(\exists K\ge 4\), \(\forall N\ge K\) even: \(\kappa \mathcal X_N\le D_{1,19/10}(N)\). The ceiling itself is not asserted.

Choosing \(\kappa =1/2000\) and using \(\mathcal X_N{\gt}0\) gives the strict paper bound \(D_{1,19/10}(N){\gt}(1/2500)\mathcal X_N=0.0004\mathcal X_N\), not merely a weak inequality.

The qualitative existence route remains separate. It uses the coarser actual \(G_{11}\) coefficient \(10385101/10^8\) and the five-branch \(J_{\rm elem}\) defined above. Its margin is the integral expression

The rational number is a certified lower bound, not the definition of \(m_{\rm old}\). In particular \(C_{67}\) has not merely been renamed. The old route has its own actual-count ledger: for every \(\delta {\gt}0\), there exists \(\varepsilon _0\in (0,2/15]\) such that, for each fixed \(0{\lt}\varepsilon {\lt}\varepsilon _0\), there exists \(N_0(\delta ,\varepsilon )\ge 4\) for which

The proof substitutes \(4J_{\rm elem}\le C_{67}\) into the older actual cross-integral ledger, keeping its coarser eleventh-term cost; see old margin definition and actual-count ledger. Its scalar positivity and independent witness exit are in old certified margin and existence theorem. Its own certified quantitative ceiling is \(126891/800000000\), not the author-route ceiling.

Taking \(\delta =m_{\rm old}/2\), then \(\varepsilon =\varepsilon _0/2\), proves \(D_{1,19/10}(N){\gt}0\) and extracts the natural-power witnesses. The source-exponent bridge finally gives \(r\le q^{(19/10)-1}\). This is the actual implementation of the unconditional existence theorem; it need not be rerouted through the stronger counting theorem.

4.1.8 Four public interfaces for the two exits

Import Goldbach.OnePlusOneNine. The public natural-power and real-exponent interfaces expose the earlier-margin existence route:

The author-\(G_{11}\) ledger supplies the strict paper count and the stronger fixed-coefficient family:

These public types have no distribution, integral-estimate or positivity premise. Their standard logical foundation is checked separately from their mathematical statement by the acceptance probes described in the verification guide. The paper’s twin-prime Theorem 1.2 and its \(\mathrm{WEH}(0.999)\)-conditional Theorems 1.3–1.4 have their own mathematical contracts; the four interfaces here concern the unconditional Goldbach result.