﻿                   Final Modular Assembly Theorem Package
                                             Denis Saltykov

                                                May 2026


                                                 Abstract
          This package gives an alternative final assembly of the proof. Unlike the full manuscript, it
      is organized as a modular theorem-package closure: four standalone theorem packages supply
      the main technical bricks, the base B1/B3/F3/F4 source layer supplies exact decomposition
      and routing, and the final I1/G2/G1/G0H layer converts the weighted asymptotic into the
      sufficiently-large binary Goldbach statement.


Contents
1 The Modular Inputs                                                                                      1
  1.1 H4 Local Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .        2
  1.2 TNG/TC1 No Rogue Short Interval . . . . . . . . . . . . . . . . . . . . . . . . . . .               2
  1.3 GoodAWACK Finite Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .                2
  1.4 CKP/X10/X16 Analytic Package . . . . . . . . . . . . . . . . . . . . . . . . . . . . .              2

2 Base Exact Decomposition and Routing                                                                    2

3 Terminal Estimates                                                                                      3
  3.1 Edge . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      3
  3.2 LongAP/Local . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .          3
  3.3 CKP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       3
  3.4 GoodAWACK . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .           3
  3.5 LocalDiag . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       3

4 Local Main Term Assembly                                                                                4

5 Weighted Assembly                                                                                       4

6 Prime-Power Removal                                                                                     4

7 Positivity and Strong Goldbach                                                                          5

8 Output Theorem                                                                                          5

9 Status of This Assembly                                                                                 5


1    The Modular Inputs
The assembly uses four theorem packages.

                                                     1
1.1   H4 Local Algebra
The H4 package proves that all admitted local/main terms are canonical tagged О›Q -local projections
inside the original B1/F3 routing cells, that no local term is double counted, and that the finite
CRT factors reconstruct the Goldbach singular series:

                                   Mlocal (N ) = S(N )N + o(N ).                              (1.1)

1.2   TNG/TC1 No Rogue Short Interval
The TNG/TC1 package proves that every actual B1-origin TC1 coarea test reaching the Liou-
ville/Fourier input is near-global:
                                    H в‰Ґ X(log X)в€’B ,
or else is routed to Edge, LongAP/Local, CKP, LocalDiag, empty support, or a finite grammar
branch before the Liouville input is invoked. Thus the proof does not use pointwise cancellation
on arbitrary shifted short intervals.

1.3   GoodAWACK Finite Grammar
The GoodAWACK finite grammar package proves that actual terminal GoodAWACK skeletons
are generated by the finite B1/B3/F3/F4/E5-clean routing grammar. The grammar preserves the
no-untagged-rank-drop invariant and excludes untagged rank-dropping affine regrouping. Hence
the HighTC-GoodAWACK residual is empty or routed to already handled terminal classes.

1.4   CKP/X10/X16 Analytic Package
The CKP/X10/X16 package proves two analytic outputs:

                            central CKP nonzero frequencies = o(N ),

after DFI/X10 is applied to the actual two-variable CKP smooth weight, and

                               X16BRS carrier-slice estimate holds,

after reduction to the X16C Shiu/AP product-carrier estimate.


2     Base Exact Decomposition and Routing
The proof starts from the ordered von Mangoldt convolution
                                                 X
                                  RО› (N ) =                О›(n1 )О›(n2 ).                      (2.1)
                                              n1 +n2 =N
                                               n1 ,n2 в‰Ґ1

    B1 gives an exact fixed-depth typed HeathвЂ“Brown decomposition
                                                  X
                                    RО› (N ) =              cB RB (N ).                        (2.2)
                                                Bв€€BJ0


No error term is introduced in (2.2).



                                                   2
    B3/F3/F3T/F4 give an exact tagged terminal partition of every parent block:
                                                   X
                                     RB (N ) =              RB,П„ (N ).                       (2.3)
                                                 П„ в€€T (B)

The terminal classes are

                 Edge,     LongAP/Local,     CKP,       GoodAWACK,       LocalDiag.

They are disjoint at the routing-history level and exhaust all descendants. Therefore

                           RО› (N ) =REdge (N ) + RLongAP (N ) + RCKP (N )
                                                                                             (2.4)
                                    + RGoodAWACK (N ) + RLocalDiag (N ).

3     Terminal Estimates
3.1   Edge
C1A verifies that every terminal Edge input satisfies a strict C1 predicate. C1 then gives

                                        REdge (N ) = o(N ).                                  (3.1)

3.2   LongAP/Local
F3P gives the positive local-coefficient predicate for LongAP/Local atoms, and D1 expands the
resulting LongAP/local algebra into an LPI-admitted local projection:

                               RLongAP (N ) = MLongAP (N ) + o(N ).                          (3.2)

3.3   CKP
For CKP, the zero-frequency term is a canonical LPI-admitted local projection later assembled by
H4. The central nonzero-frequency terms are o(N ) by the CKP/X10/X16 analytic package, and
all noncentral CKP ranges are routed by X10ER and C1P/C1A/C1 before X10 is invoked. Hence

                                  RCKP (N ) = MCKP (N ) + o(N ).                             (3.3)

3.4   GoodAWACK
The GoodAWACK branch is split into TC1 and HighTC alternatives.
   The TC1 alternative is controlled by the TNG/TC1 package, together with the near-global
X9L/Davenport input. The BRS carrier-slice estimates used inside the TC1 chain are supplied by
the X16BRS part of the CKP/X10/X16 analytic package.
   The HighTC alternative is closed by the GoodAWACK finite grammar package. Therefore

                                     RGoodAWACK (N ) = o(N ).                                (3.4)

3.5   LocalDiag
LocalDiag terms are not error terms. They are canonical local/main terms admitted by H4. Denote
their total tagged local contribution by

                                           MLocalDiag (N ).                                  (3.5)

                                                   3
4    Local Main Term Assembly
Collect all LPI-admitted local terms assembled by H4:

                     Mlocal (N ) = MLongAP (N ) + MCKP (N ) + MLocalDiag (N ).                      (4.1)

There is no fourth local summand. Auxiliary local-looking terms created by controlled CRT ab-
sorption, fixed-divisor quotienting, or primitive local slicing are tagged refinements of one of the
three displayed classes, while endpoint and smooth-boundary localizations are C1 Edge errors.
   By the H4 local algebra package,

                                    Mlocal (N ) = S(N )N + o(N ).                                   (4.2)

    The singular series is normalized for ordered Goldbach pairs:
                                   Y pв€’1                           Y            1
                                                                                         
                    S(N ) = 2C2                ,         C2 =            1в€’                  > 0.   (4.3)
                                   p|N
                                         pв€’2                      p>2
                                                                              (p в€’ 1)2
                                   p>2


5    Weighted Assembly
Using the terminal partition and the terminal estimates,

                                     RО› (N ) = Mlocal (N ) + o(N ).                                 (5.1)

The global error budget GEB records that the terminal o(N ) terms remain o(N ) after the finite
and polylogarithmic terminal summations, including Edge savings, CKP derivative losses, TC1
Davenport/AP losses, X16BRS carrier-slice losses, and local boundary terms.
   Combining (5.1) with the H4 local algebra identity gives I1:

                                      RО› (N ) = S(N )N + o(N ).                                     (5.2)


6    Prime-Power Removal
Define the genuine prime-prime weighted sum
                                                       X
                                   Rpp (N ) =                     log p1 log p2 ,                   (6.1)
                                                    p1 +p2 =N
                                                   p1 ,p2 prime

again over ordered pairs.
   G2 proves
                            RО› (N ) в€’ Rpp (N ) = O(N 1/2 (log N )2 ) = o(N ).                       (6.2)
The difference is exactly the nonnegative contribution of ordered pairs in which at least one coor-
dinate is a nontrivial prime power pk , k в‰Ґ 2. There are O(N 1/2 ) such possible coordinates up to
N , the other coordinate is determined, and each О›-weight is at most log N .
    From (5.2) and (6.2),
                                    Rpp (N ) = S(N )N + o(N ).                                (6.3)




                                                         4
7     Positivity and Strong Goldbach
For even N , every factor (p в€’ 1)/(p в€’ 2) in (4.3) is positive and at least one, so

                                             S(N ) в‰Ґ 2C2 > 0.                                  (7.1)

Hence, for all sufficiently large even N ,

                                         Rpp (N ) в‰Ґ C2 N > 0.                                  (7.2)

   Every summand in Rpp (N ) is nonnegative and is strictly positive exactly for a genuine prime
representation N = p1 + p2 . Therefore Rpp (N ) > 0 implies that such a representation exists.
   Thus
                     every sufficiently large even N is a sum of two primes.                   (7.3)


8     Output Theorem
Theorem 1 (Final modular assembly). Assume the base exact decomposition and routing lemmas
B1/B3/F3/F3T/F4, the Edge and LongAP/Local lemmas C1P/C1A/C1 and D1, the global parameter
and error-budget lemmas PAR/GEB, and the four standalone theorem packages:

    1. H4 Local Algebra;

    2. TNG/TC1 No Rogue Short Interval;

    3. GoodAWACK Finite Grammar;

    4. CKP/X10/X16 Analytic.

Then I1 gives
                                      RО› (N ) = S(N )N + o(N ).
Together with G2 and G1/G0H this proves that every sufficiently large even integer is a sum of two
primes.


9     Status of This Assembly
This document is an independent final assembly module. It is not the long full manuscript and not
a replacement for the source md proofs. Its purpose is to show the complete logical closure once
the four technical theorem packages are accepted.
    The full manuscript remains available in manuscript_full_md/ and manuscript_latex/. Both
assembly variants use the same proof-source md layer.




                                                    5

