      A Proof of the Binary Goldbach Conjecture for All Sufficiently
                           Large Even Integers
                               Denis Saltykov (ds1678@gmail.com)

                                              29 May 2026


   Status: manuscript-MD publication overview.
   This manuscript layer is prepared for LaTeX generation. The mathematical source is the lemma
and external-input layer. The present file fixes the article order and records the exact files that a
converter should include.

0.1     Main Theorems
0.1.1    Theorem 1.1 (Sufficiently large binary Goldbach)
For every sufficiently large even integer 𝑁 , there exist primes 𝑝1 , 𝑝2 such that

                                                 𝑁 = 𝑝1 + 𝑝2 .

0.1.2    Theorem 1.2 (Weighted Goldbach asymptotic)
For every sufficiently large even integer 𝑁 ,
                                         ∑︁
                         𝑅Λ (𝑁 ) =               Λ(𝑛1 )Λ(𝑛2 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ),
                                     𝑛1 +𝑛2 =𝑁

   where
                                   ∏︁ 𝑝 − 1                  ∏︁ (︂           1
                                                                                     )︂
                     S(𝑁 ) = 2𝐶2                 ,    𝐶2 =           1−                   > 0.
                                   𝑝|𝑁
                                         𝑝−2                 𝑝>2
                                                                          (𝑝 − 1)2
                                   𝑝>2

   For even 𝑁 , S(𝑁 ) ≥ 2𝐶2 > 0. Theorem 1.1 follows from Theorem 1.2 by prime-power removal
and positivity.

0.2     Canonical Build Order
The future LaTeX converter should read build_order.md; it should not scan the directory recur-
sively.

0.3     Source Policy
Proof prose refers to logical objects: Theorem 1.2, Lemma B1, Lemma F3T, Lemma E10X, X9L-GT,
X10, and so on. File paths appear only in Appendix G and in workflow metadata. Mathemat-
ical corrections must be made first in the proof-source layer and then propagated back into this
manuscript layer.

                                                      1
1     Abstract and Front Matter
Author: Denis Saltykov.
   Affiliation: independent researcher.
   Email: ds1678@gmail.com.
   Date: 29 May 2026.
   MSC 2020: primary 11P32; secondary 11N05, 11N36, 11L05, 11B30.
   Keywords: binary Goldbach problem, von Mangoldt correlations, Heath–Brown identity, Kloost-
erman fractions, Liouville orthogonality, local density, routing lemma.

1.1    Abstract
We prove that every sufficiently large even integer is a sum of two primes. The proof establishes
the weighted asymptotic
                                 ∑︁
                                           Λ(𝑛1 )Λ(𝑛2 ) = S(𝑁 )𝑁 + 𝑜(𝑁 )
                               𝑛1 +𝑛2 =𝑁

    for even 𝑁 , with the classical Goldbach singular series S(𝑁 ). The argument begins with a
fixed-depth Heath–Brown decomposition of both von Mangoldt factors and routes every resulting
B1-origin atom into one of five terminal classes: Edge, CKP, GoodAWACK, LongAP/Local, or
LocalDiag. Edge terms are estimated by strict savings, CKP terms by a Duke–Friedlander–Iwaniec
Kloosterman-fraction input after a smooth-weight derivative verification, GoodAWACK terms by
a TC1 global testing route and a finite-grammar closure, and local terms by explicit tagged Λ𝑄 -
local projections. A global error-budget lemma verifies that all terminal errors are simultaneously
summable. Prime-power removal and positivity of the singular series then give a genuine prime
representation.


2     Introduction and Relation to Known Work
The binary Goldbach problem asks whether every even integer greater than 2 is a sum of two primes.
The classical circle method proves strong averaged statements and, beginning with Vinogradov,
proves ternary Goldbach for sufficiently large odd integers. The completed weak Goldbach theorem
removes the remaining finite range in the ternary problem. The binary problem is more delicate
because the expected main term has only one degree of freedom, and minor-arc cancellation must
interact with arithmetic local factors without losing the main term.
    The present proof is organized around a finite decomposition-and-routing architecture. A fixed-
depth Heath–Brown identity expands the two von Mangoldt factors into finitely many typed product
variables. Each product block is then partitioned by deterministic routing operations. The routing
theorem is designed so that every terminal atom belongs to a class with a specified analytic or local
mechanism.
    The five terminal classes are:

    1. Edge, where strict size, conductor, boundary, or square-divisor savings give 𝑜(𝑁 );

    2. CKP, where a balanced bilinear Kloosterman-fraction structure is present;

    3. GoodAWACK, where the remaining Branch B atoms are handled by the TC1 global testing
       route and the E10Y-certified finite GoodAWACK routing grammar;


                                                    2
    4. LongAP/Local, where no nonlocal arithmetic coefficient survives and the term satisfies the
       explicit H4 tagged local projection condition;

    5. LocalDiag, where forced local dependence is admitted only when it is the same tagged LPI
       local projection later assembled by H4.

    Two features distinguish the route from a direct circle-method argument. First, the proof does
not try to estimate all descendants with one universal analytic theorem. It proves a complete finite
classification and uses different tools on the different terminal classes. Second, the proof avoids the
earlier inverse-Gowers route X8. The GoodAWACK branch is instead closed by the combination of
a TC1 global testing dichotomy and a structural finite-grammar theorem for rank-dropping affine
regroupings.
    The most delicate points are the completeness of the terminal routing, the CKP/X10 smooth-
weight match, the X16/Shiu carrier-slice estimate used inside the TC1 route, the GoodAWACK
finite-grammar closure, and the local-main reconstruction. These points are isolated as named
lemmas and appendices rather than hidden in the final assembly.


3      Main Theorems and Proof Strategy
3.1      Weighted Form
Let
                                                         ∑︁
                                        𝑅Λ (𝑁 ) =               Λ(𝑛1 )Λ(𝑛2 ).
                                                    𝑛1 +𝑛2 =𝑁

      The central theorem is Theorem 1.2:

                                          𝑅Λ (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 )
      for sufficiently large even 𝑁 .
      The singular series is
                                         ∏︁ 𝑝 − 1                    ∏︁ (︂         1
                                                                                       )︂
                          S(𝑁 ) = 2𝐶2                ,        𝐶2 =           1−          .
                                         𝑝|𝑁
                                               𝑝−2                   𝑝>2
                                                                                (𝑝 − 1)2
                                         𝑝>2

      Since S(𝑁 ) ≥ 2𝐶2 > 0 for even 𝑁 , the weighted asymptotic is eventually positive.

3.2      Decomposition and Routing
Lemma B1 gives an exact finite Heath–Brown decomposition of both factors in 𝑅Λ (𝑁 ). Lemmas
B3, F3, F4, E5, and F3T convert every B1-origin atom into a finite tagged sum of terminal atoms
in exactly the five terminal classes

                     Edge,    CKP,      GoodAWACK,             LongAP/Local,        LocalDiag.
   The tagged partition is exact; overlaps between visual algebraic shapes do not create double
counting because the routing history is part of the terminal tag.




                                                          3
3.3    Terminal Estimates
The terminal estimates are:

    1. Edge terms are 𝑜(𝑁 ) by C1A and C1.

    2. CKP terms equal the explicit H4 tagged local projection plus 𝑜(𝑁 ) by G8a, CKPD, X10, and
       B1LD.

    3. GoodAWACK terms are 𝑜(𝑁 ) by E10L, TNG, X9L-GT, X16BRS/X16C, E10Y, E10M, E10X,
       and E10K.

    4. LongAP/Local terms satisfy the H4 tagged admission condition plus 𝑜(𝑁 ) by D1 and H4.

    5. LocalDiag terms are admitted only when they are tagged LPI local projections later assembled
       by H4.

   The global error-budget lemma GEB proves that these estimates remain 𝑜(𝑁 ) after all dyadic
and routing summations.

3.4    Assembly
The local projections admitted by D1, G8a/B1LD, and LocalDiag are all passed through H4. H4
uses the explicit Λ𝑄 -model, tagged linearity over the B1/F3 partition, no double counting, and the
CRT local factor computation to prove

                                    𝑀local (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
   Combining this with the terminal error bounds gives Theorem 1.2. Lemmas G2, G1, and G0H
then remove nontrivial prime powers and convert positivity into a prime representation.


4     Notation, Parameters, and Error Budget
Throughout, 𝑁 is an even integer tending to infinity and

                                             𝐿 = log 𝑁.
   All implicit constants may depend on the fixed decomposition depth and on the fixed smooth
cutoffs, but not on 𝑁 .

4.1    Fixed Depth and Dyadic Partitions
The Heath–Brown depth is fixed once and for all. We use a parameter 𝐽0 large enough for the
global hierarchy. The explicit consistency witness used in the parameter register is
                                                     1              1
                                𝐽0 = 20,      𝜂=       ,    𝜃=         .
                                                    40            4000
     The witness is not optimized. Its role is to show that all inequalities in the parameter hierarchy
can be satisfied simultaneously.
     Every variable produced by the B1 decomposition is smoothly dyadically localized. For fixed
𝐽0 , the total number of active dyadic and routing cells is 𝐿𝑂(1) .


                                                   4
4.2     Terminal Classes
The proof uses the following terminal classes.

      Class                           Meaning                           Output
      Edge                            strict saving, boundary, short    𝑜(𝑁 )
                                      volume, square-divisor, or con-
                                      ductor loss
      CKP                             balanced Kloosterman-fraction     local projection +𝑜(𝑁 )
                                      branch
      GoodAWACK                       Branch B affine/global-testing    𝑜(𝑁 )
                                      branch
      LongAP/Local                    long local arithmetic progres-    local projection +𝑜(𝑁 )
                                      sion branch
      LocalDiag                       forced local dependence or di-    local projection
                                      agonal branch




4.3     Global Error Budget
GEB records the summability principle used throughout the proof. If a per-terminal estimate
gains either a fixed power of 𝑁 or a sufficiently large negative power of 𝐿, then the 𝐿𝑂(1) terminal
multiplicity is harmless.
   The constants are chosen in the following order:

    1. fix 𝜃 ≪ 𝜂;
    2. choose 𝐽0 ≥ 𝐽* (𝜂);
    3. fix the routing multiplicity constant 𝐶0 (𝐽0 );
    4. fix the Edge and divisor losses;
    5. choose the X16/Shiu logarithmic floor exponent;
    6. choose the TC1 near-global modulus and AP exponents;
    7. choose CKP high-frequency and DFI derivative thresholds.

  With this order, later logarithmic exponents can always dominate earlier polylogarithmic losses.
GEB is invoked only as a bookkeeping lemma; it does not replace the branch estimates.


5      External Inputs
The proof uses four external inputs, each in a fixed stated form.

5.1     X1: Heath–Brown Identity
X1 is the fixed-depth Heath–Brown identity used to decompose each von Mangoldt factor. The
active formulation is the one needed by B1: after choosing 𝐽0 , Λ is represented by a finite linear
combination of typed divisor-convolution factors with controlled coefficients and smooth dyadic
localization.

                                                    5
5.2   X9L-GT: Near-Global Liouville/AP Orthogonality
X9L-GT is the Davenport/AP input used only after the TC1 route has produced near-global active
B1-origin coarea tests. It is not invoked on arbitrary shifted short intervals. TTH supplies the
near-global length condition

                                         𝐻 ≥ 𝑋(log 𝑋)−𝐵𝜅 .
    The TC1 testing family has only polylogarithmic modulus and AP complexity, so the Davenport
saving can be chosen to dominate the recorded losses.

5.3   X10: DFI Kloosterman-Fraction Estimate
X10 is the Duke–Friedlander–Iwaniec bilinear Kloosterman-fraction estimate in the smooth weighted
form required by CKP. The CKP branch uses X10 only after G1a–G3a reduce the nonzero-frequency
terms to the DFI form and CKPD verifies the actual two-variable smooth weight.
   No later Kloosterman-fraction strengthening is an active dependency.

5.4   X16: Shiu/AP Divisor-Average Input
X16 is the Shiu-type arithmetic-progression divisor-average input used in the BRS carrier-slice step
of the TC1 route. X16C proves the active normalized carrier estimate, including the divisor-function
second moment and the logarithmic floor needed by GEB.

5.5   Citation Boundary
Each external theorem is invoked only through its named stated interface: X1, X9L-GT, X10, and
X16. The manuscript does not appeal to informal variants of these results.


6     Heath–Brown Decomposition
6.1   B1 Blocks
Lemma B1 applies the fixed-depth Heath–Brown identity to both copies of Λ in 𝑅Λ (𝑁 ). It writes
𝑅Λ (𝑁 ) as a finite sum of B1 blocks. Each B1 block consists of two finite lists of product variables,
smooth dyadic cutoffs, and elementary coefficient types

                                       𝜇 · 1≤𝑦 ,       1,   log .
   For fixed 𝐽0 , the number of elementary variables in a B1 block is bounded, and the number of
dyadic cells is 𝐿𝑂(1) .

6.2   Exactness
The B1 decomposition is an identity before estimates are applied. Smooth dyadic partitions are
inserted as exact partitions of unity up to boundary terms already routed to Edge. Thus no main
term is lost at the decomposition stage.




                                                   6
6.3   Structural Output
The output of B1 is a structural finite-convolution problem together with the equation inherited
from 𝑛1 + 𝑛2 = 𝑁 . The routing layer decides which grouped variables, divisor relations, local
congruences, and oscillatory features survive to terminal atoms.
   The subsequent proof uses only B1-origin atoms. This origin condition is important in the
GoodAWACK finite-grammar argument: formal affine systems that do not arise from the B1/B3/F3/F4
grammar are not terminal descendants of the proof.


7     Routing Exhaustion
7.1   Finite Grouping
Lemma B3 supplies a finite set of product-grouping candidates for each B1 block. Candidate labels
may overlap at this preliminary stage; they are not yet terminal classes.

7.2   Authoritative Routing Operations
Lemma F3 supplies the complete routing operations for actual F3 atoms. These include controlled
CRT absorption, ordinary divisor decisions through F4, square-divisor routing, grouping selection
or elimination, terminal Edge detection, terminal LocalDiag detection, and final terminal labelling.
    Lemma E5 is used only as content stability for transports generated by the routing grammar.
It is not an independent generator of terminal affine systems.

7.3   Exhaustion Theorem
Lemma F3T proves the finite routing exhaustion theorem:


      B1 + B3 + F3 + F4 + E5 =⇒ {Edge, CKP, GoodAWACK, LongAP/Local, LocalDiag}.

    More precisely, each B1-origin atom is partitioned into a finite disjoint sum of tagged terminal
atoms in exactly those five classes. No sixth terminal class remains.
    The proof uses a deterministic routing order and a well-founded routing measure M♯ . Nonter-
minal operations strictly decrease this measure, while terminal rows assign one of the five tags. If
a cell visually satisfies more than one terminal predicate, the tag records the first applicable class
in the deterministic order. Therefore visual overlap does not imply double counting.

7.4   Terminal Interfaces
Once F3T has assigned terminal tags, the estimates are supplied by the corresponding branch
lemmas:


Edge → 𝐶1𝐴/𝐶1,       CKP → 𝐺8𝑎,       GoodAWACK → 𝐸10𝐿,          LongAP/Local → 𝐷1/𝐻4,          LocalDiag → 𝐻4.




                                                  7
8     Edge Estimates
8.1    Edge Predicates
Edge terms are terminal cells carrying a strict saving predicate. The active predicates include
boundary or short-volume loss, Type I saving, large gcd/content, square-divisor tails, high Fourier
tails, and small-conductor layers.
    Lemma C1 proves that any cell satisfying one of the strict Edge predicates contributes 𝑜(𝑁 )
after its allowed coefficient and polylogarithmic losses.

8.2    Admission
Lemma C1A proves the converse admission statement needed by the manuscript: every active
terminal atom routed into Edge satisfies one of the strict C1 predicates. Thus Edge is not a
residual label. It is a verified saving class.
    The admission ledger treats the Edge sources from F3/F4, CKP excluded ranges, BRS carrier
slices, square-divisor routing, boundary terms, and high-frequency tails. Each source is paired with
a saving estimate and a summability check.

8.3    Summation
For fixed 𝐽0 , the number of Edge cells is 𝐿𝑂(1) . C1 supplies either a fixed power saving in 𝑁 or a
logarithmic saving chosen larger than the routing multiplicity. GEB therefore gives

                                           𝑅Edge (𝑁 ) = 𝑜(𝑁 ).


9     LongAP/Local Terms
9.1    Terminal LongAP/Local Atoms
A LongAP/Local atom is a terminal B1-origin cell satisfying the intrinsic F3P LongAP/Local pred-
icate: its long-variable coefficients lie in the controlled local coefficient algebra on a long arithmetic-
progression fibre. It is not allowed to contain a surviving nonlocal 𝜇-, 𝜆-, Fourier-, Kloosterman-,
or nilsequence-type coefficient.

9.2    Exclusion of Nonlocal Coefficients
Lemma D1.2A proves that the F3P LongAP/Local predicate has the advertised consequence inside
the routed B1/F3 partition: no nonlocal arithmetic coefficient survives in a terminal LongAP/Local
atom. The proof combines the positive F3P predicate with the finite F3/F4 routing alternatives:

    1. a surviving oscillatory or Liouville/Mobius-type factor routes to GoodAWACK or CKP;

    2. a strict saving predicate routes to Edge;

    3. forced local dependence routes to LocalDiag;

    4. only local AP/congruence data remains in LongAP/Local.

   Thus D1 may replace F3P-LongAP/Local atoms by the explicit H4 tagged local projections
without discarding hidden arithmetic oscillation.

                                                    8
9.3    Output
Lemma D1 gives, for each LongAP/Local terminal cell,

                          𝑅LongAP/Local (𝑁 ) = 𝑀LongAP/Local (𝑁 ) + 𝑜(𝑁 ),
   where the main term is the H4 Λ𝑄 -projection of the same tagged B1/F3 cell. Boundary and
smoothing errors are Edge-admitted.


10     The CKP Branch
10.1    CKP Claim
The CKP branch proves

                                    𝑅CKP (𝑁 ) = 𝑀CKP (𝑁 ) + 𝑜(𝑁 ),
   where 𝑀CKP (𝑁 ) is the explicit H4 tagged local projection obtained by the same Λ𝑄 -replacement
used in Appendix E.

10.2    Internal Reduction
The CKP proof follows the chain

             𝐺1𝑎 + 𝐺2𝑎 + 𝐺3𝑎 + 𝐶𝐾𝑃 𝐷 + 𝐺4𝑎/𝑋10 + 𝑋10-𝐸𝑅 + 𝐵1𝐿𝐷 =⇒ 𝐺8𝑎.
   Lemma G1a performs the gcd splitting 𝑢 = 𝑔𝑎, 𝑢′ = 𝑔𝑞, with (𝑎, 𝑞) = 1. Lemma G2a performs
the smooth AP/Fourier expansion. The zero-frequency term is local. Lemma G3a writes each
nonzero central frequency as a bilinear Kloosterman-fraction sum

                                                               ℎ𝑁𝑔 𝑎
                                ∑︁                           (︂      )︂
                                      𝛼𝑔 (𝑎)𝛾𝑔 (𝑞)𝑊𝑔,ℎ (𝑎, 𝑞)𝑒       .
                            𝑎∼𝐴 , 𝑞∼𝑄
                                                                𝑞
                                𝑔        𝑔
                               (𝑎,𝑞)=1


10.3    X10 Match
X10 is invoked only for the central nonzero-frequency range. CKPD proves that the actual two-
variable Fourier weight 𝑊𝑔,ℎ (𝑎, 𝑞), including the dependence 𝑧(𝑎, 𝑞, 𝑦) = (𝑁𝑔 − 𝑎𝑦)/𝑞, satisfies the
smooth derivative hypotheses of the DFI Kloosterman-fraction theorem with only polylogarithmic
loss.
    Excluded ranges are not sent to X10. The X10ER routing statement sends them to Edge
through C1A/C1, to local zero-frequency terms, or to the CKP auxiliary exclusions recorded in
G8a.

10.4    Output
The nonzero-frequency CKP contribution is 𝑜(𝑁 ). The zero-frequency term is identified by B1LD
with the local model used by H4. Therefore G8a supplies the CKP input needed by I1.




                                                  9
11      The GoodAWACK Branch
11.1     Branch B Theorem
Lemma E10L proves that the total terminal GoodAWACK contribution is 𝑜(𝑁 ). The proof has
two components:
  1. the TC1 global testing route;
  2. the HighTC finite-grammar closure.

11.2     TC1 Global Testing
The TC1 route does not choose an arbitrary shifted short interval. It tests only structural B1-origin
coarea families whose cells have not already been routed away. Theorem TNG-A gives the single
near-global-or-routed interface:

               every unrouted TC1 test is near-global, or routed away before X9L-GT.
     In the near-global alternative the test satisfies

                                           𝐻 ≥ 𝑋(log 𝑋)−𝐵𝜅 .
    Thus X9L-GT applies in its Davenport/AP form with polylogarithmic modulus and AP com-
plexity. The resulting orthogonality estimate is summable by GEB.
    In the routed alternative, TTD, ROC, BRS, and X16BRS/X16C send the test to Edge, Lon-
gAP/Local, CKP, LocalDiag, or zero before X9L-GT is invoked.

11.3     Finite GoodAWACK Grammar
The HighTC branch is closed by the finite combinatorial grammar package E10Y/E10X/E10M/E10K.
E10Y proves that every actual terminal GoodAWACK skeleton is generated from B1/B3 grouped
cells by the listed B1/B3/F3/F4/E5 grammar: fixing/projection, controlled CRT restriction, fixed
divisor quotient, F4-tagged variable quotient, local/diagonal/gcd dependence, CKP-balanced struc-
ture, Edge-type saving or boundary routing, full-rank affine regrouping, post-terminal slicing after
terminal vectors are fixed, E5 auxiliary inheritance, and final terminal labelling. E5 is used only
as content stability and is not an independent terminal generator.
     E10X proves by induction on the E10Y-certified finite grammar that every rank-dropping affine
operation created along a derivation carries an allowed origin tag. E10S and E10S-MECH are
non-logical source-maintenance and reproducibility records for the maintained Branch B source
list; they are not premises of the induction. E10M then proves that no untagged rank-dropping
AFF occurrence survives in an actual terminal GoodAWACK skeleton. E10K converts this into
AFF-origin completeness, and E10X eliminates the FreeAffineHighTC residual.
     The formal 4𝐴𝑃 -like family 𝑌𝑖 = 𝑥 + 𝑖𝑟 remains useful as an interface test, but E10X proves
that it has no untagged actual terminal occurrence in the finite routing grammar.

11.4     Output
TC1 contributes 𝑜(𝑁 ), singular tests are routed to already handled classes, and HighTC finite-
grammar residuals are eliminated structurally. Hence

                                       𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).

                                                    10
12      Local/Main Assembly
12.1     Explicit H4 Local Algebra
The local/main layer is assembled by a concrete finite local model, not by an undefined projection
convention. Let
                                ∏︁
                         𝑄=          𝑝,     𝑤 = 𝑤(𝑁 ) → ∞,                 𝑤 = 𝑜(log 𝑁 ),
                               𝑝≤𝑤

     and define

                              𝑄                                   1 ∑︁
                  Λ𝑄 (𝑎) =       1        ,      𝜎𝑄 (𝑁 ) =                  Λ𝑄 (𝑎)Λ𝑄 (𝑁 − 𝑎).
                             𝜙(𝑄) (𝑎,𝑄)=1                         𝑄 𝑎 mod 𝑄

     The local projection of the original Goldbach convolution is

                                          Loc𝑄 𝑅Λ (𝑁 ) = 𝑁 𝜎𝑄 (𝑁 ).
    For a terminal tagged cell (ℬ, 𝜏 ), LPI defines Loc𝑄 𝑅ℬ,𝜏 (𝑁 ) by replacing the arithmetic coeffi-
cients inside that same tagged cell by their residue-class local densities modulo 𝑄, preserving the
parent B1 block, routing tag, dyadic weights, and local congruence data.

12.2     H4 Admission
H4 admits a terminal local/main expression only if it satisfies the tagged admission condition

                                  local
                                 𝑀ℬ,𝜏   (𝑁 ) = Loc𝑄 𝑅ℬ,𝜏 (𝑁 ) + 𝑜ℬ,𝜏 (𝑁 ).
   Thus a local-looking expression does not enter the main term merely because it resembles a local
density. It must be attached to a parent B1 block and a terminal routing tag, and its normalization
must be the single Λ𝑄 -replacement above.
   The admitted local sources are:

  1. LongAP/Local main terms whose F3P terminal predicate already forces the long-variable
     coefficients into the local coefficient algebra, with D1 expanding them into the tagged local
     projection;

  2. CKP zero-frequency terms from G8a/B1LD, after the zero mode is identified with the same
     tagged Λ𝑄 -replacement;

  3. LocalDiag terms, admitted only when the diagonal specialization is a tagged local projection;

  4. harmless local boundary contributions explicitly admitted by H4 and already bounded through
     C1.

12.3     Linearity and No Double Counting
The exact B1 decomposition and the exact F3 tagged partition give
                                                 ∑︁          ∑︁
                                     𝑅Λ (𝑁 ) =        𝑐ℬ              𝑅ℬ,𝜏 (𝑁 ).
                                                 ℬ         𝜏 ∈𝒯 (ℬ)

     The operator Loc𝑄 is linear on this finite tagged partition. Therefore

                                                       11
               ∑︁          ∑︁
                    𝑐ℬ              Loc𝑄 𝑅ℬ,𝜏 (𝑁 ) = Loc𝑄 𝑅Λ (𝑁 ) + 𝑜(𝑁 ) = 𝑁 𝜎𝑄 (𝑁 ) + 𝑜(𝑁 ).
                ℬ        𝜏 ∈𝒯 (ℬ)

   No double counting occurs because each local term is indexed by its parent B1 block ℬ and its
routing tag 𝜏 . Different B1 blocks are different summands of the exact B1 identity, and different
tags inside the same block are disjoint cells of the F3 partition. Algebraically identical LocalDiag-
looking formulas from different tags are therefore distinct partition summands, not duplicates.

12.4     Finite Local Factors
The finite density 𝜎𝑄 (𝑁 ) factors by the CRT. For 𝑝 ≤ 𝑤,
                                                 )︂2
                              1             𝑝
                                      (︂
                    𝜎𝑝 (𝑁 ) =                          #{𝑎 mod 𝑝 : (𝑎, 𝑝) = 1, (𝑁 − 𝑎, 𝑝) = 1}.
                              𝑝            𝑝−1
     For even 𝑁 , 𝜎2 (𝑁 ) = 2. For odd 𝑝,
                                                         ⎧    𝑝
                                                         ⎪
                                                         ⎪       ,           𝑝 | 𝑁,
                                                         ⎨   𝑝−1
                                           𝜎𝑝 (𝑁 ) =               1
                                                         ⎩1 −            ,   𝑝 ∤ 𝑁.
                                                         ⎪
                                                         ⎪
                                                                (𝑝 − 1)2
     Hence
                                                               ∏︁ 𝑝 − 1
                                           𝜎𝑄 (𝑁 ) → 2𝐶2                   = S(𝑁 ).
                                                               𝑝|𝑁
                                                                     𝑝−2
                                                               𝑝>2


12.5     Weighted Assembly
Combining the LPI admission condition consumed by H4, tagged linearity, no double counting, and
the finite local factor computation gives

                                𝑀local (𝑁 ) = 𝑁 𝜎𝑄 (𝑁 ) + 𝑜(𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
     Lemma I1 then combines the terminal estimates and H4:

                                𝑅Λ (𝑁 ) = 𝑀local (𝑁 ) + 𝑜(𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
    GEB verifies that all terminal 𝑜(𝑁 ) terms remain 𝑜(𝑁 ) after the full polylogarithmic decompo-
sition and routing summation.


13      Prime-Power Removal and Final Proof
13.1     Statement
Assume the weighted asymptotic I1:

                                              𝑅Λ (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 )
    for sufficiently large even 𝑁 . Then, after removing the negligible nontrivial prime-power con-
tribution by G2, the genuine prime-pair weighted sum is positive. Consequently every sufficiently
large even 𝑁 is a sum of two primes.

                                                                12
13.2    Setup
The von Mangoldt function is supported on prime powers:
                                           {︃
                                                log 𝑝,    𝑛 = 𝑝𝑘 , 𝑘 ≥ 1,
                                  Λ(𝑛) =
                                                0,        otherwise.
    Let 𝑅𝑝𝑝 (𝑁 ) denote the ordered weighted sum restricted to genuine prime pairs:
                                                  ∑︁
                                 𝑅𝑝𝑝 (𝑁 ) =                   (log 𝑝1 )(log 𝑝2 ).
                                               𝑝1 +𝑝2 =𝑁
                                              𝑝1 ,𝑝2 prime

    The ordered-pair convention is the same convention used in B1, I1, G2, G1, and G0H.

13.3    Proof
Lemma G2 removes the nontrivial prime powers 𝑝𝑘 , 𝑘 ≥ 2. There are 𝑂(𝑁 1/2 ) such prime powers
up to 𝑁 , and once one coordinate in 𝑛1 + 𝑛2 = 𝑁 is selected the other coordinate is determined.
Since Λ(𝑛) ≤ log 𝑁 , the total contribution from pairs in which at least one coordinate is a nontrivial
prime power is

                                      𝑂(𝑁 1/2 (log 𝑁 )2 ) = 𝑜(𝑁 ).
    Therefore I1 and G2 imply

                                     𝑅𝑝𝑝 (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
    For even 𝑁 , the Goldbach singular series satisfies

                                          S(𝑁 ) ≥ 2𝐶2 > 0.
    Hence 𝑅𝑝𝑝 (𝑁 ) > 0 for all sufficiently large even 𝑁 . Since every summand in 𝑅𝑝𝑝 (𝑁 ) is nonneg-
ative and the summands on genuine prime pairs are positive, this positivity implies that at least
one ordered pair of primes 𝑝1 , 𝑝2 satisfies

                                              𝑝1 + 𝑝2 = 𝑁.

13.4    Output
Lemma G0H records the ordered-pair normalization and the final logical handoff

                                      𝐼1 + 𝐺2 =⇒ 𝐺1 =⇒ 𝐺0.
    The statement proved is the sufficiently-large binary Goldbach theorem. Finite verification
below the asymptotic threshold is outside the asymptotic claim of this manuscript.


A      Routing Tables
This appendix records the routing table used by Lemma F3T. The terminal predicates themselves
are the intrinsic predicates fixed in Lemma F3P; the branch estimates are invoked only after the
routing tag has been assigned.


                                                         13
A.1    Terminal Classes

   Class                          Entry condition                     Exit theorem
   Edge                           strict C1 saving predicate          C1A/C1
   LocalDiag                      forced local dependence or di-      H4
                                  agonal relation
   LongAP/Local                   F3P long AP/local fibre whose       D1/H4
                                  long-variable coefficients lie in
                                  the local coefficient algebra
   CKP                            balanced bilinear Kloosterman-      G8a/X10
                                  fraction structure
   GoodAWACK                      Branch B affine/global-testing      E10L
                                  residual with controlled origin




A.2    Canonical Routing Order
On each tagged B1-origin cell, F3T reads the following order.

  1. Empty or incompatible cells are zero.

  2. Strict C1 saving predicates go to Edge.

  3. Forced equality, proportionality, repeated factor, or local dependence goes to LocalDiag.

  4. Ordinary divisor and quotient predicates are decided by F4.

  5. Square-divisor obstructions are routed by F3.

  6. Controlled CRT restrictions are absorbed only when E5 verifies clean content stability.

  7. Remaining grouping alternatives are selected or eliminated from the finite B3 grouping set.

  8. The terminal predicate assigns one of the five terminal classes.

   Every nonterminal step strictly decreases M♯ . Therefore the process terminates.

A.3    Routing Table

   Row                    Source regime                Routing outcome        Reason no other termi-
                                                                              nal class receives the
                                                                              cell
   1                      empty support or             Edge-zero              no analytic mass re-
                          incompatible congru-                                mains
                          ences
   2                      boundary, short vol-         Edge                   a strict C1 saving
                          ume, large content,                                 predicate is present
                          square-divisor  tail,
                          high    Fourier tail,
                          small conductor, or
                          Type I saving


                                                  14
   3                      forced equality, pro-           LocalDiag              independent
                          portionality, repeated                                 CKP/GoodAWACK
                          factor, or local depen-                                variables are absent
                          dence
   4                      one long AP variable            LongAP/Local           the positive F3P pred-
                          and F3P local coeffi-                                  icate already excludes
                          cient algebra                                          nonlocal long-variable
                                                                                 coefficients; D1.2A ex-
                                                                                 pands the resulting lo-
                                                                                 cal algebra
   5                      central       balanced          CKP                    Edge/LocalDiag have
                          bilinear Kloosterman-                                  already failed;     the
                          fraction form                                          structure is bilinear,
                                                                                 not GoodAWACK
   6                      nonlocal      non-CKP           GoodAWACK              E10Y/E10X/E10M/E10K
                          Branch B affine resid-                                 exclude        untagged
                          ual with controlled                                    rank-dropping      AFF
                          origin                                                 residuals
   7                      ordinary divisor pred-          Edge                   F4 supplies a C1 pred-
                          icate with short quo-                                  icate
                          tient or saving
   8                      ordinary divisor pred-          LocalDiag              quotienting identifies
                          icate forcing local de-                                active forms
                          pendence
   9                      ordinary divisor pred-          CKP                    F4 removes local and
                          icate preserving bal-                                  short alternatives
                          anced bilinear struc-
                          ture
   10                     ordinary divisor pred-          GoodAWACK              quotient   origin   is
                          icate preserving con-                                  tagged and E5-clean
                          trolled Branch B affine
                          residual
   11                     large square divisor            Edge                   square-divisor saving
                                                                                 applies
   12                     small controlled square         nonterminal decrease   F3 continues with
                          divisor or full-rank                                   smaller M♯
                          CRT restriction
   13                     unresolved        finite        nonterminal decrease   B3 grouping set is fi-
                          grouping alternative            or terminal row        nite




    Rows 12–13 are not terminal rows. They are included to show that all nonterminal transitions
are among the allowed F3 operations.

A.4     Consequence
For fixed 𝐽0 , every B1-origin atom reaches exactly one tagged terminal class after finitely many
steps. This is the routing-exhaustion input used in the assembly theorem.




                                                     15
B      Edge Admission
This appendix records why every active Edge input satisfies a strict C1 predicate.

B.1     Edge Predicates
The active C1 predicates are:

    1. boundary or short-volume loss;

    2. Type I saving;

    3. large gcd or large content;

    4. large square-divisor tail;

    5. high Fourier tail;

    6. small conductor;

    7. incompatible or zero support.

    The exact numerical exponents are chosen inside the PAR/GEB hierarchy.

B.2     Admission Table

     Source                              Edge predicate                  Saving mechanism
     F3 empty or incompatible cell       zero support                    no mass
     F3 boundary cell                    boundary/short volume           volume loss
     F3 square-divisor tail              large square divisor            square-divisor summation
     F4 short quotient or divisor        Type I or short-volume saving   divisor/quotient loss
     CKP high-frequency tail             high Fourier tail               integration/Fourier decay
     CKP small-conductor layer           small conductor                 conductor saving
     CKP large 𝑔 or content              large gcd/content               divisor-bound loss
     BRS singular carrier slice resid-   boundary or slice-floor Edge    X16BRS/X16C plus C1
     ual
     LongAP/Local boundary error         boundary/short volume           C1 boundary estimate




B.3     Summability
C1A pairs each active Edge source with one of the predicates above. C1 then gives either a power
saving in 𝑁 or a logarithmic saving large enough to dominate the 𝐿𝑂(1) routing multiplicity. Hence
the total Edge contribution is 𝑜(𝑁 ).




                                                      16
C     CKP/X10 Smooth-Weight Matching
C.1    Target
The CKP branch proves

                                   𝑅CKP (𝑁 ) = 𝑀CKP (𝑁 ) + 𝑜(𝑁 ).
    The nonzero-frequency contribution is estimated by X10. The zero-frequency contribution is
local and is passed to H4.

C.2    DFI Theorem Used
The X10 input is the Duke–Friedlander–Iwaniec bilinear estimate for Kloosterman fractions. In
the smooth weighted form used here, one estimates

                                                            𝑟𝑚
                                         ∑︁                      (︂      )︂
                                            𝛼𝑚 𝛽𝑞 𝐹 (𝑚, 𝑞)𝑒    ,
                                   𝑚∼𝑀, 𝑞∼𝑄
                                                             𝑞
                                    (𝑚,𝑞)=1

   where 𝐹 is supported on a dyadic box and has controlled derivatives up to the required fixed
order. In the CKP application the derivative-control parameter is a fixed power of 𝐿.

C.3    CKP Substitution
After G1a–G3a, the central CKP nonzero-frequency layer has the form

                                                                  ℎ𝑁𝑔 𝑎
                                     ∑︁                                    (︂      )︂
                        𝒪𝑔,ℎ =           𝛼𝑔 (𝑎)𝛾𝑔 (𝑞)𝑊𝑔,ℎ (𝑎, 𝑞)𝑒       .
                               𝑎∼𝐴 , 𝑞∼𝑄
                                                                   𝑞
                                     𝑔        𝑔
                                   (𝑎,𝑞)=1

    The substitution into X10 is

                        𝑚 = 𝑎,           𝑀 = 𝐴𝑔 ,         𝑟 = |ℎ|𝑁𝑔 ,         𝑄 = 𝑄𝑔 .
   The coprimality condition is exactly (𝑎, 𝑞) = 1. For ℎ < 0, the same estimate is applied to the
conjugate phase, so the positive external integer parameter in X10 is 𝑟 = |ℎ|𝑁𝑔 . The case ℎ = 0 is
excluded from X10 and routed to the local term.

C.4    Smooth Weight
CKPD differentiates the actual CKP weight, not a separated surrogate. The weight contains the
Fourier-fibre dependence

                                                          𝑁𝑔 − 𝑎𝑦
                                           𝑧(𝑎, 𝑞, 𝑦) =           .
                                                             𝑞
    On the central support, CKPD proves

                                 ̃︁𝑔,ℎ (𝑎, 𝑞) ≪ 𝐿𝐶 𝐴−𝑖 𝑄−𝑗
                         𝜕𝑎𝑖 𝜕𝑞𝑗 𝑊                                    (0 ≤ 𝑖, 𝑗 ≤ 2).
                                                    𝑔   𝑔

    Thus the X10 smooth-weight hypotheses hold with polylogarithmic loss.




                                                     17
C.5    Excluded Ranges
The following ranges are not sent to X10:


      Excluded range                                  Routing
      ℎ=0                                             B1LD and H4
      high Fourier frequency                          Edge
      small conductor                                 Edge
      large 𝑔 or large content                        X10ER, then Edge or CKP auxiliary exclu-
                                                      sion
      boundary or short-volume layer                  Edge




   After these exclusions, the remaining central nonzero-frequency contribution is 𝑜(𝑁 ) by X10
and GEB.


D     TC1, BRS/TTH, and GoodAWACK Finite Grammar
D.1    TC1 Route
The TC1 branch tests structural B1-origin coarea families whose cells have not already been routed
away. It never invokes Liouville/AP orthogonality on an arbitrary shifted short interval.
   The route is packaged as Theorem TNG-A:

                   every unrouted TC1 test is either near-global or routed away.
    The closure barrier preventing rogue short-interval refinements is TTH-SC. It proves that every
short subtest of a released structural coarea test is either non-structural and reaggregated, or
structural and routed through TTD/ROC/BRS/X16BRS/X16C before X9L-GT is invoked.
    On the near-global alternative:

                                        𝐻 ≥ 𝑋(log 𝑋)−𝐵𝜅 .
  At this length, X9L-GT supplies the needed Davenport/AP orthogonality with polylogarithmic
modulus and AP complexity.
  The bridge from a non-small TC1 macro-template to a measured family of Liouville tests is
TGT-MF. It proves the finite Fourier/coarea transfer

                                       GT-U2 =⇒ GT-Test,
   with a probability measure 𝜈𝜅 and fixed lower bound depending only on the macro-template.
Thus the route tests an averaged family, not a selected pointwise short interval.

D.2    Singular Tests
If a testing measure is singular, it is not sent to X9L-GT. The routed alternative of TNG-A, proved
by TTD/ROC/BRS with X16BRS/X16C, shows that an unrouted singular B1-origin coarea test
must enter one of the already controlled destinations:

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

                                                 18
    The carrier-slice estimates used in this step are supplied by X16BRS and X16C. X16C uses
the Shiu AP divisor-average input and the fixed divisor-function second moment recorded in the
bibliography.

D.3      Finite GoodAWACK Grammar
The HighTC part is closed structurally. E10Y proves completeness of the finite grammar for actual
terminal GoodAWACK skeletons. The start states are B1/B3 grouped cells, and the allowed tran-
sitions are fixing/projection, controlled CRT restriction, fixed divisor quotient, F4-tagged variable
quotient, local/diagonal/gcd dependence, CKP-balanced structure, Edge routing, full-rank affine
regrouping, post-terminal slicing after terminal vectors are fixed, E5 auxiliary inheritance, and
terminal labelling.
    E10X proves a grammar invariant on the E10Y-certified grammar: every rank-dropping affine
operation generated by these transitions carries an allowed origin tag. E10S and E10S-MECH
are non-logical source-maintenance and reproducibility records for the listed Branch B source list;
they are not premises of the closure. E10M proves that every rank-dropping affine occurrence in
an actual terminal GoodAWACK skeleton is tagged by an allowed origin. Therefore no untagged
rank-dropping AFF source exists. E10K gives AFF-origin completeness, and E10X removes the
FreeAffineHighTC residual.

D.4      Formal Interface Examples
The formal 4𝐴𝑃 -like pattern 𝑌𝑖 = 𝑥 + 𝑖𝑟 is retained as a diagnostic interface example. It shows why
broad affine regrouping language is unsafe if read without origin data. It is not a terminal obstruc-
tion because any actual terminal occurrence must either be full-rank safe, tagged and rerouted, or
excluded by the no-untagged-AFF theorem.

D.5      GoodAWACK Output
Combining TC1 testing, singular rerouting, and finite-grammar HighTC closure gives

                                     𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).


E      Explicit Local Projection Algebra
This appendix records the local algebra used by H4. The term canonical local projection” is only
shorthand for the concrete construction below.

E.1      The Finite Local Model
Let
                                                                       ∏︁
                        𝑤 = 𝑤(𝑁 ) → ∞,        𝑤 = 𝑜(log 𝑁 ),      𝑄=         𝑝.
                                                                       𝑝≤𝑤

      The local model of the von Mangoldt weight modulo 𝑄 is

                                                  𝑄
                                      Λ𝑄 (𝑎) =       1        .
                                                 𝜙(𝑄) (𝑎,𝑄)=1



                                                  19
   It has average value one on Z/𝑄Z. Define
                                           1 ∑︁
                               𝜎𝑄 (𝑁 ) =             Λ𝑄 (𝑎)Λ𝑄 (𝑁 − 𝑎).
                                           𝑄 𝑎 mod 𝑄
   The local Goldbach model at modulus 𝑄 is

                                     Loc𝑄 𝑅Λ (𝑁 ) = 𝑁 𝜎𝑄 (𝑁 ).
   Endpoint and smooth-partition discrepancies are already Edge errors in C1 and are 𝑜(𝑁 ).

E.2    Tagged-Cell Projection
The exact B1 decomposition and the F3 tagged partition give a finite tagged identity
                                             ∑︁          ∑︁
                                 𝑅Λ (𝑁 ) =        𝑐ℬ              𝑅ℬ,𝜏 (𝑁 ),
                                              ℬ        𝜏 ∈𝒯 (ℬ)
   where ℬ is the parent B1 block and 𝜏 is the complete routing tag of the terminal cell.
   For a tagged cell (ℬ, 𝜏 ), define

                                            Loc𝑄 𝑅ℬ,𝜏 (𝑁 )
   by replacing the arithmetic coefficients in that same tagged cell by their residue-class local
densities modulo 𝑄, while preserving:
  1. the parent B1 block ℬ;
  2. the routing tag 𝜏 ;
  3. the dyadic and smooth weights;
  4. the local congruence restrictions already present in the cell.
    This is a tag-preserving operation. It is not a branch-specific density and it does not identify
cells that merely have the same displayed algebraic shape.

E.3    H4 Admission Condition
A terminal local/main expression is admitted into H4 only if it satisfies

                               local
                              𝑀ℬ,𝜏   (𝑁 ) = Loc𝑄 𝑅ℬ,𝜏 (𝑁 ) + 𝑜ℬ,𝜏 (𝑁 ).                     (E-adm)
   The active sources are exactly:
  1. LongAP/Local main terms from D1;
  2. CKP zero-frequency terms from G8a together with B1LD;
  3. LocalDiag cells produced by the routing table;
  4. explicitly admitted local boundary terms whose discrepancy is already covered by C1.
    D1 verifies (E-adm) for LongAP/Local cells after excluding nonlocal coefficients. G8a verifies
it for CKP ℎ = 0 cells by identifying the zero Fourier mode with the same tagged local replace-
ment. LocalDiag cells are admitted only when the diagonal specialization remains a tagged local
projection; otherwise the routing table sends the cell to Edge, CKP, GoodAWACK, impossible, or
a continuing routed case.

                                                   20
E.4    Linearity Over the B1/F3 Partition
The operator Loc𝑄 is linear on the finite tagged decomposition:
                                         ⎛         ⎞
                                          ∑︁           ∑︁
                                    Loc𝑄 ⎝ 𝑐ℬ 𝑅ℬ,𝜏 ⎠ =    𝑐ℬ Loc𝑄 𝑅ℬ,𝜏 .
                                               ℬ,𝜏                 ℬ,𝜏

    Since B1 is an exact finite identity and F3 is an exact tagged partition, the tagged local pro-
jections reconstruct the local model of the original Goldbach convolution:
                  ∑︁          ∑︁
                       𝑐ℬ              Loc𝑄 𝑅ℬ,𝜏 (𝑁 ) = 𝑁 𝜎𝑄 (𝑁 ) + 𝑜(𝑁 ).                      (E-reconstruct)
                   ℬ        𝜏 ∈𝒯 (ℬ)

    Equivalently, applying the local replacement after the tagged proof-tree partition gives the same
local main term as applying Λ(𝑛) ↦→ Λ𝑄 (𝑛 mod 𝑄) directly to the two original von Mangoldt factors
in 𝑅Λ (𝑁 ).

E.5    No Double Counting
Local terms are indexed by (ℬ, 𝜏 ). If two terms have different parent B1 blocks, they are distinct
summands of the exact B1 identity. If they have the same parent block but different tags, F3.15
gives disjoint tagged cells.
    Thus two local-looking formulas may be algebraically identical and still be different summands;
they are recombined only through the tagged linear sum in (E-reconstruct). Conversely, a local-
looking expression without a parent B1 block and routing tag is not an H4 input. Hence H4 neither
double-counts nor loses admitted local/main terms.

E.6    Local Factors and the Singular Series
By the definition of Λ𝑄 ,

                                          1 ∑︁       𝑄             𝑄
                            𝜎𝑄 (𝑁 ) =                    1(𝑎,𝑄)=1     1           .
                                          𝑄 𝑎 mod 𝑄 𝜙(𝑄)          𝜙(𝑄) (𝑁 −𝑎,𝑄)=1

   Since 𝑄 is squarefree, the CRT gives
                                                              ∏︁
                                                 𝜎𝑄 (𝑁 ) =          𝜎𝑝 (𝑁 ),
                                                              𝑝≤𝑤

   where
                                               )︂2
                                1         𝑝
                                    (︂
                   𝜎𝑝 (𝑁 ) =                         #{𝑎 mod 𝑝 : (𝑎, 𝑝) = 1, (𝑁 − 𝑎, 𝑝) = 1}.
                                𝑝        𝑝−1
   For 𝑝 = 2 and even 𝑁 , 𝜎2 (𝑁 ) = 2. For odd 𝑝, the two forbidden residues are 0 and 𝑁 . Hence
                                                       ⎧    𝑝
                                                       ⎪
                                                       ⎪       ,           𝑝 | 𝑁,
                                                       ⎨   𝑝−1
                                         𝜎𝑝 (𝑁 ) =               1
                                                       ⎩1 −            ,   𝑝 ∤ 𝑁.
                                                       ⎪
                                                       ⎪
                                                              (𝑝 − 1)2
   Therefore



                                                              21
                                           ∏︁ (︂            1               𝑝
                                                                    )︂ ∏︁
                            𝜎𝑄 (𝑁 ) = 2             1−                         .
                                          3≤𝑝≤𝑤
                                                         (𝑝 − 1)2    3≤𝑝≤𝑤
                                                                           𝑝−1
                                           𝑝∤𝑁                            𝑝|𝑁

    Letting 𝑤 → ∞,
                                                      ∏︁ 𝑝 − 1
                                  𝜎𝑄 (𝑁 ) → 2𝐶2                  = S(𝑁 ),
                                                     𝑝|𝑁
                                                           𝑝−2
                                                     𝑝>2

    with
                                              ∏︁ (︂           1
                                                                     )︂
                                      𝐶2 =            1−            .
                                              𝑝>2
                                                           (𝑝 − 1)2

E.7     H4 Local Algebra Theorem
The admitted terminal local/main terms satisfy

                                    𝑀local (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
   Indeed, by the admission condition (E-adm), every active local/main term is a tagged local
projection up to 𝑜(𝑁 ). By tagged linearity and no double counting, the sum of these projections is
𝑁 𝜎𝑄 (𝑁 ) + 𝑜(𝑁 ). By the CRT factor computation, 𝜎𝑄 (𝑁 ) → S(𝑁 ). Thus the local/main assembly
contributes exactly the Goldbach singular series main term.


F     Parameter Hierarchy and Global Error Budget
F.1     Parameter Witness
The proof fixes parameters in a nonempty hierarchy. One explicit witness is
                                                    1              1
                                 𝐽0 = 20,         𝜂=  ,     𝜃=        .
                                                   40            4000
   For this witness 𝐽0 ≥ 𝐽* (𝜂). After 𝐽0 is fixed, all later logarithmic exponents are chosen in the
order recorded by GEB.

F.2     Multiplicity Principle
The B1/B3/F3/F4 process creates at most 𝐿𝐶0 terminal cells. Hence:

    1. 𝑂(𝑁 𝐿−𝐶0 −𝐴 ) per cell sums to 𝑂(𝑁 𝐿−𝐴 );

    2. 𝑂(𝑁 1−𝜌 𝐿𝐶 ) per cell sums to 𝑜(𝑁 );

    3. a normalized 𝑜(1) estimate remains 𝑜(1) after polylogarithmic testing-family losses, once the
       relevant logarithmic exponent is chosen large enough.

F.3     Global Loss Table




                                                      22
    Source                         Estimate                         Global conclusion
    B1 decomposition               exact identity                   no error
    F3/F4 routing                  exact tagged partition           no error
    Edge                           C1 strict saving                 𝑜(𝑁 )
    LongAP/Local                   LPI local projection plus Edge   local +𝑜(𝑁 )
                                   errors
    CKP excluded ranges            Edge/local/auxiliary routing     𝑜(𝑁 ) or local
    CKP central nonzero range      X10 after CKPD                   𝑜(𝑁 )
    GoodAWACK TC1 regular          X9L-GT after TTH                 𝑜(𝑁 )
    GoodAWACK singular             BRS/ROC rerouting                handled by existing branches
    X16/BRS carrier slice          Shiu/AP carrier estimate         Edge or 𝑜(𝑁 )
    HighTC/grammar                 E10Y/E10X/E10M/E10K              no residual
    LPI/H4 local projection        CRT local model                  S(𝑁 )𝑁 + 𝑜(𝑁 )




F.4    Consequence
After summing over the complete terminal partition,

                                    𝑅Λ (𝑁 ) = S(𝑁 )𝑁 + 𝑜(𝑁 ).
   No hidden terminal-family summation remains outside GEB.
   The prime-power removal is not a terminal branch summation. It is performed after I1 by G2,
which gives 𝑅Λ (𝑁 ) − 𝑅𝑝𝑝 (𝑁 ) = 𝑜(𝑁 ).


G     Dependency Ledger and Traceability
This appendix is auxiliary. It records how the manuscript layer maps to the proof-source layer.
File paths here are not part of the proof prose.

G.1    Main Logical Chain
                 𝑋1 + 𝐵1 + 𝐵3 + 𝐹 3 + 𝐹 4 + 𝐹 3𝑇 + 𝐸5 =⇒ terminal partition.


          𝐶1𝐴 + 𝐶1,     𝐷1 + 𝐻4,    𝐺8𝑎 + 𝑋10,       𝐸10𝐿 + 𝑋9𝐿 + 𝑋16,       𝐺𝐸𝐵 =⇒ 𝐼1.


                  𝐼1 + 𝐺2 + 𝐺1 + 𝐺0𝐻 =⇒ sufficiently-large binary Goldbach.

G.2    Source Map

      Manuscript item                                Active proof-source item
      X1                                             ../External/x_1_heath_brown_identity_verification_ltx.md
      X9L-GT                                         ../External/x_9l_gt_avg_polylog_verification_ltx.md
      X10                                            ../External/x_10_verification_ltx.md
      X16                                            ../External/x_16_divisor_sum_brs_verification_ltx.md
      B1                                             ../Lemmas/b_1_ltx.md
      B3                                             ../Lemmas/b_3_ltx.md


                                                23
      F3P/F3                                         ../Lemmas/f3_intrinsic_terminal_predicate_catalogue_ltx.md
                                                     ../Lemmas/f_3_ltx.md
      F3T                                            ../Lemmas/f3_complete_routing_exhaustion_ltx.md
      F4                                             ../Lemmas/f_4_ltx.md
      E5                                             ../Lemmas/e_5_ltx.md
      C1A                                            ../Lemmas/c1_edge_admission_ledger_ltx.md
      C1                                             ../Lemmas/c_1_ltx.md
      D1                                             ../Lemmas/d_1_ltx.md
      H4                                             ../Lemmas/h_4_ltx.md
      CKPD                                           ../Lemmas/ckp_x10_smooth_weight_derivative_appendix_ltx.md
      G8a                                            ../Lemmas/g_8_a_ltx.md
      TC1/TNG                                        ../Lemmas/tc1_measured_fourier_transfer_ltx.md,
                                                     ../Lemmas/tc1_structural_coarea_closure_ltx.md,
                                                     ../Lemmas/tc1_near_global_chain_ltx.md
      BRS/ROC/TTH                                    ../Lemmas/b1_range_skeleton_roc_slice_ltx.md,
                                                     ../Lemmas/tc1_singular_origin_roc_ltx.md,
                                                     ../Lemmas/tc1_theta_1_3_ltx.md
      X16C/X16BRS                                    ../Lemmas/x16_core_shiu_ap_proof_ltx.md,
                                                     ../Lemmas/x16_brs_carrier_slice_ltx.md
      E10Y                                           ../Lemmas/e10y_goodawack_routing_grammar_completeness_ltx.
      E10X                                           ../Lemmas/e10_master_source_exhaustion_closure_ltx.md
      E10M/E10K/E10L                                 ../Lemmas/e10m_no_untagged_rank_dropping_aff_ltx.md,
                                                     ../Lemmas/e10k_aff_oc_affine_regrouping_origin_completenes
                                                     ../Lemmas/e10l_e10_clean_branch_b_ltx.md;
                                                     ../Lemmas/e10m_source_exhaustion_verification_ltx.md
                                                     is a non-logical source-maintenance record
      GEB                                            ../Lemmas/global_error_budget_ltx.md
      I1                                             ../Lemmas/i_1_ltx.md
      G2                                             ../Lemmas/g_2_ltx.md
      G1                                             ../Lemmas/g_1_ltx.md
      G0H                                            ../Lemmas/g0_final_handoff_verification_ltx.md
      Proof ledger                                   ../Proof tree and
                                                     ledger/g_proof_tree_n_ldg.md




G.3    Synchronization Rule
If an active source file listed above changes, then the corresponding manuscript section or appendix
must be checked before any LaTeX regeneration. Any mathematical correction to a manuscript
passage must be made first in the active proof-source file and only then propagated into this
manuscript layer.


References
 [1] Tenenbaum, Gerald. Introduction to Analytic and Probabilistic Number Theory. American
     Mathematical Society. vol. 163. 2015. Ch. II.5, Theorem 5 is used for fixed divisor-function
     second moments..

 [2] Davenport, Harold. On some infinite series involving arithmetical functions (II). The Quarterly
     Journal of Mathematics. vol. os-8. no. 1. pp. 313–320. 1937. doi: 10.1093/qmath/os-8.1.313.

                                                24
   Classical source for the near-global Liouville exponential-sum input; the active formulation is
   recorded in X9L-GT..

[3] Heath-Brown, D. R.. Prime numbers in short intervals and a generalized Vaughan
    identity. Canadian Journal of Mathematics. vol. 34. no. 6. pp. 1365–1377. 1982. doi:
    10.4153/CJM-1982-095-9. Source for the fixed-depth Heath–Brown identity used in X1/B1..

[4] Shiu, P.. A Brun–Titchmarsh theorem for multiplicative functions. Journal für die reine und
    angewandte Mathematik. vol. 313. pp. 161–170. 1980. doi: 10.1515/crll.1980.313.161.
    Source for the Shiu AP divisor-average input used in X16C..

[5] Duke, William and Friedlander, John B. and Iwaniec, Henryk. Bilinear forms with
    Kloosterman fractions. Inventiones Mathematicae. vol. 128. no. 1. pp. 23–43. 1997. doi:
    10.1007/s002220050135. Active CKP/X10 input: Theorem 2 with the smooth-weight for-
    mulation..

[6] Deshouillers, Jean-Marc and Iwaniec, Henryk. Kloosterman sums and Fourier coefficients of
    cusp forms. Inventiones Mathematicae. vol. 70. no. 2. pp. 219–288. 1982. Background source
    for classical Kloosterman-sum technology; the active CKP/X10 theorem is Duke–Friedlander–
    Iwaniec..




                                              25
