﻿              H4 Local Algebra Independent Theorem Package
                               Denis Saltykov (ds1678@gmail.com)

                                             May 2026


Contents
1 Abstract                                                                                           2

2 Introduction and Statement of Results                                                              2
  2.1 Purpose of the Package . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     2
  2.2 Package Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    2
       2.2.1 Theorem H4-Local-Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . .        2
  2.3 What This Package Imports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      2

3 Parameters, Notation, and Error Bookkeeping                                                        2

4 External Analytic Inputs                                                                           3
  4.1 CRT and Euler-product algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      3
  4.2 B1LD compatibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     3
  4.3 No hidden analytic estimate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .    4

5 Full Proof Body                                                                               4
  5.1 Part 1. D1: LongAP/Local local-coefficient expansion and projection . . . . . . . . . 4
  5.2 Part 2. B1LD: B1 local-density compatibility . . . . . . . . . . . . . . . . . . . . . . 12
  5.3 Part 3. H4: Tagged local algebra and singular series . . . . . . . . . . . . . . . . . . 13

6 Package Dependency Ledger and Synchronization Notes                                                24
  6.1 Compact Package Dependency Graph . . . . . . . . . . . . . . . . . . . . . . . . . .           24
  6.2 Local Ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .   24
  6.3 Synchronization Boundary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     24

7 Bibliography                                                                                       24

8 References                                                                                         25




                                                  1
1     Abstract
This package gives the local-main algebra brick used by the modular Goldbach proof. It proves
that every LPI-admitted LongAP/Local, CKP zero-frequency, and LocalDiag contribution is an
explicit tagged О›рќ‘„ -local projection, that the tagged projections do not double count, and that their
finite local factors converge to the Goldbach singular series S(рќ‘Ѓ ).


2     Introduction and Statement of Results
2.1     Purpose of the Package
The H4 package isolates the local/main algebra from the analytic estimates. It does not prove that
every terminal atom is local; this admission is supplied by the routing and branch packages. Its
responsibility is narrower and checkable: once a tagged atom is admitted to the local model, H4
proves that the atom contributes through the same О›рќ‘„ -projection and that the sum of all admitted
tagged projections is

                                          S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).

2.2     Package Theorem
2.2.1    Theorem H4-Local-Algebra
Assume the common B1/F3 tagged partition and the branch-admission statements imported from
the other theorem packages. Then all LPI-admitted local/main pieces satisfy

            рќ‘Ђlocal (рќ‘Ѓ ) = рќ‘ЂLongAP (рќ‘Ѓ ) + рќ‘ЂCKP,0 (рќ‘Ѓ ) + рќ‘ЂLocalDiag (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   There is no fourth local summand. Auxiliary local-looking terms produced by controlled CRT
absorption, fixed-divisor quotienting, or primitive local slicing are tagged refinements of one of the
three displayed classes. Endpoint and smooth-boundary localizations are C1 Edge errors.

2.3     What This Package Imports
    1. The exact B1/F3 tagged partition from the final modular assembly package.

    2. The statement that LongAP/Local atoms reaching H4 satisfy D1 admission.

    3. The statement that CKP zero-frequency terms reach H4 through B1LD/G8a.

    4. The statement that LocalDiag terms are admitted only as tagged LPI local projections later
       assembled by H4.


3     Parameters, Notation, and Error Bookkeeping
Throughout рќ‘Ѓ is an even integer tending to infinity and рќђї = log рќ‘Ѓ . This package uses the common
fixed depth рќђЅ0 and the common tagged dyadic partition from PAR. Its local parameters are:


        Parameter
            в€ЏпёЂ                                        Local use
        рќ‘„ = рќ‘ќв‰¤рќ‘¤ рќ‘ќ                                     finite local modulus



                                                  2
       рќ‘¤ = рќ‘¤(рќ‘Ѓ )                                        tends to infinity with рќ‘¤ = рќ‘њ(log рќ‘Ѓ )
                   рќ‘„
       О›рќ‘„ (рќ‘Ћ) = рќњ™(рќ‘„)  1(рќ‘Ћ,рќ‘„)=1                          local von Mangoldt model
       tagged cell (в„¬, рќњЏ )                              no-double-counting unit




    All H4 errors are either explicit рќ‘њ(рќ‘Ѓ ) errors inside the local projection limit or branch errors
already charged to GEB before H4 receives the term.
    The local bookkeeping has three separate layers.

    1. The routing layer supplies the admission tag. H4 never creates a new branch class; it only
       receives terms already certified as LongAP/Local, CKP zero-frequency, or LocalDiag. Con-
       trolled CRT absorption, fixed-divisor quotienting, and primitive local slicing are finite refine-
       ments of those source classes, while endpoint and smooth-boundary localizations are C1 Edge
       errors.

    2. The tagged-cell layer records the finite B1/F3 partition cell (в„¬, рќњЏ ). Every local projection in
       this package is attached to exactly one such tag, so the later summation over tags is disjoint.

    3. The finite-local layer passes from рќ‘„-local densities to the limiting singular series. The only
       limiting operation inside H4 is рќ‘¤ в†’ в€ћ in the Euler product after the tagged finite projections
       have been summed.

    The local summand notation is exhaustive: the only main terms assembled by H4 are рќ‘ЂLongAP ,
рќ‘ЂCKP,0 , and рќ‘ЂLocalDiag . A local-looking object without one of these tags is either a finite refinement
of its parent source class or a C1 error; it is not an independent main term outside the tagged О›рќ‘„ -
projection.


4     External Analytic Inputs
This package uses no deep external analytic estimate. Its title section is kept as "External Ana-
lytic Inputs" only to match the common theorem-package contract. The content of this section is
therefore a negative analytic input statement plus the elementary local algebra used by H4.

4.1    CRT and Euler-product algebra
H4 uses the Chinese remainder theorem to factor the finite local density attached to

                                                    рќ‘„
                                        О›рќ‘„ (рќ‘Ћ) =       1        .
                                                   рќњ™(рќ‘„) (рќ‘Ћ,рќ‘„)=1
   The local factor at a prime рќ‘ќ в‰¤ рќ‘¤ counts the admissible residue pairs (рќ‘Ћ, рќ‘Ѓ в€’ рќ‘Ћ) modulo рќ‘ќ.
Multiplying the prime factors gives the finite Goldbach local factor. Letting рќ‘¤ в†’ в€ћ gives the
standard singular series S(рќ‘Ѓ ).

4.2    B1LD compatibility
The only nontrivial internal compatibility input used by this package is B1LD: the finite-convolution
local densities produced by the B1 decomposition agree with the H4 О›рќ‘„ -projection after the common
tag is fixed. This is what allows CKP zero-frequency and LongAP/Local local terms to be collected
by the same LPI projection.

                                                    3
4.3    No hidden analytic estimate
There is no appeal here to DFI/X10, X9L-GT, Shiu/AP, or any short-interval prime estimate.
Those estimates enter other theorem packages before a term is admitted to H4, or are irrelevant to
this local algebra package.


5     Full Proof Body
The following proof-source files are included in full.

    1. Lemmas/d_1_ltx.md вЂ“ LongAP/Local local-coefficient expansion and projection

    2. Lemmas/g8a_local_density_ltx.md вЂ“ B1 local-density compatibility

    3. Lemmas/h_4_ltx.md вЂ“ Tagged local algebra and singular series

5.1    Part 1. D1: LongAP/Local local-coefficient expansion and projection
Source file: Lemmas/d_1_ltx.md.

D1. LongAP/Local Normalization Lemma

D1.0. Role Logical ID: D1.
    Used by: H4, I1.
    Uses: B1, B3, F3P, F3, F3T, F4, C1A, C1, E5, LPI, and standard smooth AP/local counting.
    Lemma D1 is responsible for the LongAP/Local branch of the proof tree. D1 proves that Lon-
gAP/Local terms enter the local assembly through the independent LPI local projection interface:
the same tagged cell is projected by the replacement О›(рќ‘›) в†¦в†’ О›рќ‘„ (рќ‘› mod рќ‘„), with parent B1 block,
routing tag, dyadic weights, and local congruence data preserved. The downstream H4 assembly
consumes only local/main terms that satisfy the LPI-admissible form

                                 local
                                рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
    Therefore D1 proves

                               LongAP              LongAP
                              рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ )

   for every tagged LongAP/Local atom \{}((\{}mathcal B,\{}tau) \{}).
   In other words, D1 does not merely evaluate a local AP sum; it proves that its main term has
exactly the same normalization as the LPI local model later assembled by H4.
   вЂ”

D1.1. Tagged LongAP/Local atom               Let (в„¬, рќњЏ ) be a tagged LongAP/Local atom obtained
after

                                        рќђµ1 в†’ рќђµ3 в†’ рќђ№ 3/рќђ№ 4.
   By the intrinsic LongAP/Local predicate in Lemma F3P, such an atom has the following positive
properties:



                                                  4
  1. it is a long AP or a finite union of controlled long AP fibres;

  2. there is a controlled modulus рќ‘„рќњЏ в‰¤ (log рќ‘Ѓ )рќђ¶ ;

  3. every coefficient depending on the long AP variable belongs to the local coefficient algebra
     Cloc (рќ‘„рќњЏ );

  4. all remaining restrictions are controlled local congruence / AP restrictions;

  5. all local terms preserve the parent B1 block tag в„¬ and the routing tag рќњЏ .

   In particular all moduli are controlled:

                                              рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ ;
   A model tagged LongAP/Local atom has the form
                        LongAP
                               (рќ‘Ѓ ) =            рќ‘Љв„¬,рќњЏ (рќ‘Ґ)1рќђґ(рќ‘Ґ)в‰Ўрќ‘Џ    (mod рќ‘ћ) рќњЊрќ‘„ (рќ‘Ґ),
                                         в€‘пёЃ
                       рќ‘…в„¬,рќњЏ
                                        рќ‘Ґв€€О©в„¬,рќњЏ

   where:

  вЂў \{}(\{}Omega_{\{}mathcal B,

   \{}tau} \{}) is a smooth tagged box/fibre;

  вЂў \{}(W_{\{}mathcal B,

   \{}tau} \{}) is a smooth dyadic weight;

  вЂў рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ ;

  вЂў \{}(\{}rho_Q(x)

   \{}) denotes the finite product of local coprimality/residue constraints inherited from the B1
coefficients and the Goldbach equation;

  вЂў no nonlocal coefficient such as рќњ†(рќђї(рќ‘Ґ)), рќњ‡(рќђї(рќ‘Ґ)), a nonlocal finite-convolution factor, or a
    CKP oscillatory phase remains.

   The exclusion of such factors is a consequence of the positive F3P LongAP/Local predicate,
not an analytic assumption made inside D1. Lemma D1.2A records the consequence in the form
needed for local AP counting.
   вЂ”

D1.2. LPI local model recalled         In Lemma LPI, choose

                       рќ‘„=               рќ‘¤ = рќ‘¤(рќ‘Ѓ ) в†’ в€ћ,             рќ‘¤ = рќ‘њ(log рќ‘Ѓ ).
                             в€ЏпёЃ
                                  рќ‘ќ,
                            рќ‘ќв‰¤рќ‘¤

   The local von Mangoldt model is

                                                   рќ‘„
                                       О›рќ‘„ (рќ‘Ћ) =       1        .
                                                  рќњ™(рќ‘„) (рќ‘Ћ,рќ‘„)=1


                                                    5
   For every tagged atom, the LPI local projection is defined as

                                            Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ )
  by replacing the arithmetic coefficients in the tagged atom by their local residue-class densities
modulo рќ‘„, while keeping:

  вЂў the same tag \{}((\{}mathcal B,

   \{}tau) \{});

  вЂў the same smooth/dyadic weights;

  вЂў the same local congruence restrictions;

  вЂў the same finite routing cell.

   Lemma D1 identifies the LongAP main term with exactly this object.
   вЂ”

D1.2A. F3P consequence for LongAP/Local coefficients

Lemma 5.1 (Lemma D1.2A. No nonlocal arithmetic coefficient survives in LongAP/Local). Let
(в„¬, рќњЏ ) be a terminal atom produced by the B1/B3/F3/F4 routing tree and tagged as LongAP/Local.
Then every coefficient which still depends on a long AP variable is local in the following sense: after
refining by a controlled modulus рќ‘„рќњЏ в‰¤ (log рќ‘Ѓ )рќђ¶ , it is a finite linear combination of residue-class
and coprimality indicators modulo рќ‘„рќњЏ , multiplied by smooth dyadic weights and tag constants. In
particular, no terminal LongAP/Local atom contains a surviving factor of the form
                                                                     (пёѓ     )пёѓ
                                                                      рќ‘рќђї(рќ‘ў)
                       рќњ‡(рќђї(рќ‘ў)),      рќњ†(рќђї(рќ‘ў)),       рќ‘’(рќ›јрќђї(рќ‘ў)),       рќ‘’       ,
                                                                        рќ‘ћ
    or any finite-convolution descendant of these which is not determined by the controlled local
residue data.

Proof. The proof is the direct consequence of the intrinsic predicate catalogue F3P, together with
the F3/F4 exhaustion of unresolved obstructions.
   By F3P.7, a terminal LongAP/Local atom satisfies

                                       рќ’Іlong (в„¬, рќњЏ ) вЉ‚ Cloc (рќ‘„рќњЏ )
    for a controlled modulus рќ‘„рќњЏ в‰¤ (log рќ‘Ѓ )рќђ¶ . Expanding the generators of Cloc (рќ‘„рќњЏ ) gives a finite
linear combination of smooth dyadic weights, tag constants, residue-class indicators, coprimality
indicators, and fixed controlled-divisor factors. This proves the asserted local form.
    It remains only to justify that a forbidden nonlocal coefficient could not have received a Lon-
gAP/Local terminal tag. This is not a downstream estimate; it is the intrinsic terminal-labelling
rule.
    B3 preliminary classification. Lemma B3 records a LongAP/Local candidate only when,
after fixing the auxiliary variables, the remaining counting problem is a controlled AP/local count
with smooth weights and no nonlocal oscillatory arithmetic coefficient. If a Mobius-, Liouville-,
or other nonlocal central-long coefficient remains, B3 records a BranchB/GoodAWACK candidate
unless a CKP-balanced grouping or a forced LocalDiag dependence has already been detected.

                                                   6
    F3P/F3 terminal predicate. Lemma F3P makes the LongAP/Local predicate a positive
local-coefficient condition. Hence a cell with a surviving рќњ‡-, рќњ†-, Kloosterman-, Fourier-, reciprocal,
finite-convolution, or nilsequence-type oscillation cannot be terminally labelled LongAP/Local at
the F3 stage. The remaining routing alternatives are:

      Surviving feature                                               Routing consequence
      рќњ‡(рќђї), рќњ†(рќђї), or affine finite-convolution oscillation at-        GoodAWACK, unless CKP or LocalDiag applies first
      tached to a long variable
      balanced multiplicative or reciprocal-phase structure           CKP
      strict saving predicate, short residual volume, bound-          Edge through C1P/C1A/C1
      ary, high frequency, or small conductor
      forced equality, proportionality, repeated factor, or lo-       LocalDiag
      cal dependence
      only controlled residue-class / coprimality data mod-           admissible LongAP/Local
      ulo (log рќ‘Ѓ )рќђ¶




    F4 divisor and quotient decisions. Ordinary divisor or quotient conditions are not allowed
to remain unresolved inside LongAP/Local. Lemma F4 routes such a condition to Edge, LocalDiag,
CKP, or GoodAWACK, or absorbs a controlled fixed divisor with strict decrease of the F3 measure.
If after such absorption only controlled local congruence data remain, the later terminal cell may
be LongAP/Local. If a nonlocal divisor/quotient coefficient remains, the cell is routed by F4 and
is not D1-admissible.
    Controlled CRT and local restrictions. Lemma E5 and the F3 controlled CRT steps may
replace a full-rank finite-index restriction by residue-class data with controlled content. These
operations do not convert a nonlocal arithmetic function into a local density. They only record
congruence and coprimality conditions modulo controlled moduli. If the modulus or conductor is
not controlled, the cell is routed to Edge, CKP, LocalDiag, or F4 rather than to D1.
    The routing measure in Lemma F3 is well-founded; Lemma F3T records the same finite case
distinction as a synchronized table for the proof tree. Therefore the process terminates. At a
terminal LongAP/Local tag, the positive F3P predicate has already forced every long-variable
coefficient into Cloc (рќ‘„рќњЏ ). Lemma proved.
    вЂ”


D1.3. Pure local AP counting lemma

Lemma 5.2 (Lemma D1.1. Smooth AP count with controlled modulus). Let \{}(W\{}in C_cЛ†\{}infty(\{}mathbb
R) \{}), and let

                                                                             рќ‘ў
                                                                        (пё‚       )пё‚
                                                   рќ‘Љрќ‘€ (рќ‘ў) = рќ‘Љ                         .
                                                                             рќ‘€
   For a controlled modulus

                                                       рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ ,
   and a residue class рќ‘џ (mod рќ‘ћ), we have
                                              1 в€‘пёЃ
                                 рќ‘Љрќ‘€ (рќ‘ў) =          рќ‘Љрќ‘€ (рќ‘ў) + рќ‘‚рќђґ (рќ‘€ (log рќ‘Ѓ )в€’рќђґ ) + рќ‘‚рќђґ ((log рќ‘Ѓ )рќђґ )
                      в€‘пёЃ

                рќ‘ўв‰Ўрќ‘џ    (mod рќ‘ћ)
                                              рќ‘ћ рќ‘ў



                                                                  7
    after smoothing and boundary truncation, with the total boundary contribution routed to the C1
predicates E1/E6.
    In particular, when this estimate is inserted into a tagged LongAP atom with total volume в‰Ќ рќ‘Ѓ ,
the error is

                                                    рќ‘њ(рќ‘Ѓ )
   after summing over polylogarithmically many local moduli and tags.

Proof. The assertion follows from the exact finite Fourier expansion of the residue class:

                                                   1 в€‘пёЃ        в„Ћ(рќ‘ў в€’ рќ‘џ)
                                                               (пё‚           )пё‚
                              1рќ‘ўв‰Ўрќ‘џ   (mod рќ‘ћ) =               рќ‘’          .
                                                   рќ‘ћ в„Ћ mod рќ‘ћ      рќ‘ћ

   The zero frequency gives
                                                1 в€‘пёЃ
                                                     рќ‘Љрќ‘€ (рќ‘ў).
                                                рќ‘ћ рќ‘ў
   For в„Ћ Мё= 0, smoothness and summation by parts give decay faster than any power of рќ‘ћ/рќ‘€ . Since
рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ and the LongAP direction has length at least a fixed power of рќ‘Ѓ , the nonzero finite
Fourier terms are negligible. Boundary discrepancies are smooth dyadic boundary terms and satisfy
the C1 admission predicates E1/E6.
   Lemma proved.
   вЂ”


D1.4. Local residue density and LPI tagged projection                     The LongAP/Local atom has only
controlled local congruence data. After refining modulo

                                       рќ‘„вЂІ = lcm(рќ‘„, рќ‘ћ1 , . . . , рќ‘ћрќ‘љ ),
   where all extra local moduli satisfy

                                               рќ‘ћрќ‘– в‰¤ (log рќ‘Ѓ )рќђ¶ ,
   we still have

                                          рќ‘„вЂІ = рќ‘„ В· (log рќ‘Ѓ )рќ‘‚(1)
   up to harmless overlap in prime factors.
   The local main term obtained by repeated use of Lemma D1.1 is

                                                                      Vol(О©в„¬,рќњЏ )
                         (рќ‘Ѓ ) =              рќ›їв„¬,рќњЏ (рќ‘Ћ; рќ‘Ѓ )wв„¬,рќњЏ (рќ‘Ћ) В·              + рќ‘њ(рќ‘Ѓ ),
                                     в€‘пёЃ
                     D1
                    рќ‘Ђв„¬,рќњЏ
                                  рќ‘Ћ mod рќ‘„вЂІ
                                                                         рќ‘„вЂІ

   where:

  вЂў \{}(\{}delta_{\{}mathcal B,

   \{}tau}(a;N) \{}) records the tagged local congruence constraints;

  вЂў \{}(\{}mathfrak w_{\{}mathcal B,

                                                      8
    \{}tau}(a) \{}) is the product of local densities of the B1 arithmetic coefficients in that residue
class;
  вЂў the smooth volume is the same as in the original tagged atom.
   But this is exactly the definition of
                                                 LongAP
                                           Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ )
   from Lemma LPI, because both objects are obtained by:

  1. keeping the same parent tag \{}((\{}mathcal B,

   \{}tau) \{});
  1. keeping the same smooth cell;

  2. replacing arithmetic coefficients by their local residue-class densities;

  3. averaging over the same controlled local congruence data.
   Therefore
                                                 LongAP
                                D1
                               рќ‘Ђв„¬,рќњЏ (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   вЂ”

D1.5. No hidden nonlocal estimates              D1 explicitly excludes the following from the Lon-
gAP/Local class:

  1. PNT-in-AP input;

  2. BombieriвЂ“Vinogradov type cancellation;

  3. Mobius/Liouville cancellation;

  4. nilsequence orthogonality;

  5. CKP oscillatory phases;

  6. nonzero Fourier phases not already routed to C1/G8a.

   If a tagged atom contains a factor of the form

                                                                рќ‘рќ‘Ћ
                                                                   (пё‚   )пё‚
                                рќњ†(рќђї(рќ‘ў)),       рќњ‡(рќђї(рќ‘ў)),        рќ‘’     ,
                                                                 рќ‘ћ
   or any nonlocal oscillatory coefficient, then it is not D1-admissible. It must be routed to one of:

                        GoodAWACK,           CKP,         Edge,         LocalDiag
   by B3/F3/F4/C1/G8a/E10.
   Lemma D1.2A proves this exclusion from the intrinsic F3P LongAP/Local predicate plus the
F3/F4 routing alternatives. Thus D1 remains a pure local counting lemma: it never invokes
cancellation of Mobius, Liouville, nilsequence, Kloosterman, or nonzero Fourier coefficients.
   вЂ”

                                                  9
D1.6. Boundary and endpoint errors             The local AP count produces endpoint and smoothing
errors. These have one of the forms:

                                              рќ‘‚((log рќ‘Ѓ )рќђ¶ )
   per fibre, or boundary mass

                                 в‰¤ рќ‘Ѓ рќњЂ(рќ‘Ѓ ),          рќњЂ(рќ‘Ѓ )(log рќ‘Ѓ )рќђ¶ в†’ 0.
   By Lemma C1, such errors are routed to:

                                      рќђё1 : boundary/dyadic tail,
   or

                                      рќђё6 : short residual volume,
   or, when a short Type-I error is involved,

                                 рќђё7 : Type I short-variable error.
   Therefore the total D1 error is

                                                 рќ‘њ(рќ‘Ѓ )
   after polylogarithmic summation over tags.
   вЂ”

D1.7. Tag preservation       Every D1 operation preserves the tag

                                                 (в„¬, рќњЏ ).
   The AP count is performed inside a fixed tagged cell. It does not merge cells from different
parent B1 blocks and does not identify visually similar local terms from different routing histories.
   Therefore the D1 local main terms preserve the tag separation later used by the no-double-
counting mechanism of Lemma H4:

                                     рќ‘Ђlocal (рќ‘Ѓ ) =                   (рќ‘Ѓ ).
                                                     в€‘пёЃ
                                                               local
                                                           рќ‘ђв„¬ рќ‘Ђв„¬,рќњЏ
                                                     в„¬,рќњЏ
   вЂ”

D1.8. D1 theorem

Theorem 5.3 (Theorem D1). Let \{}((\{}mathcal B, \{}tau) \{}) be a terminal LongAP/Local
atom produced by the routing tree. Then
                              LongAP              LongAP
                             рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   Consequently, summing over all tagged LongAP/Local atoms,

                          рќ‘…LongAP/Local (рќ‘Ѓ ) = рќ‘ЂLongAP/Local (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ),
   where

                                                     10
                                                                        LongAP
                    рќ‘ЂLongAP/Local (рќ‘Ѓ ) =                       рќ‘ђв„¬ Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ).
                                                 в€‘пёЃ

                                           в„¬,рќњЏ в€€LongAP/Local
   Thus every D1 local term is LPI-admissible and therefore ready for the H4 assembly.
Proof. Fix a tagged terminal LongAP/Local atom \{}((\{}mathcal B, \{}tau) \{}). By Lemma
D1.2A, all remaining arithmetic restrictions are controlled local AP/congruence conditions with
moduli в‰¤ (log рќ‘Ѓ )рќђ¶ , and no nonlocal oscillatory factor remains.
    Apply the smooth AP counting lemma to the long AP directions. The zero/local part gives the
average over the corresponding residue classes modulo the controlled local modulus. Refining these
local conditions with the LPI modulus рќ‘„ gives exactly the tagged LPI projection \{}(\{}operator-
name{Loc}_Q R_{\{}mathcal B, \{}tau}Л†{\{}mathrm{LongAP}}(N) \{}), namely the explicit
О›рќ‘„ -local replacement inside the same B1/F3 cell. Boundary and endpoint discrepancies are C1
Edge errors and contribute рќ‘њ(рќ‘Ѓ ).
    All operations are performed inside the fixed tag \{}((\{}mathcal B, \{}tau) \{}), so no lo-
cal terms are merged or double-counted. Summing over the polylogarithmic number of tagged
LongAP/Local atoms preserves the \{}(o(N) \{}) error.
    The theorem is proved.
    вЂ”


D1.9. Interface refinements      The D1 statement used in the proof is:

                                             LongAP
                               рќ’њ(рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ    (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ )
   for every tagged LongAP/Local atom.
   Thus:
  1. D1 local terms satisfy the LPI admission condition consumed by H4;
  2. D1 does not hide nonlocal cancellation estimates;
  3. all local AP normalizations are compatible with \{}(\{}Lambda_Q(a)=Q/\{}varphi(Q)1_{(a,Q)=1}
   \{});
  1. all boundary/endpoint errors are routed to C1;
  2. parent B1 and routing tags are preserved.
   вЂ”
Remark 5.4 (D1.10. Output).

     Every tagged LongAP/Local atom equals its LPI canonical local projection plus рќ‘њ(рќ‘Ѓ ).
   D1 contains no hidden nonlocal cancellation; boundary and endpoint errors are routed to C1;
parent B1 and routing tags are preserved.
   Consequences:
  вЂў the LPI admission condition is discharged for LongAP/Local terms;
  вЂў together with G8a, all major local/main sources are LPI-admissible;
  вЂў the remaining external checks are outside D1.

                                                  11
D1.11. Logical Dependencies            Internal dependencies: B1, B3, F3, F3T, F4, C1A, C1, E5, LPI.
  Children served: H4 and I1.

5.2   Part 2. B1LD: B1 local-density compatibility
Source file: Lemmas/g8a_local_density_ltx.md.

B1LD. Local Densities for B1-Inherited CKP Coefficients

B1LD.0. Role Logical ID: B1LD.
    Used by: G8a, H4.
    Uses: B1, C1, and finite CRT local algebra.
    This file supplies the local-density interface used in G8a.5. The issue is not that the B1 coeffi-
cients are literally the von Mangoldt function; they are finite-convolution pieces coming from the
exact HeathвЂ“Brown decomposition. The point is that the LPI canonical local projection Locрќ‘„ is
defined tagwise for those very same finite-convolution coefficients, and CRT local density algebra
is compatible with the exact B1 decomposition.
    вЂ”

                                                                               Let рќ‘„ =         рќ‘ќв‰¤рќ‘¤ рќ‘ќ be squarefree. For
                                                                                          в€ЏпёЂ
B1LD.1. Local model of an elementary B1 coefficient
an elementary coefficient sequence рќ‘Ћ(рќ‘›) of B1 type

                                       рќњ‡(рќ‘›)1рќ‘›в‰¤рќ‘¦ ,            1,       log рќ‘›,
   with a fixed smooth dyadic cutoff, define its local residue model modulo рќ‘„ by
                                            1
                 рќ‘Ћрќ‘„ (рќ‘џ; рќ‘„) =                                                          рќ‘Ћ(рќ‘›)рќ‘Љрќ‘‹ (рќ‘›),
                                                                            в€‘пёЃ
                               |{рќ‘› в€ј рќ‘‹ : рќ‘› в‰Ў рќ‘џ        (mod рќ‘„)}|          рќ‘›в€јрќ‘‹
                                                                      рќ‘›в‰Ўрќ‘џ (mod рќ‘„)

    with the usual empty-class convention. Partial summation handles the log рќ‘› coefficient, the
constant coefficient is immediate, and the рќњ‡-coefficient is local because on a squarefree modulus its
residue constraints factor prime-by-prime by CRT. Boundary errors from the smooth dyadic cutoff
are C1 Edge errors.
    Thus every elementary B1 coefficient has a well-defined finite local model modulo рќ‘„, with errors
рќ‘њ(1) after the standard choice рќ‘¤ = рќ‘њ(log рќ‘Ѓ ).
    вЂ”

B1LD.2. Finite convolution compatibility Let в„¬ be a typed B1 dyadic block. Its coefficient
is a finite Dirichlet-convolution expression in elementary factors of the three types above. For a
residue class рќ‘џ mod рќ‘„, the local model of the product constraint is the finite CRT convolution

                       рќњЊв„¬,рќ‘„ (рќ‘џ) =                           рќ‘Ћ1,рќ‘„ (рќ‘џ1 ; рќ‘„) В· В· В· рќ‘Ћрќ‘,рќ‘„ (рќ‘џрќ‘ ; рќ‘„).               (B1-local)
                                             в€‘пёЃ

                                    рќ‘џ1 В·В·В·рќ‘џрќ‘ в‰Ўрќ‘џ   (mod рќ‘„)

   Because рќ‘„ is squarefree, CRT gives a product over primes рќ‘ќ в‰¤ рќ‘¤:

                                      рќњЊв„¬,рќ‘„ (рќ‘џ) =            рќњЊв„¬,рќ‘ќ (рќ‘џ mod рќ‘ќ).
                                                     в€ЏпёЃ

                                                    рќ‘ќв‰¤рќ‘¤




                                                       12
   This is a finite algebraic identity for the local models. It does not require any prime distribution
theorem.
   вЂ”

B1LD.3. Compatibility with Locрќ‘„ The LPI canonical local projection of a tagged atom is
defined by replacing each arithmetic coefficient in that tagged atom by its local residue-class model
modulo рќ‘„, while keeping the same smooth dyadic weights, routing tag, and linear/congruence
constraints.
    For a tagged CKP atom (в„¬, рќњЏ ), the outer coefficient sequences рќ›јрќ‘” (рќ‘Ћ) and рќ›ѕрќ‘” (рќ‘ћ) are restrictions,
gcd-splits, and dyadic localizations of B1 finite-convolution coefficients. Therefore their local models
are exactly the corresponding restrictions of рќњЊв„¬,рќ‘„ . The operations involved are finite CRT restric-
tion, gcd splitting, and fixed dyadic localization; each commutes with the finite local convolution
(B1-local), up to C1 boundary terms.
    Hence the local densities used in
                                             Locрќ‘„ рќ‘…в„¬,рќњЏ
                                                    CKP
                                                        (рќ‘Ѓ )
are precisely the local densities of the B1-inherited CKP coefficients that appear in the в„Ћ = 0 term
of G8a.
    вЂ”

B1LD.4. Lemma Lemma B1-LD. For every tagged CKP atom (в„¬, рќњЏ ), the local-density re-
placement used by LPI for Locрќ‘„ рќ‘…в„¬,рќњЏ  CKP (рќ‘Ѓ ) is the CRT finite-convolution local model of the B1-

inherited coefficient sequences рќ›јрќ‘” (рќ‘Ћ), рќ›ѕрќ‘” (рќ‘ћ), and the fibre coefficients in G8a. Therefore the zero-
frequency CKP term computed in G8a.5 has the same arithmetic local density factors as the
canonical LPI projection, up to C1 boundary errors.

Proof. Elementary coefficient local models are defined in B1LD.1. B1LD.2 shows that finite convo-
lution and CRT localization commute. G1a gcd splitting and the tagged CKP dyadic restrictions
are finite refinements of the same coefficient support, so they preserve the local model tagwise.
LPI defines Locрќ‘„ using exactly these tagwise local coefficient models; H4 later assembles the LPI-
admitted terms. Thus the arithmetic coefficient part of the G8a в„Ћ = 0 term and the arithmetic
coefficient part of the LPI canonical projection agree. Endpoint and smoothing discrepancies are
C1 boundary errors by construction. Lemma proved.
    вЂ”


Remark 5.5 (B1LD.5. Output). Every CKP zero-frequency term that enters the local/main branch
has the same tagged B1 local coefficient model as the LPI projection. Thus the в„Ћ = 0 CKP
contribution can be assembled by H4 without changing normalization and without double-counting
any parent B1 block.

B1LD.6. Logical Dependencies           Internal dependencies: B1, C1, finite CRT local algebra.
  Children served: G8a, H4.

5.3   Part 3. H4: Tagged local algebra and singular series
Source file: Lemmas/h_4_ltx.md.

H4. Local/Main Compatibility Lemma

                                                  13
H4.0. Role Logical ID: H4.
    Used by: I1, final local/main assembly.
    Uses: LPI, B1, B3, F3P, F3, F3T, F4, D1, G8a, B1LD, C1, C1A, finite CRT local algebra, and the
local model О›рќ‘„ .
    Lemma H4 is responsible for the main term of the proof. After B3/F3/F4/C1 routing, all
terminal atoms are divided into error classes and local/main classes.
    The error classes are already handled by:

                  Edge в†’ рќђ¶1,         CKPв„ЋМё=0 в†’ рќђє8рќ‘Ћ,          GoodAWACK в†’ рќђё10.
   The local/main contributions come from:

                          LongAP/Local,          LocalDiag,       CKPв„Ћ=0 .
   H4 has to prove:

                                    рќ‘Ђlocal (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   The local/main compatibility statement must prevent:

  1. double counting local terms;

  2. loss of some local terms;

  3. mismatched normalizations among LongAP, LocalDiag, and CKP zero-frequency terms;

  4. incorrect assembly of the Euler product.

   Lemma H4 handles this by consuming the LPI local projection/admission interface and the
parent B1 block tags. Thus H4 is an assembly lemma: it does not define the local projection
independently of D1 or G8a, but assembles the local terms after D1, G8a, and B1LD have proved
LPI-admissibility.
   вЂ”

H4.1. Local modulus and local model The local model is the one defined in Lemma LPI.
We recall it here for the calculation of the singular series.
  Let

                                 рќ‘¤ = рќ‘¤(рќ‘Ѓ ) в†’ в€ћ,         рќ‘¤ = рќ‘њ(log рќ‘Ѓ ),
   and set

                                             рќ‘„=
                                                   в€ЏпёЃ
                                                        рќ‘ќ.
                                                  рќ‘ќв‰¤рќ‘¤

   Define the local model of О› modulo рќ‘„ by

                                                  рќ‘„
                                      О›рќ‘„ (рќ‘Ћ) =       1        .
                                                 рќњ™(рќ‘„) (рќ‘Ћ,рќ‘„)=1
   This normalization gives average value one:
                                        1 в€‘пёЃ
                                                  О›рќ‘„ (рќ‘Ћ) = 1.
                                        рќ‘„ рќ‘Ћ mod рќ‘„

                                                  14
   Define the local Goldbach density at modulus рќ‘„:
                                         1 в€‘пёЃ
                             рќњЋрќ‘„ (рќ‘Ѓ ) =             О›рќ‘„ (рќ‘Ћ)О›рќ‘„ (рќ‘Ѓ в€’ рќ‘Ћ).
                                         рќ‘„ рќ‘Ћ mod рќ‘„

   The canonical local main term is

                                   рќ‘Ђрќ‘„ (рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ),
   where the рќ‘њ(рќ‘Ѓ ) comes only from endpoint/smooth partition effects already routed to C1 or
from replacing exact interval length by рќ‘Ѓ + рќ‘‚(1).
   вЂ”

H4.2. Canonical local projection of the original problem              Define the canonical local pro-
jection of the original Goldbach sum by

                                      Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ).
   Equivalently,
                                              1 в€‘пёЃ
                        Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) = рќ‘Ѓ В·              О›рќ‘„ (рќ‘Ћ)О›рќ‘„ (рќ‘Ѓ в€’ рќ‘Ћ).
                                              рќ‘„ рќ‘Ћ mod рќ‘„

    This definition is independent of a particular branch of the proof tree.
    The purpose of H4 is to prove that the sum of all local/main pieces produced by D1, G8a
zero-frequency, and LocalDiag routing is exactly this canonical local projection, up to рќ‘њ(рќ‘Ѓ ):

                                рќ‘Ђlocal (рќ‘Ѓ ) = Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   Then H4 computes the limit

                                          рќњЋрќ‘„ (рќ‘Ѓ ) в†’ S(рќ‘Ѓ )
   as рќ‘¤ в†’ в€ћ.
   вЂ”

H4.3. Parent B1 block tags       From Lemma B1 we have the exact decomposition

                                    рќ‘…О› (рќ‘Ѓ ) =           рќ‘ђв„¬ рќ‘…в„¬ (рќ‘Ѓ ).
                                                 в€‘пёЃ

                                                в„¬в€€BрќђЅ0

   Every atom produced later by B3/F3 carries a parent tag

                                          tag(рќ’њ) = (в„¬, рќњЏ ),
   where:

  вЂў в„¬ is the parent typed B1 block;

  вЂў рќњЏ is the finite routing/grouping history inside B3/F3.




                                                 15
    B3/F3 guarantee that these tagged atoms form a finite partition of the parent block contribution;
this is Lemma F3.15:

                                        рќ‘…в„¬ (рќ‘Ѓ ) =              рќ‘…в„¬,рќњЏ (рќ‘Ѓ ),
                                                      в€‘пёЃ

                                                    рќњЏ в€€рќ’Ї (в„¬)

   with no overlap at the tagged level.
   This is the bookkeeping mechanism preventing double counting.
   вЂ”

H4.4. Canonical local projection of tagged atoms For every tagged local atom \{}((\{}math-
cal B,\{}tau) \{}), define its canonical local projection

                                               Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ )
   as the contribution of that tagged cell to the local model obtained by replacing the arithmetic
coefficients by their residue-class local densities modulo рќ‘„, while keeping the same smooth/dyadic
weights and the same tag.
   The definition is linear:
                                      вЋ›         вЋћ

                                 Locрќ‘„ вЋќ рќ‘ђв„¬ рќ‘…в„¬,рќњЏ вЋ  =    рќ‘ђв„¬ Locрќ‘„ рќ‘…в„¬,рќњЏ .
                                       в€‘пёЃ           в€‘пёЃ

                                         в„¬,рќњЏ               в„¬,рќњЏ

   The local/main term assigned by D1, G8a zero frequency, or LocalDiag is admitted into H4
only if it equals this canonical projection:

                                   local
                                  рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њв„¬,рќњЏ (рќ‘Ѓ ).
    This is the LPI admission condition as consumed by H4.
    Thus H4 does not accept arbitrary local-looking main terms. It accepts only tagged canonical
local projections.
    By Lemma LPI.1, the admitted local source set is exactly

                                LLPI = LLongAP/Local вЉ” LCKP,0 вЉ” LLocalDiag .
    There is no separate residual projection class. The only auxiliary local-looking operations that
can occur before H4 are controlled CRT restriction or absorption, fixed-divisor quotienting, primi-
tive local slicing, and endpoint or smooth-boundary localization. The first three are finite tagged
refinements of one of the three displayed source classes and must satisfy the same LPI admis-
sion condition. Endpoint and smooth-boundary terms are C1 Edge contributions, not local/main
sources.
    вЂ”

H4.4A. Compatibility of the local projection with prior routing The following compati-
bility table records the LPI admission compatibility consumed by H4. It records why the operation
Locрќ‘„ may be applied to the tagged terminal cells without changing the local algebra of the original
Goldbach convolution.

   Source operation before H4          Compatibility with Locрќ‘„              Excluded failure mode




                                                      16
    B1 HeathвЂ“Brown expansion                   B1 is an exact finite convolution iden-   treating an individual B1 summand
                                               tity before estimation; О›рќ‘„ replaces       as an independent local model
                                               the two original von Mangoldt factors
                                               after the identity is summed over all
                                               B1 tags.
    B3 product grouping                        B3 only partitions the finite product-    counting two different groupings as
                                               coordinate descriptions and preserves     two local main terms for the same
                                               the parent B1 tag.                        tagged cell
    F3/F4 terminal routing                     F3/F4 refine the summation domain         admitting a local term without its in-
                                               by exact tagged partitions or send        herited B1/F3 tag
                                               the cell to a terminal class.
    Controlled CRT absorption                  compatible finite-index restriction of    changing the normalization from О›рќ‘„
                                               residue classes modulo рќ‘„; incompat-       to a branch-specific density
                                               ible fibres are empty.
    Fixed-divisor or quotient decision         admitted locally only after B1-LD         quotient main term with unmatched
                                               identifies the quotient coefficient       arithmetic coefficient
                                               model with the same CRT local re-
                                               placement.
    Gcd/local/proportional relation            admitted only as a tagged LocalDiag       untagged diagonal density or non-
                                               projection of a parent cell.              canonical specialization
    LongAP/Local branch                        F3P gives the intrinsic local-            branch-specific AP density with a
                                               coefficient predicate, and D1.2A          nonlocal coefficient
                                               expands it into the tagged Locрќ‘„
                                               projection.
    CKP zero-frequency branch                  G8a.5 and B1-LD identify the в„Ћ = 0        importing a nonzero Fourier mode
                                               mode with the tagged local projec-        into H4
                                               tion.
    C1 Edge removal                            C1 contributes only рќ‘њ(рќ‘Ѓ ) and is not      losing a local main term by labelling
                                               part of рќ‘Ђlocal .                          it Edge without a strict C1 predicate
    GoodAWACK and CKP nonzero                  these are error branches, already         double-counting an error branch as a
    modes                                      handled before H4.                        local term
    Primitive local slicing                    a finite tagged subdivision of an al-     treating a slice as a new branch with-
                                               ready admitted LongAP/Local, CKP          out its parent tag
                                               в„Ћ = 0, or LocalDiag source.
    Endpoint or smooth-boundary local-         routed to C1 and charged as рќ‘њ(рќ‘Ѓ ).        importing a boundary correction into
    ization                                                                              the main term




    Consequently H4 does not rely on the phrase "canonical projection" as an unproved convention.
A local/main contribution is admitted only after the source operation is compatible with the single
replacement rule

                                                   О›(рќ‘›) в†¦в†’ О›рќ‘„ (рќ‘› mod рќ‘„)
   on the tagged Goldbach convolution.
   вЂ”

H4.5. Local reconstruction from the B1 decomposition

Lemma 5.6 (Lemma H4.1). The sum of the canonical local projections of all tagged descendants
of the exact B1 decomposition reconstructs the local Goldbach model:

                                           Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).                               (H4-reconstruct)
                      в€‘пёЃ          в€‘пёЃ
                           рќ‘ђв„¬
                      в„¬         рќњЏ в€€рќ’Ї (в„¬)

    Equivalently, the LPI local projection of the full tagged proof tree is not a branch-specific surro-
gate. It is the convolution of the single local model О›рќ‘„ with itself along рќ‘›1 + рќ‘›2 = рќ‘Ѓ .



                                                                17
Proof. By Lemma B1, the HeathвЂ“Brown decomposition used in the proof is an exact finite identity
for the two von Mangoldt factors in рќ‘…О› (рќ‘Ѓ ), after the fixed smooth dyadic partition of unity has
been inserted. Thus

                                            рќ‘…О› (рќ‘Ѓ ) =          рќ‘ђв„¬ рќ‘…в„¬ (рќ‘Ѓ )
                                                         в€‘пёЃ

                                                           в„¬

    before any terminal estimate is applied. By Lemma F3.15, each parent block is then partitioned
into tagged descendants:

                                           рќ‘…в„¬ (рќ‘Ѓ ) =               рќ‘…в„¬,рќњЏ (рќ‘Ѓ ).
                                                          в€‘пёЃ

                                                        рќњЏ в€€рќ’Ї (в„¬)

    The local replacement defined by LPI and assembled by H4 is the finite CRT local replacement
of the same B1 coefficient factors and the same dyadic cells. For B1-inherited finite-convolution
coefficients this compatibility is the content of Lemma B1-LD: elementary B1 coefficient models,
finite convolution, CRT restriction, gcd splitting, and tagged dyadic localization commute with the
local replacement, up to C1 boundary terms.
    Therefore applying Locрќ‘„ to the exact B1/F3 tagged partition gives the same result as applying
the local model directly to the original two von Mangoldt factors. On the original factors the local
model is by definition

                                                                      рќ‘„
                                О›(рќ‘›) в†¦в†’ О›рќ‘„ (рќ‘› mod рќ‘„) =                   1        .
                                                                     рќњ™(рќ‘„) (рќ‘›,рќ‘„)=1
   Consequently the reconstructed local sum is

                                                        О›рќ‘„ (рќ‘›1 )О›рќ‘„ (рќ‘›2 )
                                              в€‘пёЃ

                                            рќ‘›1 +рќ‘›2 =рќ‘Ѓ

   with the same smooth endpoint convention as the tagged cells. Counting by the residue class
рќ‘Ћ в‰Ў рќ‘›1 (mod рќ‘„) gives

                                           1 в€‘пёЃ
                  О›рќ‘„ (рќ‘›1 )О›рќ‘„ (рќ‘›2 ) = рќ‘Ѓ В·             О›рќ‘„ (рќ‘Ћ)О›рќ‘„ (рќ‘Ѓ в€’ рќ‘Ћ) + рќ‘њ(рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
         в€‘пёЃ

      рќ‘›1 +рќ‘›2 =рќ‘Ѓ
                                           рќ‘„ рќ‘Ћ mod рќ‘„

   The рќ‘њ(рќ‘Ѓ ) term is only the endpoint/smooth-boundary discrepancy already admitted by C1.
This proves (H4-reconstruct).
   вЂ”


H4.6. Dyadic and routing recombination

Lemma 5.7 (Lemma H4.2). The dyadic partitions and routing tags used before H4 do not change
the local main term:

                                    рќ‘ђв„¬ Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) = Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
                              в€‘пёЃ

                              в„¬,рќњЏ




                                                          18
Proof. The dyadic partition in B1 is an exact partition of unity on the active support. Hence
summing over dyadic scales recombines the original B1 finite-convolution expression exactly. The
later B3/F3/F4 operations are finite tagged partitions: they split summation domains by grouping
choices, CRT restrictions, fixed-divisor cases, quotient cases, terminal predicates, and boundary
alternatives. Each such operation is either an exact finite partition or a boundary/short-volume
removal already admitted by C1.
    The operator Locрќ‘„ is linear and tag-preserving. Therefore it commutes with the finite re-
combination of dyadic cells and routing cells. The only discrepancy comes from endpoint and
smooth-boundary cells, which are C1 Edge contributions and hence рќ‘њ(рќ‘Ѓ ). Lemma proved.
    вЂ”


H4.7. Admission of branch local terms
Lemma 5.8 (Lemma H4.3). Every terminal local/main contribution entering I1 satisfies the LPI
admission condition consumed by H4

                                 local
                                рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).                     (H4-adm)
Proof. There are three sources of local/main terms.

  1. LongAP/Local. Lemma F3P first states the positive local-coefficient

    predicate for this terminal class, and Lemma D1, including Lemma D1.2A, expands that local
algebra into controlled residue/coprimality data. Its local residue-density theorem then identifies
the zero/local part of the long AP count with Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ), with boundary terms routed to C1.

  1. CKP zero frequency. Lemma G8a separates в„Ћ = 0 from в„Ћ Мё= 0. The

    nonzero frequencies are not local terms. The в„Ћ = 0 term is identified in G8a.5 with the LPI
canonical local projection. Lemma B1-LD supplies the arithmetic compatibility of the B1-inherited
finite-convolution coefficients under gcd splitting, CRT localization, and tagged dyadic restriction.

  1. LocalDiag. In the F3/F4 routing, LocalDiag means forced equality,

    proportionality, gcd-local dependence, or collision that produces a canonical local tagged cell.
If a degeneracy is not a canonical local projection, it is not admitted by H4; the F3T routing table
sends it instead to Edge, CKP, GoodAWACK, impossible, or a continuing routed case. Thus every
LocalDiag term that reaches H4 is already a tagged canonical local projection.
    These are the only local/main terminal classes in the routing table. Hence every local/main
contribution entering I1 satisfies (H4-adm). Lemma proved.
    вЂ”


H4.8. No double counting lemma
Lemma 5.9 (Lemma H4.4). The sum of all admitted local/main terms satisfies

                               рќ‘Ђlocal (рќ‘Ѓ ) =                               (рќ‘Ѓ ),
                                                    в€‘пёЃ
                                                                     local
                                                                 рќ‘ђв„¬ рќ‘Ђв„¬,рќњЏ
                                               в„¬,рќњЏ в€€рќ’Їlocal (в„¬)

   and no local term is counted twice.

                                                     19
Proof. Each term is indexed by its parent B1 block в„¬ and a unique routing tag рќњЏ . By Lemma
F3.15, B3/F3/F4 routing produces a finite exact partition of every parent block into tagged cells.
Therefore two different tags correspond either to disjoint cells of the same B1 block or to summands
from different B1 blocks in the exact B1 decomposition.
    This includes LocalDiag atoms. A LocalDiag condition is detected by a structural predicate
such as forced equality, proportionality, gcd-local dependence, or collision of forms; two different
routing cells may therefore look locally identical. H4 does not identify local terms by visual form. It
sums the canonical projection of each tagged cell. Since the underlying tagged cells are disjoint by
(F3-partition), structurally identical LocalDiag expressions from different tags are complementary
summands, not duplicates.
    If (в„¬, рќњЏ ) Мё= (в„¬ вЂІ , рќњЏ вЂІ ), then either в„¬ Мё= в„¬вЂІ , in which case the two summands already occur separately
in the exact B1 expansion, or в„¬ = в„¬ вЂІ and рќњЏ Мё= рќњЏ вЂІ , in which case Lemma F3.15 gives disjoint
summation domains. Linearity of Locрќ‘„ then preserves this separation.
    Thus no double counting occurs. Lemma proved.
    вЂ”


H4.9. Completeness of local terms

Lemma 5.10 (Lemma H4.5). Every terminal local/main atom produced by B3/F3/F4 routing is
included in exactly one of:

                             LongAP/Local,          LocalDiag,       CKPв„Ћ=0 .

Proof. By Lemma F3 and the LPI interface, every terminal atom belongs to exactly one termi-
nal routing class at the tagged level. Error classes are Edge, CKP nonzero-frequency error, and
GoodAWACK. Local/main classes are LongAP/Local, LocalDiag, and CKP zero-frequency. Con-
trolled CRT restrictions, quotients and local slicing may produce auxiliary local projection sub-
terms, but such subterms inherit the parent tag and are admitted only inside one of these three
classes. They are not a separate local/main source.
    Therefore every admitted local/main contribution is tagged once and all terminal local/main
contributions are included. Lemma proved.
    вЂ”


H4.10. Linearity of the local projection

Lemma 5.11 (Lemma H4.6). The sum of canonical local projections over all tagged local/main
atoms equals the canonical local projection of the original Goldbach sum:

                                    рќ‘ђв„¬ Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) = Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
                              в€‘пёЃ

                              в„¬,рќњЏ

Proof. The B1 decomposition is exact and B3/F3 tagged routing partitions each parent block into
finitely many cells. The operator Locрќ‘„ is linear by definition. Therefore applying Locрќ‘„ before or
after summing the tagged decomposition gives the same result.
    All nonlocal/error classes contribute either zero to the admitted local sum or are handled as
рќ‘њ(рќ‘Ѓ ) by C1/E10/G8a nonzero-frequency estimates. The remaining admitted local classes sum to
the full canonical local projection. Lemma proved.


                                                     20
    вЂ”


H4.11. Compatibility of LongAP, CKP zero-frequency and LocalDiag normalizations

Lemma 5.12 (Lemma H4.7A). Every admitted local/main term from LongAP/Local, CKP zero-
frequency, or LocalDiag is normalized by the single LPI operation

                                               О›(рќ‘›) в†¦в†’ О›рќ‘„ (рќ‘› mod рќ‘„)
    inside the original tagged Goldbach convolution. No branch is allowed to introduce a separate
local density convention.
    Equivalently, for every admitted tagged cell (в„¬, рќњЏ ),

                                       local
                                      рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
    The verification is as follows.


  Source of the local term      Branch expression before             H4 normalization                Excluded alternative
                                H4
  LongAP/Local                  a      long   arithmetic-            F3P forces all long-variable    if a nonlocal coefficient sur-
                                progression main    term             coefficients into Cloc (рќ‘„рќњЏ ),   vives, the atom is not F3P-
                                after D1                             and D1.2A identifies the re-    LongAP/Local and hence
                                                                     maining AP density with         not LPI-admitted
                                                                     Locрќ‘„ рќ‘…в„¬,рќњЏ
  CKP в„Ћ = 0                     the zero Fourier mode in the         G8a.5 identifies the в„Ћ =        в„Ћ Мё= 0 is never local and is
                                G8a CKP expansion                    0 mode with the same            sent to CKP/X10
                                                                     Locрќ‘„ рќ‘…в„¬,рќњЏ , using B1-LD
                                                                     for coefficient compatibility
  LocalDiag                     a forced equality, propor-           admitted only when the di-      noncanonical degeneracies
                                tionality, gcd-local depen-          agonal cell is the canonical    are routed by F3T to Edge,
                                dence, or collision cell             local projection of a tagged    CKP, GoodAWACK, im-
                                                                     B1/F3/F4 cell                   possible, or a continuing
                                                                                                     routed case
  Controlled CRT restriction    a finite-index refinement of         admitted only when the          branch-specific CRT densi-
  or absorption                 a tagged source class                parent tag and the О›рќ‘„ -         ties are not H4 inputs
                                                                     replacement rule are pre-
                                                                     served
  Fixed-divisor quotienting     a coefficient refinement of a        admitted only through the       quotient main terms with
                                tagged source class                  B1-LD compatibility check       unmatched coefficient mod-
                                                                                                     els are not H4 inputs
  Primitive local slicing       a finite subdivision of the          admitted only as part of its    a slice is not a fourth local
                                same tagged local source             parent LongAP/Local, CKP        branch
                                                                     в„Ћ = 0, or LocalDiag class
  Endpoint     or     smooth-   boundary correction                  routed to C1 as рќ‘њ(рќ‘Ѓ ), not      boundary terms are not lo-
  boundary localization                                              assembled by H4                 cal main terms




Proof. The operator Locрќ‘„ was defined before any branch-specific terminal analysis: it replaces
the arithmetic coefficients in the original tagged Goldbach convolution by their residue-class local
model modulo рќ‘„, while keeping the same dyadic weights, summation domain, and routing tag.
Therefore it is a property of the parent tagged cell, not of the branch that later recognizes the local
contribution.
    For LongAP/Local cells, F3P and D1.2A first exclude exactly the obstruction that would leave
a branch-specific arithmetic coefficient. The remaining main term is the residue-density projection
of the same tagged cell, hence it is Locрќ‘„ рќ‘…в„¬,рќњЏ .


                                                                21
    For CKP cells, G8a separates the zero Fourier mode from all nonzero modes. The nonzero
modes are analytic error terms. The zero mode is a local projection only after G8a.5 and B1-LD
identify its finite-convolution coefficients with the B1-inherited local density; hence its admitted
form is again Locрќ‘„ рќ‘…в„¬,рќњЏ .
    For LocalDiag cells, the routing tag records the exact forced relation that created the diagonal
cell. H4 admits such a cell only when the diagonal specialization is a canonical tagged projection.
If the specialization is not canonical, it never reaches H4 and is routed elsewhere by F3T.
    Thus the equality of normalizations is not assumed branch-by-branch; it is enforced by the
definition of admissible local/main term.
    вЂ”


H4.12. Calculation of local factors                  By the definition of О›рќ‘„ ,

                                        1 в€‘пёЃ       рќ‘„             рќ‘„
                        рќњЋрќ‘„ (рќ‘Ѓ ) =                      1(рќ‘Ћ,рќ‘„)=1     1           .
                                        рќ‘„ рќ‘Ћ mod рќ‘„ рќњ™(рќ‘„)          рќњ™(рќ‘„) (рќ‘Ѓ в€’рќ‘Ћ,рќ‘„)=1

   Since рќ‘„ is squarefree, CRT gives

                                               рќњЋрќ‘„ (рќ‘Ѓ ) =              рќњЋрќ‘ќ (рќ‘Ѓ ),
                                                                в€ЏпёЃ

                                                                рќ‘ќв‰¤рќ‘¤

   where

                              1
                                             )пё‚2
                                        рќ‘ќ
                                  (пё‚
                  рќњЋрќ‘ќ (рќ‘Ѓ ) =                        #{рќ‘Ћ mod рќ‘ќ : (рќ‘Ћ, рќ‘ќ) = 1, (рќ‘Ѓ в€’ рќ‘Ћ, рќ‘ќ) = 1}.
                              рќ‘ќ        рќ‘ќв€’1
   For рќ‘ќ = 2 and even рќ‘Ѓ , the only unit residue is 1, and рќ‘Ѓ в€’ 1 в‰Ў 1 (mod 2), so

                                                          рќњЋ2 (рќ‘Ѓ ) = 2.
    For odd рќ‘ќ:
    If рќ‘ќ | рќ‘Ѓ , then the forbidden residues рќ‘Ћ в‰Ў 0 and рќ‘Ћ в‰Ў рќ‘Ѓ coincide. Hence the number of admissible
residues is

                                                            рќ‘ќ в€’ 1,
   and

                                            1
                                                                )пё‚2
                                                           рќ‘ќ                       рќ‘ќ
                                                     (пё‚
                                  рќњЋрќ‘ќ (рќ‘Ѓ ) =                           (рќ‘ќ в€’ 1) =       .
                                            рќ‘ќ             рќ‘ќв€’1                     рќ‘ќв€’1
   If рќ‘ќ в€¤ рќ‘Ѓ , the two forbidden residues are distinct, so the number of admissible residues is

                                                            рќ‘ќ в€’ 2,
   and

                                   1                                  рќ‘ќ(рќ‘ќ в€’ 2)        1
                                                   )пё‚2
                                             рќ‘ќ
                                       (пё‚
                     рќњЋрќ‘ќ (рќ‘Ѓ ) =                           (рќ‘ќ в€’ 2) =             =1в€’          .
                                   рќ‘ќ        рќ‘ќв€’1                       (рќ‘ќ в€’ 1)2     (рќ‘ќ в€’ 1)2
   Therefore



                                                              22
                                          в€ЏпёЃ (пё‚             1               рќ‘ќ
                                                                    )пё‚ в€ЏпёЃ
                          рќњЋрќ‘„ (рќ‘Ѓ ) = 2               1в€’                         .
                                        3в‰¤рќ‘ќв‰¤рќ‘¤
                                                         (рќ‘ќ в€’ 1)2    3в‰¤рќ‘ќв‰¤рќ‘¤
                                                                           рќ‘ќв€’1
                                         рќ‘ќв€¤рќ‘Ѓ                              рќ‘ќ|рќ‘Ѓ

   Letting рќ‘¤ в†’ в€ћ, we get
                                                            в€ЏпёЃ рќ‘ќ в€’ 1
                                        рќњЋрќ‘„ (рќ‘Ѓ ) в†’ 2рќђ¶2                   ,
                                                            рќ‘ќ|рќ‘Ѓ
                                                                  рќ‘ќв€’2
                                                            рќ‘ќ>2

   where
                                              в€ЏпёЃ (пё‚         1
                                                                     )пё‚
                                       рќђ¶2 =           1в€’          .
                                              рќ‘ќ>2
                                                         (рќ‘ќ в€’ 1)2
   Thus

                                            рќњЋрќ‘„ (рќ‘Ѓ ) в†’ S(рќ‘Ѓ ).
   вЂ”

H4.13. Local/Main compatibility theorem

Theorem 5.13 (Theorem H4). In the proof tree, the sum of all terminal local/main contributions
satisfies

                                      рќ‘Ђlocal (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).

Proof. By the compatibility table H4.4A and Lemma H4.3, every LongAP/Local, CKP zero-
frequency, and LocalDiag term that reaches H4 satisfies the LPI admission condition

                               local
                              рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њв„¬,рќњЏ (рќ‘Ѓ ).
   By Lemma H4.4, local/main terms are summed by unique B1 parent tags and routing tags, so
there is no double counting. By Lemma H4.5, all terminal local/main atoms are included.
   Therefore

                            рќ‘Ђlocal (рќ‘Ѓ ) =           рќ‘ђв„¬ Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
                                            в€‘пёЃ

                                              в„¬,рќњЏ

   By Lemmas H4.1, H4.2, and H4.6, the tagged sum of canonical local projections reconstructs
the full local Goldbach model:

                      рќ‘Ђlocal (рќ‘Ѓ ) = Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   By the local factor calculation,

                                            рќњЋрќ‘„ (рќ‘Ѓ ) в†’ S(рќ‘Ѓ ).
   Hence

                                      рќ‘Ђlocal (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   The theorem is proved.

                                                       23
    вЂ”


Remark 5.14 (H4.14. Output).

              All admitted local/main terms assemble as Locрќ‘„ рќ‘…О› (рќ‘Ѓ ) = рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).

    Every local term is a canonical local projection, carries parent B1 and routing tags, and is
admitted only when its branch-specific normalization matches Locрќ‘„ . CKP zero-frequency, LongAP
local terms, and LocalDiag terms are combined by tagged linearity. The singular series is computed
from the explicit finite local model О›рќ‘„ .
    вЂ”

H4.15. Logical Dependencies Internal dependencies: LPI, B1, B3, F3P, F3, F3T, F4, D1, G8a,
B1LD, C1, C1A, and the local model О›рќ‘„ .
   Children served: I1 and the final local/main assembly.


6      Package Dependency Ledger and Synchronization Notes
6.1        Compact Package Dependency Graph
H4-Local-Algebra +вЂ“ D1: LongAP/Local atoms enter the LPI projection later assembled by H4 +вЂ“
B1LD: B1 finite-convolution local densities match the H4 model +вЂ“ H4: tagged local reconstruction,
no double counting, singular series

6.2        Local Ledger

      ID                             Uses                                  Exports
      D1                             B1/B3/F3/F4 routing, C1P/C1A/C1,          LongAP/Local projection admission
                                     E10L, G8a
      B1LD                           B1 local density algebra              CKP zero-frequency compatibility
      H4                             D1, B1LD, tagged partition, CRT al-   S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ) local assembly
                                     gebra




6.3        Synchronization Boundary
The package is synchronized with the one-file proof through the logical IDs D1, B1LD, and H4.
File paths are navigation aids only.


7      Bibliography
This local package has no active external analytic bibliography. Its mathematical references are
the standard CRT factorization and the elementary Euler-product computation of the Goldbach
singular series. In the modular dossier these standard facts are recorded through the logical IDs
B1LD and H4 rather than through a separate external theorem number.




                                                     24
8     References
Active logical references for this package:

    1. D1, which admits LongAP/Local terms into the LPI projection later assembled by H4.

    2. B1LD, which identifies the B1 finite-convolution local density with the LPI local model later
       assembled by H4.

    3. H4, which proves tagged reconstruction, no double counting, and convergence to S(рќ‘Ѓ ).

   The package has no direct external analytic citation. All analytic estimates used to route
nonlocal terms away from H4 are imported through the other theorem packages, not invoked here.




                                                 25

