                        H4 Local Algebra Theorem Package
                                            Denis Saltykov

                                               May 2026


                                                Abstract
         This note isolates the H4 local/main assembly node from the full proof package. Its purpose
     is to prove, as a standalone local algebra statement, that all admitted local/main terms assemble
     into the classical Goldbach singular-series main term S(N )N + o(N ). The proof makes explicit
     the local model ΛQ , the tagged LPI admission condition consumed by H4, the linearity over the
     B1/F3 tagged partition, the no-double-counting mechanism, and the finite CRT calculation of
     the local factors.


Contents
1 Scope                                                                                                  1

2 The Local Model                                                                                        2

3 Tagged Decomposition and H4 Admission                                                                  2

4 Admission of the Main Local Sources                                                                    3

5 Reconstruction                                                                                         3

6 No Double Counting and No Loss                                                                         4

7 Local Factors                                                                                          5

8 Main Theorem                                                                                           5

9 Output                                                                                                 6


1   Scope
This package does not estimate Edge, CKP nonzero-frequency, or GoodAWACK terms. Those
terms are discharged by their own terminal branches. H4 handles only the admitted local/main
terms and proves
                                 Mlocal (N ) = S(N )N + o(N ).                      (H4-LA)
The statement must exclude three failure modes: a branch-specific local normalization, double
counting of local terms, and loss of tagged local mass.
   The proof uses the logical inputs B1, B3, F3, F3T, F4, D1, G8a, B1LD, C1, C1A, and finite
CRT algebra.


                                                    1
2      The Local Model
Let                                                                               Y
                         w = w(N ) → ∞,          w = o(log N ),              Q=         p.
                                                                                  p≤w

Then Q is squarefree and Q = N o(1) . Define
                                                      Q
                                          ΛQ (a) =       1        .
                                                     φ(Q) (a,Q)=1
The finite local Goldbach density is
                                             1 X
                                σQ (N ) =              ΛQ (a)ΛQ (N − a).                       (2.1)
                                             Q a mod Q

The canonical local projection of the original Goldbach convolution is

                                         LocQ RΛ (N ) = N σQ (N ).                             (2.2)

Endpoint and smooth-boundary discrepancies are C1-admitted boundary errors and are o(N ).


3      Tagged Decomposition and H4 Admission
B1 gives an exact finite identity
                                                      X
                                         RΛ (N ) =           cB RB (N ).                       (3.1)
                                                     B∈BJ0

After B3/F3/F4 routing, each parent block is partitioned into tagged cells:
                                                       X
                                         RB (N ) =              RB,τ (N ),                     (3.2)
                                                     τ ∈T (B)

before any terminal estimate is applied. The tag (B, τ ) records the parent B1 block and the finite
routing/grouping history.

Definition 1 (Tagged LPI local projection). For a tagged cell (B, τ ), define LocQ RB,τ (N ) by
replacing the arithmetic coefficients in that same tagged cell by their residue-class local models
modulo Q, while preserving the parent tag, routing tag, smooth/dyadic weights, controlled local
congruence data, and the equation n1 + n2 = N .
                                                                          local (N ) is admitted
Definition 2 (LPI admission condition consumed by H4). A local/main term MB,τ
by H4 only if
                               local
                            MB,τ     (N ) = LocQ RB,τ (N ) + oB,τ (N ).                    (3.3)

      The admitted local source set is

                              LH4 = LLongAP/Local ⊔ LCKP,0 ⊔ LLocalDiag .                      (3.4)

There is no fourth residual projection source. Controlled CRT absorption, fixed-divisor quotienting,
and primitive local slicing are admitted only as tagged refinements of one of the three displayed
classes. Endpoint and smooth-boundary localizations are C1 Edge terms and do not enter LH4 .

                                                       2
4    Admission of the Main Local Sources
Lemma 1 (LongAP/Local admission). Every LongAP/Local terminal term admitted into H4 sat-
isfies the admission condition (3.3).

Proof. D1 first excludes any surviving nonlocal coefficient attached to the long AP variable. Thus
no factor such as                                                      !
                                                                 kL(u)
                           µ(L(u)), λ(L(u)), e(αL(u)), e
                                                                   q
survives inside a terminal LongAP/Local atom. All remaining restrictions are controlled residue-
class, coprimality, AP, or CRT restrictions with moduli (log N )O(1) .
    The smooth AP count replaces each controlled residue class by its zero frequency density.
Nonzero finite Fourier terms are negligible by smoothness and by the length of the LongAP direc-
tion; endpoint errors are C1-admitted. The resulting LongAP/Local main term is therefore exactly
the tagged ΛQ -local projection of the same cell, up to o(N ).

Lemma 2 (CKP zero-frequency admission). Every CKP zero-frequency term admitted into H4
satisfies the admission condition (3.3).

Proof. G8a separates the CKP AP/fibre expansion into the zero frequency h = 0 and the nonzero
frequencies h ̸= 0. The nonzero frequencies are not local terms. For h = 0, the finite AP expansion
gives the average over the residue fibre:
                                          1b           1X
                                            Fa,q (0) =     Fa,q (y).
                                          q            q y

B1LD proves that the B1-inherited coefficient local densities commute with finite convolution, CRT
localization, gcd splitting, and tagged dyadic restriction. Hence the arithmetic coefficient factors in
the CKP h = 0 term are exactly those used by LocQ RB,τ    CKP (N ). The tag is preserved throughout.

Thus (3.3) holds.

Lemma 3 (LocalDiag admission). Every LocalDiag term admitted into H4 satisfies the admission
condition (3.3).

Proof. In F3/F4, LocalDiag denotes a forced equality, proportionality, gcd-local dependence, or
unavoidable collision that produces a canonical local tagged cell. H4 admits such a cell only
when the diagonal specialization is the local projection of the same parent B1/F3/F4 cell. If the
specialization is not canonical, F3T routes it instead to Edge, CKP, GoodAWACK, impossible, or
a continuing routed case. Therefore every LocalDiag term reaching H4 is a tagged canonical local
projection.


5    Reconstruction
Lemma 4 (Tagged local reconstruction).
                          X           X
                               cB              LocQ RB,τ (N ) = N σQ (N ) + o(N ).                (5.1)
                           B        τ ∈T (B)




                                                         3
Proof. B1 is an exact finite identity before estimation, and F3/F4 give finite tagged partitions
before terminal estimates. The operator LocQ is linear and tag-preserving. Applying LocQ to the
tagged decomposition is therefore the same as applying the local model directly to the original two
von Mangoldt factors.
   On the original factors this replacement is
                                                                  Q
                                Λ(n) 7→ ΛQ (n mod Q) =               1        .
                                                                 φ(Q) (n,Q)=1

Thus the reconstructed local sum is
                                             X
                                                       ΛQ (n1 )ΛQ (n2 ).
                                           n1 +n2 =N

Counting by a ≡ n1 (mod Q) gives
         X                                 1 X
                  ΛQ (n1 )ΛQ (n2 ) = N ·             ΛQ (a)ΛQ (N − a) + o(N ) = N σQ (N ) + o(N ).
      n1 +n2 =N
                                           Q a mod Q

The o(N ) term is only the endpoint/smooth-boundary discrepancy admitted by C1.


6    No Double Counting and No Loss
Lemma 5 (No double counting). The admitted local/main sum
                                                         X
                                                                    local
                                   Mlocal (N ) =                cB MB,τ   (N )                       (6.1)
                                                   (B,τ )∈LH4

counts no local term twice.

Proof. Each admitted term carries the tag (B, τ ). If two tags have different parent B1 blocks, they
are different summands of the exact B1 identity. If they have the same parent block but different
routing tags, the F3 partition identity gives disjoint tagged cells.
    LocalDiag terms do not create an exception. Two LocalDiag expressions may look algebraically
identical after specialization, but H4 does not identify terms by visual form. It sums the canonical
projection of each tagged cell. Thus visually identical LocalDiag expressions from different tags are
complementary summands, not duplicates.

Lemma 6 (Completeness of admitted local terms). Every terminal local/main atom produced by
the routing tree and admitted into the main term lies in exactly one component of LH4 .

Proof. F3 assigns every terminal atom to exactly one terminal routing class. Error classes are
Edge, CKP nonzero-frequency, and GoodAWACK. Local/main classes are LongAP/Local, CKP
zero-frequency, and LocalDiag. The only auxiliary local-looking operations are controlled CRT
absorption, fixed-divisor quotienting, and primitive local slicing; each is a tagged refinement of one
of these three classes. Endpoint and smooth-boundary localizations are C1 Edge terms. Hence
there is no lost admitted local term and no hidden local class.




                                                          4
7    Local Factors
Since Q is squarefree, CRT gives                          Y
                                           σQ (N ) =           σp (N ),
                                                         p≤w
where
                                      2
                             1   p
                                      
                   σp (N ) =            #{a mod p : (a, p) = 1, (N − a, p) = 1}.
                             p p−1
For p = 2 and even N , the only unit residue is 1, hence σ2 (N ) = 2.
   For odd p | N , the two forbidden residues coincide, so
                                                      p
                                          σp (N ) =      .
                                                    p−1
For odd p ∤ N , the two forbidden residues are distinct, so
                                               p(p − 2)        1
                                   σp (N ) =            =1−          .
                                               (p − 1)2     (p − 1)2
Therefore
                                           Y                1                    p
                                                                      Y
                           σQ (N ) = 2               1−                               .
                                         3≤p≤w
                                                          (p − 1)2        3≤p≤w
                                                                                p − 1
                                          p∤N                              p|N
Letting w → ∞,
                                                        Y p−1
                                   σQ (N ) → 2C2                    = S(N ),                      (7.1)
                                                        p|N
                                                              p−2
                                                        p>2
where
                                               Y             1
                                                                      
                                       C2 =             1−          .
                                               p>2
                                                           (p − 1)2


8    Main Theorem
Theorem 1 (H4 local algebra). In the routed proof tree, the sum of all admitted local/main con-
tributions satisfies
                               Mlocal (N ) = S(N )N + o(N ).
Proof. By the admission lemmas and the LPI no-residual-projection rule, every local/main term
admitted into H4 satisfies the tagged admission identity (3.3). By the no-double-counting lemma
these terms are not counted twice, and by the completeness lemma there is no hidden admitted
local class. Therefore
                                               X
                           Mlocal (N ) =                cB LocQ RB,τ (N ) + o(N ).
                                           (B,τ )∈LH4

The nonlocal/error classes have already been removed by their terminal estimates and are not part
of Mlocal . The admitted local classes exhaust the local projection of the tagged proof tree, so tagged
local reconstruction gives
                       Mlocal (N ) = LocQ RΛ (N ) + o(N ) = N σQ (N ) + o(N ).
By the local factor calculation, σQ (N ) → S(N ). Hence
                                     Mlocal (N ) = S(N )N + o(N ).



                                                         5
9   Output
The output supplied to the global assembly theorem is

           MLongAP (N ) + MCKP,0 (N ) + MLocalDiag (N ) + Mproj (N ) = S(N )N + o(N ).

The equality is tagwise. No error branch is imported into H4, no branch uses a separate local
density convention, and no untagged local main term is admitted.




                                               6
