﻿Proof of the Binary Goldbach Theorem for Sufficiently Large Even
      Integers: Final Modular Assembly Full Proof Package
                              Denis Saltykov (ds1678@gmail.com)

                                             May 2026


Contents
1 Proof of the Binary Goldbach Theorem for Sufficiently Large Even Integers:
  Final Modular Assembly Full Proof Package                                                          3
  1.1 Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
  1.2 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
  1.3 Included Proof-Source Files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Part 1. PAR: Parameter register                                                                   3
      2.0.1 PAR. Global Parameter Register . . . . . . . . . . . . . . . . . . . . . . . . .        4

3 Part 2. GEB: Global error budget                                                                  7
      3.0.1 GEB. Global Error Budget and Parameter Hierarchy . . . . . . . . . . . . . .            7

4 Part 3. X1: HeathвЂ“Brown identity verification                                             10
      4.0.1 X1. HeathвЂ“Brown Identity Input for B1 . . . . . . . . . . . . . . . . . . . . . 10

5 Part 4. B1: Typed HeathвЂ“Brown decomposition                                             13
      5.0.1 B1. Typed HeathвЂ“Brown Decomposition . . . . . . . . . . . . . . . . . . . . . 13

6 Part 5. B3: Block classification                                                           18
      6.0.1 B3. Block Classification Lemma . . . . . . . . . . . . . . . . . . . . . . . . . 18

7 Part 6. F3P: Intrinsic terminal predicate catalogue                                         24
      7.0.1 F3P. Intrinsic Terminal Predicate Catalogue . . . . . . . . . . . . . . . . . . . 24

8 Part 7. F3: Routing partition                                                           28
      8.0.1 F3. Routing Exhaustion / No-Cycle Theorem . . . . . . . . . . . . . . . . . . 28

9 Part 8. F3A: Routing interface completeness                                               39
      9.0.1 F3A. Completeness of the F3.6 Routing Interface . . . . . . . . . . . . . . . . 39

10 Part 9. F3T: Complete routing exhaustion                                                 42
       10.0.1 F3T. Finite Routing Table for B1-Origin Atoms . . . . . . . . . . . . . . . . 42

11 Part 10. F4: Large-divisor and quotient routing                                            50
       11.0.1 F4. Large Divisor Routing Lemma . . . . . . . . . . . . . . . . . . . . . . . . 50


                                                  1
12 Part 11. C1A: Edge admission ledger                                                      58
       12.0.1 C1A. Admission of Terminal Edge Atoms . . . . . . . . . . . . . . . . . . . . 58

13 Part 12. C1: Unified Edge estimate                                                           62
       13.0.1 C1. Unified Edge Estimate . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

14 Part 13. I1: Final weighted assembly                                                         70
       14.0.1 I1. Final Weighted Assembly . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

15 Part 14. G2: Prime powers negligible                                                       75
       15.0.1 G2. Prime Powers Negligible Lemma . . . . . . . . . . . . . . . . . . . . . . . 75

16 Part 15. G1: Weighted asymptotic to strong Goldbach                                  78
       16.0.1 G1. Passage from Weighted Asymptotic to Strong Goldbach . . . . . . . . . 78

17 Part 16. G0H: Final handoff verification                                                81
       17.0.1 G0H. Final Handoff from I1/G2 to Strong Goldbach . . . . . . . . . . . . . . 81




                                                2
1     Proof of the Binary Goldbach Theorem for Sufficiently Large
      Even Integers: Final Modular Assembly Full Proof Package
1.1    Abstract
This full-proof package contains the common decomposition, routing, Edge, parameter, global
error-budget, and final handoff source texts used to prove the binary Goldbach theorem for all
sufficiently large even integers from the four modular theorem packages.

1.2    Scope
This is the full source-level version of the final binary-Goldbach assembly node. It complements
the route-level final assembly PDF and does not replace the full one-file manuscript.

1.3    Included Proof-Source Files
    1. Lemmas/proof_parameters_ltx.md вЂ“ Parameter register

    2. Lemmas/global_error_budget_ltx.md вЂ“ Global error budget

    3. External/x_1_heath_brown_identity_verification_ltx.md вЂ“ HeathвЂ“Brown identity ver-
       ification

    4. Lemmas/b_1_ltx.md вЂ“ Typed HeathвЂ“Brown decomposition

    5. Lemmas/b_3_ltx.md вЂ“ Block classification

    6. Lemmas/f3_intrinsic_terminal_predicate_catalogue_ltx.md вЂ“ Intrinsic terminal pred-
       icate catalogue

    7. Lemmas/f_3_ltx.md вЂ“ Routing partition

    8. Lemmas/f3_routing_interface_completeness_ltx.md вЂ“ Routing interface completeness

    9. Lemmas/f3_complete_routing_exhaustion_ltx.md вЂ“ Complete routing exhaustion

 10. Lemmas/f_4_ltx.md вЂ“ Large-divisor and quotient routing

 11. Lemmas/c1_edge_admission_ledger_ltx.md вЂ“ Edge admission ledger

 12. Lemmas/c_1_ltx.md вЂ“ Unified Edge estimate

 13. Lemmas/i_1_ltx.md вЂ“ Final weighted assembly

 14. Lemmas/g_2_ltx.md вЂ“ Prime powers negligible

 15. Lemmas/g_1_ltx.md вЂ“ Weighted asymptotic to strong Goldbach

 16. Lemmas/g0_final_handoff_verification_ltx.md вЂ“ Final handoff verification


2     Part 1. PAR: Parameter register
Source file: Lemmas/proof_parameters_ltx.md.


                                                  3
2.0.1   PAR. Global Parameter Register
PAR.0. Role Logical ID: PAR.
   This file fixes the structural constants used by the proof. Its purpose is to make all parameter
choices explicit and to prevent hidden dependencies between the HeathвЂ“Brown decomposition,
routing, Edge estimates, CKP/X10, BRS/TTH, and GoodAWACK.
   The register proves the following bookkeeping assertion: the displayed hierarchy of constants is
nonempty and is strong enough for all later uses of logarithmic losses, slice floors, near-global TC1
image lengths, and CKP/DFI smooth-weight thresholds.
   Used by: B1, C1, BRS, TTH, G3a, G8a, CKPD, X10, GEB, and I1.
   Uses: the constant outputs of X16C and CKPD.

PAR.1. Statement        There exist constants

                0 < рќњѓ в‰Є рќњ‚ в‰Є 1,       рќђЅ0 ,    рќђ¶0 , рќђ¶1 , рќђ¶16 , рќњЊ16 , рќђµ16 , рќђµрќњ… , рќђµHF , рќђ¶DFI , рќђµ
   which can be chosen in the order specified below and which satisfy all parameter inequalities
needed by the active proof tree.
   More precisely:

  1. the HeathвЂ“Brown depth рќђЅ0 can be chosen above the structural lower bound рќђЅ* (рќњ‚);

  2. all routing, Edge, CKP, BRS/TTH, X16, and X10 losses are bounded by fixed powers of
     log рќ‘Ѓ once рќђЅ0 is fixed;

  3. the later logarithmic exponents рќђµ16 , рќђµрќњ… , рќђµHF , рќђ¶DFI , and рќђµ can be enlarged without changing
     any earlier finite decomposition;

  4. the resulting global summability of terminal errors is available to Lemma GEB.

PAR.2. Order of choices        The parameters are chosen in the following order:

  1. choose small structural exponents 0 < рќњѓ в‰Є рќњ‚ в‰Є 1;

  2. choose the HeathвЂ“Brown depth рќђЅ0 в‰Ґ рќђЅ* (рќњ‚);

  3. fix the B1/B3/F3/F4 dyadic and routing complexity bounds рќђ¶0 (рќђЅ0 );

  4. fix the C1 strict-Edge polylogarithmic loss рќђ¶1 (рќђЅ0 );

  5. fix the X16-BRS carrier-slice constants рќђ¶16 (рќђЅ0 ) and рќњЊ16 (рќђЅ0 ) > 0 supplied by Lemma X16C;

  6. choose the X16 slice-floor exponent рќђµ16 large enough that the floor term рќ‘‹рќђ¶ (log рќ‘Ѓ )в€’рќђµ16 is
     strict C1 Edge after X16 losses;

  7. choose the BRS/TTH loss рќђµрќњ… larger than all preceding polylogarithmic losses and larger than
     рќђµ16 ;

  8. choose the CKP high-frequency and DFI smooth-weight thresholds large enough to dominate
     the G2a/G3a/G8a/X10 derivative losses, as quantified in Lemma CKPD;

  9. choose the auxiliary square-divisor exponent рќђµ after рќђ¶0 and рќђ¶1 , enlarged whenever C1/F4
     square-divisor routing requires it.

                                                  4
PAR.3. Parameter Table

 Parameter          Meaning               Source               Required condition
 рќђЅ0                 HeathвЂ“Brown           B1                   Fixed, рќђЅ0 в‰Ґ рќђЅ*
                    identity depth
 рќђЅ*                 lower bound ensur-    B1, PAR              рќђЅ* (рќњ‚)           =
                    ing bounded rout-                          max{10, вЊ€(4рќњ‚)в€’1 вЊ‰+
                    ing/CS/CKP com-                            1} is sufficient
                    plexity
 рќњѓ                  small-                B3, C1               0<рќњѓв‰Єрќњ‚
                    variable/range
                    cutoff
 рќњ‚                  large gcd/content     B3, G8a              fixed small positive
                    and       balanced-                        number
                    range cutoff
 рќђ¶0                 number            of  B1, C1, F3           рќђ¶0 = рќђ¶0 (рќђЅ0 )
                    typed/routing
                    cells
 рќђ¶1                 strict Edge coeffi-   C1                   рќђ¶1 = рќђ¶1 (рќђЅ0 )
                    cient/polylogarithmic
                    loss
 рќђ· = рќђїрќђµ             large       square-   C1, F4               рќђµ > рќђ¶1 + рќђ¶0 + 10,
                    divisor threshold                          enlarged as needed
 рќђ¶16                X16-BRS logarith-     X16C                 admissibly рќђ¶16 =
                    mic loss                                   100рќђЅ02 + 100, af-
                                                               ter harmless en-
                                                               largement
 рќњЊ16                X16-BRS power-       X16C                  admissibly рќњЊ16 =
                    saving remainder                           1/(106 рќђЅ04 )
 рќђµ16                X16      slice-floor X16C, BRS             choose рќђµ16 > рќђ¶0 +
                    exponent рќ‘Њ16 =                             рќђ¶1 + рќђ¶16 + 20
                    max(рќ‘Њ # , рќ‘‹рќђ¶ рќђїв€’рќђµ16 )
 рќђµрќњ…                 near-global    TC1   BRS, TTH              choose рќђµрќњ… > рќђµ16 +
                    image loss in TTH                          рќђ¶0 + рќђ¶1 + рќђ¶16 +
                                                               рќњЊв€’1
                                                                16 +20 after X16-
                                                               BRS is fixed
 рќђµHF                CKP           high-   h                    g\{}le             G2a, G8a, X10   dominates    G2a
                    frequency    cutoff                        LЛ†{B_{\{}mathrm{HF}}}\{})          Fourier     decay
                    \{}(                                                                          and X10 smooth-
                                                                                                  weight loss
 рќђ¶DFI               DFI       smooth-     CKPD, X10            fixed   by   Lemma
                    weight   derivative                        CKPD
                    loss




      Here and below рќђї = log рќ‘Ѓ .

PAR.4. Minimal Consistency Checks                      The following inequalities must hold simultaneously:

     1. C1/F4 square-divisor routing uses рќђµ > рќђ¶0 + рќђ¶1 + 10.

     2. X16/BRS uses рќђµ16 > рќђ¶0 + рќђ¶1 + рќђ¶16 + 20.

     3. BRS/TTH uses
                                     рќђµрќњ… > рќђµ16 + рќђ¶0 + рќђ¶1 + рќђ¶16 + рќњЊв€’1
                                                                 16 + 20.

     4. X9L-GT is invoked only after TTH supplies

                                                  рќђ» в‰Ґ рќ‘‹(log рќ‘‹)в€’рќђµрќњ… .



                                                          5
  5. X10 is invoked only in the central CKP range and only after the two-variable smooth weight
     рќ‘Љрќ‘”,в„Ћ (рќ‘Ћ, рќ‘ћ) satisfies the DFI derivative bounds with loss (log рќ‘Ѓ )рќђ¶DFI , as proved in CKPD.

  6. All sums over рќ‘”-layers use constants independent of рќ‘”. The only рќ‘”-dependence allowed is
     through the explicit dyadic scales рќђґрќ‘” , рќ‘„рќ‘” , рќ‘†рќ‘” and through summable powers handled by G4a
     and G8a.

PAR.5. Proof of Nonemptiness            The lower bound for рќђЅ* (рќњ‚) is conservative:

                                   рќђЅ* (рќњ‚) = max{10, вЊ€(4рќњ‚)в€’1 вЊ‰ + 1}.
   The constant 10 covers the fixed finite CauchyвЂ“Schwarz, generalized von Neumann, and routing-
complexity overheads. The term вЊ€(4рќњ‚)в€’1 вЊ‰ + 1 ensures that the HeathвЂ“Brown cutoff is not coarser
than the large-gcd/content hierarchy used in the balanced CKP and TC1 ranges.
   One concrete witness is
                                     1                1
                               рќњ‚=       ,       рќњѓ=        ,      рќђЅ0 = 20.
                                     40              4000
   Then

                               рќђЅ* (рќњ‚) = max{10, вЊ€(4рќњ‚)в€’1 вЊ‰ + 1} = 11,
   so рќђЅ0 в‰Ґ рќђЅ* (рќњ‚). After рќђЅ0 is fixed, Lemma X16C supplies admissible constants
                                                                        1
                              рќђ¶16 = 100рќђЅ02 + 100,             рќњЊ16 =             .
                                                                      106 рќђЅ04
   Choose

                               рќђµ16 = вЊ€рќђ¶0 (рќђЅ0 ) + рќђ¶1 (рќђЅ0 ) + рќђ¶16 + 21вЊ‰
   and then choose
                              вЊ€пёЃ                                                    вЊ‰пёЃ
                        рќђµрќњ… = рќђµ16 + рќђ¶0 (рќђЅ0 ) + рќђ¶1 (рќђЅ0 ) + рќђ¶16 + рќњЊв€’1
                                                                16 + 21 .

    The CKP high-frequency threshold рќђµHF , the DFI derivative-loss constant рќђ¶DFI , and the auxil-
iary square-divisor exponent рќђµ are then chosen after these quantities, large enough for the inequal-
ities in PAR.4. Enlarging any of these later constants is harmless because all affected families are
finite once рќђЅ0 is fixed.
    This proves that the hierarchy in PAR.1 is nonempty.

PAR.6. Notational Conventions               The singular series is denoted throughout by

                                                  S(рќ‘Ѓ ).
   The proof does not use a separate Sing(N) symbol. Terminal class names are written in prose
as Edge, LongAP/Local, CKP, GoodAWACK, and LocalDiag, and in displayed formulae as

             Edge,      LongAP/Local,            CKP,         GoodAWACK,                 LocalDiag.
   No independent macros such as в€–рќђ¶рќђѕрќ‘ѓ or в€–рќђєрќ‘њрќ‘њрќ‘‘рќђґрќ‘Љ рќђґрќђ¶рќђѕ are part of the source convention.



                                                     6
Remark 2.1 (PAR.7. Output). The proof tree should not use disconnected phrases such as "take all
parameters sufficiently large". All later parameter choices must be compatible with this register.
    If the Shiu/AP X16 proof, the CKP/X10 derivative appendix, or the MRT/PACK interface
changes, this parameter register must be checked before the proof tree can again be treated as
closed.

PAR.8. Logical Dependencies Internal inputs used: X16C, CKPD.
  Internal nodes served: B1, C1, BRS, TTH, G3a, G8a, X10, GEB, and I1.


3     Part 2. GEB: Global error budget
Source file: Lemmas/global_error_budget_ltx.md.

3.0.1    GEB. Global Error Budget and Parameter Hierarchy
GEB.0. Role Logical ID: GEB.
    Lemma GEB is an internal bookkeeping lemma. It does not introduce a new analytic estimate.
Its role is to prove that, with the parameter hierarchy of PAR, all terminal error terms produced by
the proof tree are summable and contribute рќ‘њ(рќ‘Ѓ ) after the finite B1/B3/F3/F4 decomposition.
    Used by: I1.
    Uses: PAR, B1, B3, F3, F3T, F4, C1A, C1, D1, G8a, CKPD, E10L, TNG, X16BRS, X16C, TTH, and H4.
    External inputs used through their stated forms: X9, X10, and X16.

GEB.1. Statement After fixing the parameters in the order prescribed by PAR, the following
assertions hold uniformly over all tagged terminal cells in the proof tree:

    1. every strict Edge contribution is рќ‘њ(рќ‘Ѓ ) after summing over all cells;

    2. every nonzero CKP contribution is рќ‘њ(рќ‘Ѓ );

    3. every GoodAWACK TC1 contribution surviving to X9L-GT is рќ‘њ(рќ‘Ѓ );

    4. every singular BRS/X16 carrier-slice remainder is either strict Edge or рќ‘њ(рќ‘Ѓ );

    5. all local/main terms admitted by D1, G8a, and LocalDiag recombine through H4 into S(рќ‘Ѓ )рќ‘Ѓ +
       рќ‘њ(рќ‘Ѓ ).

    Consequently the I1 assembly may write

                                      рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ )
    without hiding any additional summation over terminal families.

GEB.2. Setup and Constant Order               Let рќђї = log рќ‘Ѓ . Constants are fixed in the following
order:

    1. choose 0 < рќњѓ в‰Є рќњ‚ в‰Є 1;

    2. choose рќђЅ0 в‰Ґ рќђЅ* (рќњ‚);

    3. fix the finite routing and dyadic complexity constant рќђ¶0 (рќђЅ0 );

                                                   7
  4. fix the strict Edge polylogarithmic loss рќђ¶1 (рќђЅ0 );

  5. fix рќђ¶16 (рќђЅ0 ) and рќњЊ16 (рќђЅ0 ) > 0 from X16C;

  6. choose рќђµ16 > рќђ¶0 + рќђ¶1 + рќђ¶16 + 20;

  7. choose рќђµрќњ… > рќђµ16 + рќђ¶0 + рќђ¶1 + рќђ¶16 + рќњЊв€’1
                                        16 + 20;

  8. choose the CKP high-frequency and DFI derivative thresholds after the preceding constants;

  9. enlarge the auxiliary square-divisor exponent рќђµ after рќђ¶0 and рќђ¶1 .

   The hierarchy is nonempty by PAR. A concrete consistency witness is
                                         1                1
                                   рќњ‚=       ,      рќњѓ=         ,         рќђЅ0 = 20.
                                         40              4000
   For this witness

                                   рќђЅ* (рќњ‚) = max{10, вЊ€(4рќњ‚)в€’1 вЊ‰ + 1} = 11,
   so рќђЅ0 в‰Ґ рќђЅ* (рќњ‚). After рќђЅ0 is fixed, Lemma X16C supplies
                                                                            1
                                  рќђ¶16 = 100рќђЅ02 + 100,             рќњЊ16 =           .
                                                                          106 рќђЅ04
    Then рќђµ16 , рќђµрќњ… , the CKP thresholds, and рќђµ are chosen by the inequalities above. Enlarging any
later logarithmic exponent is harmless because рќђЅ0 and the routing grammar are already fixed.

GEB.3. Polylogarithmic Multiplicity Principle For fixed рќђЅ0 , the B1 HeathвЂ“Brown expan-
sion, the smooth dyadic partitions, and the B3/F3/F4 routing grammar create at most рќђїрќђ¶0 terminal
cells after harmless enlargement of рќђ¶0 .
    Therefore:

  1. a per-cell estimate рќ‘‚(рќ‘Ѓ рќђїв€’рќђ¶0 в€’рќђґ ) with fixed рќђґ > 0 sums to рќ‘‚(рќ‘Ѓ рќђїв€’рќђґ ) = рќ‘њ(рќ‘Ѓ );

  2. a per-cell estimate рќ‘‚(рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶ ) with fixed рќњЊ > 0 sums to рќ‘њ(рќ‘Ѓ );

  3. a normalized testing estimate рќ‘њ(1) multiplied by an рќђїрќ‘‚(1) -complexity family remains рќ‘њ(1)
     after the Davenport/AP saving exponent is chosen larger than the recorded polylogarithmic
     losses.

    This principle is applied only after the corresponding branch lemma has verified that its input
is one of the terminal classes.

GEB.4. Global Loss Table

 Source                 Estimate before global   Multiplicity or loss      Parameter condition   Global conclusion
                        summation
 B1 dyadic decomposi-   exact identity and       at most рќђїрќђ¶0 cells         fixed рќђЅ0              no error
 tion                   smooth partition
 F3/F4 routing          exact tagged terminal    at most рќђїрќђ¶0 cells         termination by Mв™Ї     no error
                        partition




                                                          8
 C1 Edge                 рќ‘Ѓ рќђїв€’рќђ¶0 в€’10           or      рќђїрќђ¶0 cells                 C1A admission    and    рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ )
                         рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1     per ad-                                  fixed рќњЊ > 0
                         mitted atom
 D1 LongAP/Local         canonical LPI local          boundary terms C1-        C1P/C1A/C1 and LPI/H4       local projection +рќ‘њ(рќ‘Ѓ )
                         projection plus bound-       admitted                  compatibility
                         ary/error terms
 CKP excluded ranges     strict Edge,      high-      polylogarithmic   рќ‘”, в„Ћ-   X10ER, C1P/C1A/C1, G1a,     рќ‘њ(рќ‘Ѓ ) or LPI local term
                         frequency decay, small       families                  G2a, G8a, B1LD          assembled by H4
                         conductor, large рќ‘”, or
                         local zero frequency
 CKP central nonzero     DFI-X10 bound in the         CKPD derivative loss      X10         hypotheses  рќ‘њ(рќ‘Ѓ )
 frequencies             central Kloosterman-         and    polylogarithmic    matched in CKPD;
                         fraction range               рќ‘”, в„Ћ-sum                  thresholds chosen after
                                                                                PAR
 GoodAWACK        TC1    normalized     X9L-GT        PACK family and           TNG/TTH give рќђ» в‰Ґ        рќ‘њ(рќ‘Ѓ )
 regular branch          Davenport/AP        esti-    polylogarithmic  AP       рќ‘‹(log рќ‘‹)в€’рќђµрќњ… and X9
                         mate рќ‘њ(1)                    complexity                is invoked only there
 GoodAWACK singular      singular tests route to      no independent short-     TTD/ROC/BRS/X16BRS/X16C handled by     existing
 branch                  Edge, LongAP/Local,          interval input                                    branches
                         CKP, LocalDiag, or
                         zero
 X16/BRS carrier slice   рќ‘Ѓ (log рќ‘Ѓ )рќђ¶16 рќ‘Њ16 /рќ‘‹рќ‘ѓ +      floor loss рќ‘Њ16    =       рќђµ16 > рќђ¶0 + рќђ¶1 + рќђ¶16 +   strict Edge or рќ‘њ(рќ‘Ѓ )
                         рќ‘Ѓ 1в€’рќњЊ16 (log рќ‘Ѓ )рќђ¶16 af-      рќ‘‹рќђ¶ рќђїв€’рќђµ16       where      20
                         ter normalization            needed
 GoodAWACK HighTC        untagged           rank-     finite  GoodAWACK         E10Y/E10X/E10M/E10Kno residual FreeAffine-
 finite grammar          dropping      AFF      is    grammar                                      HighTC
                         impossible;       tagged
                         alternatives route to
                         existing classes
 LPI/H4 local projec-    рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ )+рќ‘њ(рќ‘Ѓ ) for the      finite CRT/local pro-     рќ‘¤(рќ‘Ѓ ) в†’ в€ћ, рќ‘¤(рќ‘Ѓ ) =      S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ )
 tion                    admitted local model         jection family            рќ‘њ(log рќ‘Ѓ )




   Each row is used only through its named branch lemmas. Lemma GEB records the global
summation and compatibility of losses; it does not replace C1, G8a, E10L, X16C, X9, X10, H4, or the
separate prime-power removal lemma G2.

GEB.5. Proof By B1, B3, F3P, F3, F3T, and F4, the weighted Goldbach sum is exactly decom-
posed into a finite tagged family of terminal contributions. The number of terminal cells is bounded
by рќђїрќђ¶0 .
   For Edge terms, C1A verifies that each Edge input satisfies one of the strict C1 predicates.
Lemma C1 gives either рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 or рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 per cell. The polylogarithmic multiplicity principle
therefore gives

                                                     рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
    For LongAP/Local terms, F3P gives the positive local-coefficient predicate and D1 expands
those atoms into the LPI local projection. For LocalDiag terms, the intrinsic local-dependence tag
is admitted through LPI and assembled by H4. Boundary and smooth-partition discrepancies are
C1-admitted. Hence these branches contribute the LPI local model assembled by H4 plus рќ‘њ(рќ‘Ѓ ).
    For CKP terms, G8a separates zero and nonzero frequencies. The zero-frequency terms are
admitted into H4 through B1LD. Excluded nonzero ranges are routed through X10ER and C1P/C1A/C1.
The central nonzero range is matched to the DFI theorem by CKPD and X10; the remaining poly-
logarithmic losses are dominated by the CKP thresholds chosen after PAR. Thus the total CKP
nonlocal contribution is рќ‘њ(рќ‘Ѓ ).



                                                              9
    For GoodAWACK terms, E10L applies the TC1/HighTC dichotomy. The TC1 regular branch
is packaged by TNG and reaches X9L-GT only after TTH supplies the near-global length

                                                рќђ» в‰Ґ рќ‘‹(log рќ‘‹)в€’рќђµрќњ… .
    The Davenport/AP saving exponent dominates the PACK and modulus losses recorded in PAR.
The TC1 contribution is therefore рќ‘њ(рќ‘Ѓ ). Singular B1-origin tests are routed by TTD/ROC/BRS, with
X16BRS/X16C controlling carrier-slice remainders; the slice-floor condition on рќђµ16 puts the residual
floor term inside strict Edge, and the power-saving term is summable. The HighTC/grammar
branch is closed by E10Y/E10X/E10M/E10K, so no untagged rank-dropping AFF residual remains.
    Lemma H4 then sums all admitted local projections into

                                                 рќ‘Ѓ рќњЋрќ‘„ (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ )
    and proves рќњЋрќ‘„ (рќ‘Ѓ ) в†’ S(рќ‘Ѓ ). Combining the rows of the global loss table gives

                                         рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
    This proves Lemma GEB.
Remark 3.1 (GEB.6. Output). Lemma GEB supplies I1 with a single global error statement: after
all terminal branches are evaluated, the remaining nonlocal and boundary contributions are рќ‘њ(рќ‘Ѓ ),
while the admitted local branches combine to S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).

GEB.7. Logical Dependencies Internal dependencies: PAR, B1, B3, F3, F3T, F4, C1A, C1, D1,
G8a, CKPD, E10L, TNG, X16BRS, X16C, TTH, and H4.
   External dependencies: X9 and X10 only through their stated forms, and X16 only through the
X16C/X16BRS interface.


4     Part 3. X1: HeathвЂ“Brown identity verification
Source file: External/x_1_heath_brown_identity_verification_ltx.md.

4.0.1    X1. HeathвЂ“Brown Identity Input for B1
X1.0. Statement and Role This document verifies the external dependency X1 used by Lemma
B1. The required input is the exact HeathвЂ“Brown identity
                             рќђЅ0
                                           (пёѓ    )пёѓ
                                            рќђЅ0
                    О›(рќ‘›) =        (в€’1)                                       рќњ‡(рќ‘љ1 ) В· В· В· рќњ‡(рќ‘љрќ‘— ) log рќ‘џ1
                             в€‘пёЃ                              в€‘пёЃ
                                     рќ‘—в€’1

                             рќ‘—=1
                                            рќ‘—         рќ‘љ1 В·В·В·рќ‘љрќ‘— рќ‘џ1 В·В·В·рќ‘џрќ‘— =рќ‘›
                                                            рќ‘љрќ‘– в‰¤рќ‘¦

    for рќ‘› в‰¤ рќ‘¦ рќђЅ0 . In B1 one takes рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 , so this must apply for every рќ‘› в‰¤ рќ‘Ѓ .
    The proof obligations for X1 are:

    1. Does the displayed formula match a valid HeathвЂ“Brown identity?

    2. Does the choice рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 put all B1 arguments in the exact range?

    3. Does the subsequent dyadic localization introduce any error or hidden coefficient type?



                                                            10
   External source:
   D. R. Heath-Brown, *Prime numbers in short intervals and a generalized Vaughan identity*,
Canadian Journal of Mathematics 34 (1982), no. 6, 1365вЂ“1377, DOI 10.4153/CJM-1982-095-9.
   The proof below records the exact finite identity in the range used by B1; no analytic estimate
from the paper is invoked.

X1.1. Formal identity       Let рќђЅ в‰Ґ 1, рќ‘¦ в‰Ґ 1, and

                       рќњ‡рќ‘¦ (рќ‘›) := рќњ‡(рќ‘›)1рќ‘›в‰¤рќ‘¦ ,               1(рќ‘›) := 1,              рќђї(рќ‘›) := log рќ‘›.
   All convolutions below are Dirichlet convolutions. The identity needed by B1 is

                                       рќђЅ
                                                        (пёѓ )пёѓ
                                                          рќђЅ (пёЃ *рќ‘—             )пёЃ
                          О›(рќ‘›) =           (в€’1)               рќњ‡рќ‘¦ * рќђї * 1*(рќ‘—в€’1) (рќ‘›)                         (X1.1)
                                      в€‘пёЃ
                                                  рќ‘—в€’1

                                      рќ‘—=1
                                                          рќ‘—

   for every рќ‘› в‰¤ рќ‘¦ рќђЅ . Expanding the convolution gives exactly the B1 formula, with рќ‘џ1 carrying
the logarithm and рќ‘џ2 , . . . , рќ‘џрќ‘— carrying the 1-weights.

X1.2. Proof of the identity           Write formal Dirichlet series only as a coefficient bookkeeping
device:

                                            рќђ·(рќ‘“ ; рќ‘ ) =              рќ‘“ (рќ‘›)рќ‘›в€’рќ‘  .
                                                              в€‘пёЃ

                                                              рќ‘›в‰Ґ1

   Then

                                                                                               рќњЃ вЂІ (рќ‘ )
                   рќђ·(1; рќ‘ ) = рќњЃ(рќ‘ ),           рќђ·(рќђї; рќ‘ ) = в€’рќњЃ вЂІ (рќ‘ ),                 рќђ·(О›; рќ‘ ) = в€’           .
                                                                                               рќњЃ(рќ‘ )
   Let

                                              рќ‘Ђрќ‘¦ (рќ‘ ) = рќђ·(рќњ‡рќ‘¦ ; рќ‘ ).
   The Dirichlet series of the right side of (X1.1) is
                                             рќђЅ
                                                              (пёѓ )пёѓ
                                  вЂІ                                рќђЅ
                              (в€’рќњЃ (рќ‘ ))           (в€’1)                рќ‘Ђрќ‘¦ (рќ‘ )рќ‘— рќњЃ(рќ‘ )рќ‘—в€’1 .
                                            в€‘пёЃ
                                                        рќ‘—в€’1

                                            рќ‘—=1
                                                                   рќ‘—

   Factoring one рќњЃ(рќ‘ )в€’1 , this becomes
                                          рќђЅ
                                 рќњЃ вЂІ (рќ‘ ) в€‘пёЃ
                                                              (пёѓ )пёѓ
                                                    рќђЅ (пёЂ           )пёЂрќ‘—
                               в€’            (в€’1)рќ‘—в€’1      рќ‘Ђрќ‘¦ (рќ‘ )рќњЃ(рќ‘ ) .
                                 рќњЃ(рќ‘ ) рќ‘—=1           рќ‘—

   The binomial sum is
                                 рќђЅ
                                                    (пёѓ )пёѓ
                                                     рќђЅ
                                      (в€’1)             рќђґрќ‘— = 1 в€’ (1 в€’ рќђґ)рќђЅ .
                                в€‘пёЃ
                                             рќ‘—в€’1

                                рќ‘—=1
                                                     рќ‘—

   Therefore the right side of (X1.1) has Dirichlet series
                                               (пёЃ                                )пёЂрќђЅ )пёЃ
                                 рќђ·(О›; рќ‘ ) 1 в€’ 1 в€’ рќ‘Ђрќ‘¦ (рќ‘ )рќњЃ(рќ‘ )                                                (X1.2)
                                                         (пёЂ
                                                                                          .

                                                              11
   Let

                                              рќђµ := рќ›ї1 в€’ рќњ‡рќ‘¦ * 1.
   For 1 < рќ‘› в‰¤ рќ‘¦,

                              (рќњ‡рќ‘¦ * 1)(рќ‘›) =                   рќњ‡(рќ‘‘) =          рќњ‡(рќ‘‘) = 0,
                                                 в€‘пёЃ                     в€‘пёЃ

                                               рќ‘‘|рќ‘›, рќ‘‘в‰¤рќ‘¦                 рќ‘‘|рќ‘›

   and for рќ‘› = 1 the same convolution equals 1. Hence

                               рќђµ(1) = 0,            рќђµ(рќ‘›) = 0          (1 < рќ‘› в‰¤ рќ‘¦).
    Thus every nonzero coefficient of рќђµ is supported on рќ‘› > рќ‘¦. Consequently every nonzero coeffi-
cient of рќђµ *рќђЅ is supported on рќ‘› > рќ‘¦ рќђЅ .
    From (X1.2), the difference between О› and the right side of (X1.1) is О› * рќђµ *рќђЅ . Since рќђµ *рќђЅ is
supported on рќ‘› > рќ‘¦ рќђЅ , this difference has zero coefficient for every рќ‘› в‰¤ рќ‘¦ рќђЅ . This proves (X1.1).

X1.3. Match with Lemma B1             Lemma B1 fixes a sufficiently large constant рќђЅ0 and takes

                                                 рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 .
   Therefore

                                                    рќ‘Ѓ = рќ‘¦ рќђЅ0 .
   Every positive argument рќ‘› appearing in either copy of

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

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

   satisfies 1 в‰¤ рќ‘› в‰¤ рќ‘Ѓ = рќ‘¦ рќђЅ0 . The exact identity above applies to both О›(рќ‘›1 ) and О›(рќ‘›2 ). The
case рќ‘› = 1 is harmless because log 1 = 0, and рќ‘› = 0 is not an argument of О› in the positive-integer
Goldbach convolution.
   The coefficient types in B1 are also exactly those generated by (X1.1):

                             рќњ‡(рќ‘љрќ‘– )1рќ‘љрќ‘– в‰¤рќ‘¦ ,         log рќ‘џ1 ,       1 on рќ‘џ2 , . . . , рќ‘џрќ‘— .
    There is no missing factor of рќ‘—. The logarithm is attached to one ordered рќ‘џ-variable; this
corresponds to the single factor в€’рќњЃ вЂІ (рќ‘ )рќњЃ(рќ‘ )рќ‘—в€’1 , not to differentiating рќњЃ(рќ‘ )рќ‘— .

X1.4. Dyadic localization check          After the identity, B1 inserts an exact smooth dyadic parti-
tion

                                                         рќњ”рќ‘‹ (рќ‘Ј) = 1
                                               в€‘пёЃ

                                                рќ‘‹

    for each positive HeathвЂ“Brown variable рќ‘Ј. On the support of a factorization of рќ‘› в‰¤ рќ‘Ѓ , every
variable is at most рќ‘Ѓ , so only рќ‘‚(log рќ‘Ѓ ) dyadic scales occur per variable. Since рќђЅ0 is fixed, the total
number of dyadic blocks in the two-sided Goldbach decomposition is

                                              рќ‘‚рќђЅ0 (log рќ‘Ѓ )4рќђЅ0 ,
                                                    (пёЂ             )пёЂ



                                                           12
    as stated in B1. This localization is exact and creates no analytic error term.
    The dyadic weights preserve the B1 coefficient classes:

                                 рќњ‡ В· 1в‰¤рќ‘¦ В· рќњ”рќ‘‹ ,       (log) В· рќњ”рќ‘‹ ,       рќњ”рќ‘‹ .
   Their pointwise sizes are divisor/polylog bounded on each block, with the only unbounded
elementary factor being log рќ‘џ1 в‰¤ log рќ‘Ѓ .

X1.5. Output for B1        The X1 input supplies exactly what Lemma B1 uses:

    1. exact finite decomposition of every О›(рќ‘›), 1 в‰¤ рќ‘› в‰¤ рќ‘Ѓ ;

    2. no truncation error from the HeathвЂ“Brown identity;

    3. no error from dyadic localization;

    4. no extra coefficient type beyond рќњ‡1в‰¤рќ‘¦ , 1, and log;

    5. fixed-рќђЅ0 polylogarithmic block count.

   Thus the B1 output used by I1 is not conditional on an unverified analytic estimate. X1 is a
standard formal identity whose applicability is checked in the exact B1 range.
Parameter check 4.1 (X1.6. Parameter check and conclusion).

                                X1 is verified in the exact B1 range.

   The HeathвЂ“Brown identity used in Lemma B1 is valid for the chosen рќђЅ0 and рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 . It
applies to every positive argument in the Goldbach convolution, and the subsequent smooth dyadic
decomposition remains exact. X1 is a closed external input for the proof tree.

X1.7. Logical dependencies         Internal dependency served: B1.


5     Part 4. B1: Typed HeathвЂ“Brown decomposition
Source file: Lemmas/b_1_ltx.md.

5.0.1    B1. Typed HeathвЂ“Brown Decomposition
B1.0. Role Logical ID: B1.
  Lemma B1 is the first technical decomposition node. Its purpose is to replace the two von
Mangoldt factors in

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

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

   by a finite sum of typed smooth dyadic finite-convolution blocks. No estimate is made and no
contribution is discarded at this stage.
   Used by: B3, F3, F4, I1, H4, BGS, E10M, E10X, the CKP branch, the GoodAWACK branch, and
the X16 carrier-slice branch.
   Uses: PAR for the structural depth рќђЅ0 , X1 for the HeathвЂ“Brown identity, and X2 for the smooth
dyadic partition of unity.

                                                      13
B1.1. Statement       For fixed sufficiently large рќђЅ0 and рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 , the Goldbach sum has the exact
decomposition

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

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

     where each рќ‘…в„¬ (рќ‘Ѓ ) is a typed smooth dyadic finite-convolution block of the form
                                                  рќ‘џ            рќ‘ 
                                                       рќ‘Ћрќ‘– +         рќ‘Џрќ‘— = рќ‘Ѓ,
                                                 в€ЏпёЃ           в€ЏпёЃ

                                                 рќ‘–=1          рќ‘—=1

     with

                                                        рќ‘џ, рќ‘  в‰¤ 2рќђЅ0 .
     The elementary coefficient types are

                                            рќњ‡ В· 1в‰¤рќ‘¦ ,            1,        log .
     The number of blocks satisfies

                                            #BрќђЅ0 в‰ЄрќђЅ0 (log рќ‘Ѓ )4рќђЅ0 .
     The decomposition is exact; no error term is created at the B1 stage.

B1.2. Parameter and Range Setup                    Fix the structural HeathвЂ“Brown depth

                                                          рќђЅ0 в‰Ґ рќђЅ* ,
     as allowed by PAR. The value рќђЅ0 is a fixed constant of the proof, not a variable depending on
рќ‘Ѓ.
     Set

                                                        рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 .
     Then every рќ‘› в‰¤ рќ‘Ѓ satisfies

                                                          рќ‘› в‰¤ рќ‘¦ рќђЅ0 .
     This is the range in which the exact HeathвЂ“Brown identity is applied.

B1.3. Exact HeathвЂ“Brown Identity                      For рќ‘› в‰¤ рќ‘Ѓ and рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 , X1 supplies the exact identity
                             рќђЅ0
                                            (пёѓ     )пёѓ
                                              рќђЅ0
                    О›(рќ‘›) =        (в€’1)                                         рќњ‡(рќ‘љ1 ) В· В· В· рќњ‡(рќ‘љрќ‘— ) log рќ‘џ1 .
                             в€‘пёЃ                                в€‘пёЃ
                                      рќ‘—в€’1

                             рќ‘—=1
                                              рќ‘—         рќ‘љ1 В·В·В·рќ‘љрќ‘— рќ‘џ1 В·В·В·рќ‘џрќ‘— =рќ‘›
                                                          рќ‘љ1 ,...,рќ‘љрќ‘— в‰¤рќ‘¦

     Denote the inner рќ‘—-th contribution by

                             О›рќ‘— (рќ‘›) =                           рќњ‡(рќ‘љ1 ) В· В· В· рќњ‡(рќ‘љрќ‘— ) log рќ‘џ1 .
                                                  в€‘пёЃ

                                         рќ‘љ1 В·В·В·рќ‘љрќ‘— рќ‘џ1 В·В·В·рќ‘џрќ‘— =рќ‘›
                                           рќ‘љ1 ,...,рќ‘љрќ‘— в‰¤рќ‘¦

     Then

                                                              14
                                    рќђЅ0
                                                                                          (пёѓ   )пёѓ
                                                                                           рќђЅ0
                           О›(рќ‘›) =         рќ‘ђрќ‘— О›рќ‘— (рќ‘›),               рќ‘ђрќ‘— = (в€’1)
                                    в€‘пёЃ
                                                                                    рќ‘—в€’1
                                                                                              .
                                    рќ‘—=1
                                                                                           рќ‘—

   This identity is exact on the range рќ‘› в‰¤ рќ‘Ѓ .

B1.4. Elementary Coefficient Types                 Each рќ‘—-block contains 2рќ‘— variables:

                                         рќ‘љ1 , . . . , рќ‘љрќ‘— , рќ‘џ1 , . . . , рќ‘џрќ‘— .
   The elementary coefficient types are

                                        рќ›јрќ‘љрќ‘– (рќ‘љрќ‘– ) = рќњ‡(рќ‘љрќ‘– )1рќ‘љрќ‘– в‰¤рќ‘¦ ,


                                              рќ›јрќ‘џ1 (рќ‘џ1 ) = log рќ‘џ1 ,
   and

                                    рќ›јрќ‘џрќ‘– (рќ‘џрќ‘– ) = 1                 (2 в‰¤ рќ‘– в‰¤ рќ‘—).
   Thus all elementary types belong to

                                              {рќњ‡ В· 1в‰¤рќ‘¦ , 1, log}.
    After dyadic localization these coefficients become smooth dyadic coefficient sequences, but
their arithmetic type remains the same.

B1.5. Exact Smooth Dyadic Partition                     Let

                                              рќњ” в€€ рќђ¶рќ‘ђв€ћ ([1/2, 2])
   be non-negative and satisfy

                                                    рќ‘Ў
                                              (пё‚        )пё‚
                                                             =1            (рќ‘Ў > 0).
                                    в€‘пёЃ
                                          рќњ”
                                    рќ‘в€€Z
                                                   2рќ‘

   For the dyadic scale рќ‘‹ = 2рќ‘ , set

                                                                       рќ‘Ў
                                                                  (пё‚       )пё‚
                                              рќњ”рќ‘‹ (рќ‘Ў) = рќњ”                        .
                                                                       рќ‘‹
   Then for every positive integer рќ‘›,

                                               1=                рќњ”рќ‘‹ (рќ‘›),
                                                         в€‘пёЃ

                                                             рќ‘‹

   where the sum ranges over dyadic scales. If рќ‘› в‰¤ рќ‘Ѓ , only рќ‘‚(log рќ‘Ѓ ) scales occur.
   For each variable рќ‘Ј in a HeathвЂ“Brown block, insert the exact partition

                                               1=                рќњ”рќ‘‰ (рќ‘Ј).
                                                         в€‘пёЃ

                                                             рќ‘‰

   Since this is a partition of unity, the dyadic decomposition creates no error.


                                                             15
B1.6. Dyadically Localized Blocks for О›                                       For a tuple of dyadic scales

                                                     X = (рќ‘Ђ1 , . . . , рќ‘Ђрќ‘— , рќ‘…1 , . . . , рќ‘…рќ‘— )
    define
                                                          вЋ›                                   вЋћ
                                                               рќ‘—                                                          рќ‘—
               О›рќ‘—,X (рќ‘›) =                                           рќњ‡(рќ‘љрќ‘– )рќњ”рќ‘Ђ (рќ‘љрќ‘– )вЋ  (log рќ‘џ1 )рќњ”рќ‘… (рќ‘џ1 )                          рќњ”рќ‘…рќ‘– (рќ‘џрќ‘– ).
                                            в€‘пёЃ                в€ЏпёЃ                                                         в€ЏпёЃ
                                                          вЋќ
                                                                                     рќ‘–                           1
                                   рќ‘љ1 В·В·В·рќ‘љрќ‘— рќ‘џ1 В·В·В·рќ‘џрќ‘— =рќ‘›       рќ‘–=1                                                        рќ‘–=2
                                     рќ‘љ1 ,...,рќ‘љрќ‘— в‰¤рќ‘¦

    The exact decomposition becomes
                                                            рќђЅ0
                                              О›(рќ‘›) =                         О›рќ‘—,X (рќ‘›),
                                                            в€‘пёЃ         в€‘пёЃ
                                                                  рќ‘ђрќ‘—                               рќ‘› в‰¤ рќ‘Ѓ.
                                                            рќ‘—=1          X

   The sum over X is finite. Every variable on the support is at most рќ‘Ѓ , so each variable has
рќ‘‚(log рќ‘Ѓ ) possible dyadic choices. Let рќђ·рќђЅ0 (рќ‘Ѓ ) denote the number of admissible dyadic choices.
Since the number of variables is at most 2рќђЅ0 ,

                                                          рќђ·рќђЅ0 (рќ‘Ѓ ) в‰ЄрќђЅ0 (log рќ‘Ѓ )2рќђЅ0 .

B1.7. Goldbach Block Expansion                                 Insert the localized decomposition into

                                                     рќ‘…О› (рќ‘Ѓ ) =                           О›(рќ‘›1 )О›(рќ‘›2 ).
                                                                           в€‘пёЃ

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

    This gives the exact identity
                                                                  рќђЅ0
                                              рќ‘…О› (рќ‘Ѓ ) =                                    рќ‘…рќ‘—,рќ‘— вЂІ ,X,Y (рќ‘Ѓ ),
                                                                  в€‘пёЃ                 в€‘пёЃ
                                                                           рќ‘ђрќ‘— рќ‘ђрќ‘— вЂІ
                                                                рќ‘—,рќ‘— вЂІ =1             X,Y

    where

                                          рќ‘…рќ‘—,рќ‘— вЂІ ,X,Y (рќ‘Ѓ ) =                          О›рќ‘—,X (рќ‘›1 )О›рќ‘— вЂІ ,Y (рќ‘›2 ).
                                                                           в€‘пёЃ

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

    Expanding the convolutions, each such block has the form


рќ‘…рќ‘—,рќ‘— вЂІ ,X,Y (рќ‘Ѓ ) =                                                     рќђґрќ‘—,X (рќ‘љ1 , . . . , рќ‘љрќ‘— , рќ‘џ1 , . . . , рќ‘џрќ‘— )рќђµрќ‘— вЂІ ,Y (рќ‘љвЂІ1 , . . . , рќ‘љвЂІрќ‘— вЂІ , рќ‘џ1вЂІ , . . . , рќ‘џрќ‘—вЂІ вЂІ ),
                                          в€‘пёЃ

                     рќ‘љ1 В·В·В·рќ‘љрќ‘— рќ‘џ1 В·В·В·рќ‘џрќ‘— +рќ‘љвЂІ1 В·В·В·рќ‘љвЂІрќ‘— вЂІ рќ‘џ1вЂІ В·В·В·рќ‘џрќ‘—вЂІ вЂІ =рќ‘Ѓ
                                   рќ‘љ1 ,...,рќ‘љрќ‘— в‰¤рќ‘¦
                                   рќ‘љвЂІ1 ,...,рќ‘љвЂІрќ‘— вЂІ в‰¤рќ‘¦


    where
                                            вЋ›                                  вЋћ
                                                 рќ‘—                                                          рќ‘—
                               рќђґрќ‘—,X = вЋќ              рќњ‡(рќ‘љрќ‘– )рќњ”рќ‘Ђрќ‘– (рќ‘љрќ‘– )вЋ  (log рќ‘џ1 )рќњ”рќ‘…1 (рќ‘џ1 )                         рќњ”рќ‘…рќ‘– (рќ‘џрќ‘– ),
                                                в€ЏпёЃ                                                         в€ЏпёЃ

                                               рќ‘–=1                                                         рќ‘–=2

    and рќђµрќ‘— вЂІ ,Y is defined in the same way on the second side.
    This is a typed dyadic finite-convolution block.



                                                                              16
B1.8. Block Count and Coefficient Bounds The number of choices of (рќ‘—, рќ‘— вЂІ ) is at most рќђЅ02 .
For each side the number of dyadic choices is рќ‘‚рќђЅ0 ((log рќ‘Ѓ )2рќђЅ0 ). Hence

                                       #BрќђЅ0 в‰ЄрќђЅ0 (log рќ‘Ѓ )4рќђЅ0 .
   Since рќђЅ0 is fixed, this is a polylogarithmic number of blocks. Therefore any block-level estimate
with saving

                                          рќ‘‚(рќ‘Ѓ (log рќ‘Ѓ )в€’рќђґ )
   for sufficiently large рќђґ = рќђґ(рќђЅ0 ) can be summed over all typed blocks. The general record needed
by the proof is the bound (log рќ‘Ѓ )4рќђЅ0 .
   On each dyadic block the elementary coefficients satisfy divisor-bounded estimates. For the
рќњ‡-variables,

                                       |рќњ‡(рќ‘љрќ‘– )рќњ”рќ‘Ђрќ‘– (рќ‘љрќ‘– )| в‰¤ 1.
   For unit variables,

                                          |рќњ”рќ‘…рќ‘– (рќ‘џрќ‘– )| в‰¤ рќђ¶рќњ” .
   For the logarithmic variable,

                                     | log рќ‘џ1 рќњ”рќ‘…1 (рќ‘џ1 )| в‰Є log рќ‘Ѓ.
   Thus each full coefficient in a typed block is polylogarithmically bounded:

                                         в‰ЄрќђЅ0 (log рќ‘Ѓ )рќђ¶(рќђЅ0 ) .
   This is the coefficient loss allowed by the later branches.

B1.9. Proof By the HeathвЂ“Brown identity with fixed рќђЅ0 and рќ‘¦ = рќ‘Ѓ 1/рќђЅ0 , the function О›(рќ‘›) has
an exact finite decomposition into the contributions О›рќ‘— (рќ‘›), 1 в‰¤ рќ‘— в‰¤ рќђЅ0 , for all рќ‘› в‰¤ рќ‘Ѓ .
   For every variable in every О›рќ‘— , insert the exact smooth dyadic partition

                                           1=        рќњ”рќ‘‹ (рќ‘Ј).
                                                в€‘пёЃ

                                                рќ‘‹

    The partition is exact, so this introduces no error and gives the localized pieces О›рќ‘—,X .
    Insert the localized decomposition for both copies of О› in рќ‘…О› (рќ‘Ѓ ). Expanding the convolutions
gives a finite sum of typed dyadic finite-convolution blocks. The number of such blocks is

                                          рќ‘‚рќђЅ0 ((log рќ‘Ѓ )4рќђЅ0 ).
   The coefficient types and bounds follow directly from the elementary coefficient list and the
smooth dyadic support. This proves Lemma B1.
Remark 5.1 (B1.10. Output). Lemma B1 supplies the exact HeathвЂ“Brown typed dyadic decompo-
sition with fixed sufficiently large рќђЅ0 , polylogarithmically many blocks, and no error term.
    The exact smooth dyadic partition is fixed inside B1. Boundary and tail compatibility for
subsequent routing is checked later by B3, F3, F4, and C1; it is not an additional error in the B1
identity.



                                                  17
B1.11. Logical Dependencies Internal dependencies: PAR.
   External or standard dependencies: X1 and X2.
   Internal nodes served: B3, F3, F4, I1, H4, BGS, E10M, E10X, the CKP branch, the GoodAWACK
branch, and the X16 carrier-slice branch.


6     Part 5. B3: Block classification
Source file: Lemmas/b_3_ltx.md.

6.0.1      B3. Block Classification Lemma
B3.0. Role Logical ID: B3.
    Lemma B3 sits between the exact B1 decomposition and the F3 routing theorem. It does not
estimate sums. Its purpose is to produce a finite and exhaustive preliminary classification of the
typed blocks produced by B1.
    Used by: F3, F4, I1, BGS, E10M, and E10X.
    Uses: B1 and the standard smooth dyadic partition input X2.

B3.1. Statement Let в„¬ be any typed smooth dyadic finite-convolution block produced by
Lemma B1. Then B3 constructs a finite grouping set

                                                  рќ’ў(в„¬)
    with

                                           |рќ’ў(в„¬)| в‰¤ 24рќђЅ0 ,
    and assigns в„¬ to at least one of the preliminary classes

                     TypeI/Edge,       LongAP/Local,          BranchB,     CKP,
    possibly with an additional LocalDiag flag.
    Moreover:

    1. every scale pattern after B1 is represented among the alternatives in рќ’ў(в„¬);

    2. all admissible product groupings are finite and are passed to F3;

    3. TypeI/CKP and CKP/BranchB boundaries are handled as candidate overlaps, not as mutu-
       ally exclusive hard cuts;

    4. every forced local dependence is flagged for LocalDiag;

    5. no residual classes

                        MultiBalancedResidual      or    MixedProductAffineResidual

        remain.




                                                   18
B3.2. Input from B1        By Lemma B1 there is an exact decomposition

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

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

  where each typed block has the form

                      рќ‘…в„¬ (рќ‘Ѓ ) =                              рќђґ(рќ‘Ґ1 , . . . , рќ‘Ґрќ‘џ )рќђµ(рќ‘¦1 , . . . , рќ‘¦рќ‘  ),
                                              в€‘пёЃ

                                     рќ‘Ґ1 В·В·В·рќ‘Ґрќ‘џ +рќ‘¦1 В·В·В·рќ‘¦рќ‘  =рќ‘Ѓ

  with

                                                      рќ‘џ, рќ‘  в‰¤ 2рќђЅ0 ,
  and all variables dyadically localized:

                                            рќ‘Ґрќ‘– в€ј рќ‘‹рќ‘– ,             рќ‘¦рќ‘— в€ј рќ‘Њрќ‘— .
  The elementary coefficient types are inherited from B1:

                                        рќњ‡ В· 1в‰¤рќ‘Ѓ 1/рќђЅ0 ,            1,        log .
  No estimate is made in B3; only structural alternatives are recorded.

B3.3. Scale Vector and Finite Grouping Set                          For every dyadic block define the scale expo-
nents

                                              log рќ‘‹рќ‘–                      log рќ‘Њрќ‘—
                                       рќњ‰рќ‘– =          ,            рќњђрќ‘— =           .
                                              log рќ‘Ѓ                       log рќ‘Ѓ
  Since the products satisfy

                                     рќ‘Ґ1 В· В· В· рќ‘Ґрќ‘џ в‰¤ рќ‘Ѓ,             рќ‘¦1 В· В· В· рќ‘¦рќ‘  в‰¤ рќ‘Ѓ,
  one has
                                рќ‘џ                                  рќ‘ 
                                     рќњ‰рќ‘– в‰¤ 1 + рќ‘њ(1),                     рќњђрќ‘— в‰¤ 1 + рќ‘њ(1).
                               в€‘пёЃ                                 в€‘пёЃ

                               рќ‘–=1                                рќ‘—=1

  Define the finite grouping set

                        рќ’ў(в„¬) = {(рќђј, рќђЅ) : рќђј вЉ† {1, . . . , рќ‘џ}, рќђЅ вЉ† {1, . . . , рќ‘ }}.
  For (рќђј, рќђЅ) в€€ рќ’ў(в„¬), put

                                        рќ‘ўрќђј =                      рќ‘Јрќђј =
                                                в€ЏпёЃ                        в€ЏпёЃ
                                                      рќ‘Ґрќ‘– ,                      рќ‘Ґрќ‘– ,
                                                рќ‘–в€€рќђј                       рќ‘–в€€рќђј
                                                                           /

  and

                                       рќ‘ўвЂІрќђЅ =                      рќ‘ЈрќђЅвЂІ =
                                               в€ЏпёЃ                         в€ЏпёЃ
                                                      рќ‘¦рќ‘— ,                       рќ‘¦рќ‘— .
                                               рќ‘—в€€рќђЅ                        рќ‘— в€€рќђЅ
                                                                            /

  Then every grouping gives



                                                             19
                                             рќ‘ўрќђј рќ‘Јрќђј + рќ‘ўвЂІрќђЅ рќ‘ЈрќђЅвЂІ = рќ‘Ѓ.
      The number of possible groupings is bounded by

                                           |рќ’ў(в„¬)| в‰¤ 2рќ‘џ+рќ‘  в‰¤ 24рќђЅ0 ,
      which is an absolute constant once рќђЅ0 is fixed. This is the finite grouping set supplied to Lemma
F3.

B3.4. Qualitative Scale Predicates             Fix small constants

                                               0<рќњѓв‰Єрќњ‚в‰Є1
      as in PAR.
      A grouped factor рќ‘ў is short if

                                                    рќ‘ў в‰¤ рќ‘Ѓ рќњѓ.
      A grouped factor рќ‘ў is central if

                                          рќ‘Ѓ 1/2в€’рќњ‚ в‰¤ рќ‘ў в‰¤ рќ‘Ѓ 1/2+рќњ‚ .
      A factor is long if it is not short and has enough length for smooth AP/local or WACLE analysis:

                                                    рќ‘ў > рќ‘Ѓ рќњѓ.
      A grouping (рќђј, рќђЅ) is CKP-balanced if

                                 рќ‘ўрќђј в‰Ќ рќ‘Ѓ 1/2+рќ‘‚(рќњ‚) ,          рќ‘ўвЂІрќђЅ в‰Ќ рќ‘Ѓ 1/2+рќ‘‚(рќњ‚) ,
    and both complementary factors рќ‘Јрќђј , рќ‘ЈрќђЅвЂІ are nontrivial long variables or controlled finite-convolution
factors.
    These predicates depend only on dyadic scales, so they are decidable from the scale vector of
the block.

B3.5. Preliminary Candidate Classes B3 assigns every typed block to a finite list of candidate
classes. A block may receive more than one candidate class. Lemma F3 later chooses the actual
route using рќ’ў(в„¬). Thus B3 is responsible for exhaustive candidate generation, not for terminal
uniqueness.

TypeI/Edge Candidate A block is a TypeI/Edge candidate if, for some admissible grouping,
one side has a short grouped factor:

                                         min(рќ‘ўрќђј , рќ‘Јрќђј , рќ‘ўвЂІрќђЅ , рќ‘ЈрќђЅвЂІ ) в‰¤ рќ‘Ѓ рќњѓ ,
   or if the scale vector gives explicit short residual volume after fixing all but one variable.
   Such atoms are not automatically terminal Edge. They are sent to F3/C1, where only the error
part with strict C1 saving is terminal Edge.




                                                       20
LongAP/Local Candidate A block is a LongAP/Local candidate if, after fixing all but one
long variable, the equation reduces to a controlled arithmetic progression or congruence count with
smooth weights and no remaining nonlocal oscillatory arithmetic coefficient.
   The schematic form is

                             рќ‘Ћрќ‘ў + рќ‘Џ в‰Ў рќ‘Ѓ    (mod рќ‘ћ),            рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ ,
   or an equivalent controlled local AP condition. The local main part is passed to D1/H4.

CKP Candidate        A block is a CKP candidate if there exists a grouping such that

                                           рќ‘ўрќ‘Ј + рќ‘ўвЂІ рќ‘Ј вЂІ = рќ‘Ѓ,
   where рќ‘ў, рќ‘ўвЂІ are central or balanced long finite-convolution factors and the coefficient sequences
remain divisor-bounded finite-convolution sequences of B1 type.
   This is the preliminary class later handled by the CKP package.

BranchB Candidate A block is a BranchB candidate if, after all short, local, CKP-balanced,
and collision candidates are removed, the residual structure is central-long affine/WACLE-type
with nonlocal oscillatory finite-convolution coefficients.
    Equivalently, BranchB is the residual non-short, nonlocal, non-CKP, non-diagonal preliminary
class with enough affine structure for GoodAWACK routing in F3/E10.

LocalDiag Flag If any grouping reveals forced equality, proportionality, repeated factor, fixed
gcd-local dependence, or affine dependence among active forms, B3 attaches a LocalDiag flag.
Lemma F3 then treats it as terminal LocalDiag or routes it through the corresponding local branch.

B3.6. Exhaustive Classification Algorithm                For each typed block в„¬:

  1. build its finite grouping set рќ’ў(в„¬);

  2. for each grouping (рќђј, рќђЅ), compute the dyadic scales of

                                           рќ‘ўрќђј ,   рќ‘Јрќђј ,     рќ‘ўвЂІрќђЅ ,   рќ‘ЈрќђЅвЂІ ;

  3. if a short factor or short residual volume is present, add a TypeI/Edge candidate;

  4. if a purely local AP configuration is exposed, add a LongAP/Local candidate;

  5. if a balanced bilinear finite-convolution structure is exposed, add a CKP candidate;

  6. if a forced local dependence or collision is exposed, add a LocalDiag flag;

  7. after all groupings are tested, if no previous candidate exhausts the nonlocal central-long
     part, add a BranchB candidate.

    Thus B3 never stops with an undefined residual. The default residual is not an unclassified
class; it is precisely a BranchB candidate, provided it is non-short, nonlocal, and non-CKP.




                                                  21
B3.7. Exclusion of MultiBalancedResidual              There is no residual class

                                      MultiBalancedResidual.
   A multi-balanced product pattern means that more than one grouping produces central or near-
central factors. B3 does not require uniqueness of the grouping. All such groupings are placed in
the finite set

                                               рќ’ў(в„¬).
    If any grouping produces a CKP-balanced bilinear form, a CKP candidate is added. If several
do, all are recorded as grouping alternatives and passed to the finite grouping-elimination protocol
in F3.
    Thus multi-balancedness is not a residual class. It is a finite multiplicity of CKP/BranchB
grouping alternatives:

                                      MultiBalanced вЉ† рќ’ў(в„¬).
   Since

                                           |рќ’ў(в„¬)| в‰¤ 24рќђЅ0 ,
   this multiplicity is finite and is absorbed by F3.

B3.8. Exclusion of MixedProductAffineResidual                There is no residual class

                                   MixedProductAffineResidual.
   A mixed product-affine residual would be a block that is:

  1. not short/TypeI;

  2. not purely LongAP/Local;

  3. not CKP-balanced under any grouping;

  4. not locally diagonal;

  5. but still contains nonlocal central-long finite-convolution structure.

    By definition B3 assigns exactly such residuals to the BranchB candidate class. This is not
circular: BranchB is the preliminary class designed for non-short, nonlocal, non-CKP central-long
affine/WACLE atoms. Lemmas F3 and F4 then decide whether the atom becomes GoodAWACK,
LocalDiag, CKP, Edge, or LongAP/Local.
    Thus the mixed residual is not unclassified:

                             MixedProductAffineResidual вЉ† BranchB.

B3.9. Boundary Conventions




                                                 22
TypeI and CKP         Suppose a grouping gives

                                             рќ‘ўрќ‘Ј + рќ‘ўвЂІ рќ‘Ј вЂІ = рќ‘Ѓ.
   If one of the grouped factors is short,

                                        min(рќ‘ў, рќ‘Ј, рќ‘ўвЂІ , рќ‘Ј вЂІ ) в‰¤ рќ‘Ѓ рќњѓ ,
    then B3 records a TypeI/Edge candidate. It may also record a CKP candidate for another
grouping if another grouping is balanced. There is no conflict: B3 generates candidates and F3
later routes them.
    If all relevant grouped factors are long and two principal factors are central/balanced, B3 records
a CKP candidate.

CKP and BranchB If some grouping gives a balanced finite-convolution bilinear form compat-
ible with CKP, B3 records a CKP candidate.
    If no grouping gives CKP but the block remains non-short and nonlocal, the block is a BranchB
candidate. Thus

          BranchB = CentralLongNonlocal в€– CKPCompatible в€– LocalDiag в€– TypeI/Edge.
  This definition is preliminary. Lemmas F3 and F4 may later reroute BranchB candidates into
CKP or LocalDiag if divisor/gcd structure becomes visible.

LongAP/Local and BranchB A block is LongAP/Local only if, after fixing auxiliary variables,
the remaining counting problem is purely local and has no nonlocal oscillatory coefficient.
    If an oscillatory coefficient remains, such as a Mobius/Liouville-type finite-convolution factor
in a long affine form, the block is not LongAP/Local. It is a BranchB candidate unless CKP or
LocalDiag applies.
    Thus D1 is not asked to hide nonlocal arithmetic estimates. The terminal LongAP/Local
coefficient-exclusion statement is proved later using this B3 boundary together with the F3/F4
terminal routing alternatives.

B3.10. Proof The number of variables in each B1 block is bounded by 2рќђЅ0 on each side. Therefore
the set of all product groupings is finite and has size at most 24рќђЅ0 . For each grouping, B3 tests
the dyadic scale predicates: short, central, long, local, balanced, and collision. Each test is a finite
condition on the scale vector and algebraic form of the block.
    If a short factor appears, a TypeI/Edge candidate is recorded. If the equation reduces to
controlled local AP counting without nonlocal oscillatory coefficients, a LongAP/Local candidate
is recorded. If a balanced finite-convolution bilinear structure is exposed, a CKP candidate is
recorded. If a forced local dependence is exposed, a LocalDiag flag is recorded. If, after all tests,
a non-short, nonlocal, non-CKP, non-diagonal central-long structure remains, it is by definition a
BranchB candidate.
    Thus every block receives at least one candidate class. Multi-balanced blocks produce several
grouping alternatives inside the finite set рќ’ў(в„¬), and mixed product-affine residuals are precisely
BranchB candidates. Therefore no undefined residual class remains. This proves Lemma B3.
Remark 6.1 (B3.11. Output). Lemma B3 supplies exhaustive preliminary block classification and
a finite grouping set for F3:


                                                    23
                                рќђµ1 =в‡’ рќђµ3 =в‡’ рќђ№ 3 =в‡’ terminal routing.
   All B1 scale patterns are assigned to TypeI/Edge, LongAP/Local, CKP, or BranchB candidates,
with LocalDiag flags when forced dependencies occur. No MultiBalancedResidual or MixedPro-
ductAffineResidual remains.
   The output of B3 is not an analytic estimate. It is the finite candidate generation input used
by F3 to prove terminal routing.

B3.12. Logical Dependencies Internal dependencies: B1.
  External or standard dependencies: X2.
  Internal nodes served: F3, F4, I1, BGS, E10M, and E10X.


7     Part 6. F3P: Intrinsic terminal predicate catalogue
Source file: Lemmas/f3_intrinsic_terminal_predicate_catalogue_ltx.md.

7.0.1    F3P. Intrinsic Terminal Predicate Catalogue
F3P.0. Statement and Role Lemma F3P fixes the terminal predicates used by the F3/F4
routing layer. The predicates are intrinsic: they are stated in terms of the current tagged atom, its
coefficient algebra, its affine/product forms, and its unresolved structural conditions. They do not
use the estimates later proved by C1, D1, G8a, E10L, or H4.
   The output is a finite catalogue

                IsEdge,    IsCKP,        IsGoodAWACK,       IsLocalDiag,   IsLongAPLocal.
    The LongAP/Local predicate is positive. It is not defined as the residual class left after excluding
Edge, CKP, GoodAWACK, and LocalDiag. Instead it requires that all surviving long-variable
coefficients belong to the local coefficient algebra Cloc (рќ‘„рќњЏ ).
    Logical dependencies are B1, B3, C1A predicate names, the F3/F4 atom interface, finite CRT
algebra, and the parameter register. The lemma is used by F3, D1, LPI, H4, and the proof ledger.
    вЂ”

F3P.1. Tagged Atom Data                 A routed atom is a finite tagged object

                                             рќ’њ = (рќ’±, в„’, рќ’ћ, рќ’І, в„›, рќњЏ )
    where:

    1. рќ’± is the finite variable list;

    2. в„’ is the finite list of affine/product forms;

    3. рќ’ћ is the finite list of congruence, divisibility, coprimality, quotient, and local constraints;

    4. рќ’І is the finite coefficient and smooth-weight data;

    5. в„› is the finite unresolved routing set;

    6. рќњЏ is the complete routing tag.

                                                       24
    All complexity constants are bounded in terms of the fixed parameter hierarchy. The tag рќњЏ
records the parent B1 block and every exact refinement already made by B3/F3/F4.
    вЂ”

F3P.2. Local Coefficient Algebra          For a controlled modulus рќ‘„рќњЏ в‰¤ (log рќ‘Ѓ )рќђ¶рќњЏ , define Cloc (рќ‘„рќњЏ )
to be the algebra generated by:

  1. smooth dyadic weights of fixed differentiability complexity;

  2. constants depending only on the tag рќњЏ ;

  3. residue-class indicators 1рќђї(рќ‘§)в‰Ўрќ‘Ћ (mod рќ‘ћ) with рќ‘ћ | рќ‘„рќњЏ ;

  4. coprimality indicators 1(рќђї(рќ‘§),рќ‘ћ)=1 with рќ‘ћ | рќ‘„рќњЏ ;

  5. fixed controlled-divisor factors whose divisor value is part of the tag;

  6. finite products and finite linear combinations of the preceding generators.

    This algebra is local: its values are determined by smooth position data and residue/coprimality
classes modulo рќ‘„рќњЏ . It contains no long-variable arithmetic oscillation.
    The following are explicitly not elements of Cloc (рќ‘„рќњЏ ), unless the relevant expression has already
been fixed into tag data or reduced to residue/coprimality data:
                                                                   (пёѓ       )пёѓ
                                                                    рќ‘рќђї(рќ‘§)
                          рќњ†(рќђї(рќ‘§)),   рќњ‡(рќђї(рќ‘§)),      рќ‘’(рќ›јрќђї(рќ‘§)),      рќ‘’       ,
                                                                      рќ‘ћ
    nonlocal finite-convolution descendants of these functions, nilsequence-type oscillations, unre-
solved ordinary divisor predicates, and unresolved quotient equations.
    вЂ”

F3P.3. Intrinsic Edge Predicate
                                              IsEdge(рќ’њ)
   holds if the tagged atom carries one of the strict saving predicates admitted by C1P/C1A/C1:

  1. smooth boundary or dyadic tail;

  2. large square-divisor tail;

  3. large-gcd or large-content volume saving;

  4. high Fourier tail;

  5. small-conductor layer with a C1 saving certificate;

  6. short residual volume;

  7. Type I short-variable error.

    An ordinary condition рќ‘‘ | рќђї(рќ‘§) is not Edge by itself. It is Edge only if one of the displayed
saving predicates is present.
    вЂ”

                                                  25
F3P.4. Intrinsic CKP Predicate
                                             IsCKP(рќ’њ)
    holds if рќ’њ has a balanced finite-convolution bilinear form reducible, after controlled gcd/content
splitting and smooth dyadic localization, to

                                           рќ‘ўрќ‘¦ + рќ‘ўвЂІ рќ‘¦ вЂІ = рќ‘Ѓрќ‘”
   with non-short grouped variables on both sides, divisor-bounded coefficients, central/balanced
ranges, controlled content, and no forced local diagonal obstruction. The predicate is structural;
the DFI/X10 estimate is not part of the predicate.
   вЂ”

F3P.5. Intrinsic GoodAWACK Predicate

                                          IsGoodAWACK(рќ’њ)

   holds if the tagged atom is a central-long affine WACLE/GoodAWACK atom with:

  1. bounded affine complexity;

  2. smooth weight of polylogarithmic complexity;

  3. no forced local diagonal relation;

  4. no unresolved ordinary divisor or quotient predicate;

  5. at least one marked affine Liouville-type or finite-convolution affine form with controlled
     content;

  6. long fibre directions.

   This is the structural Branch B input class. The cancellation estimate is proved only later by
the GoodAWACK package.
   вЂ”

F3P.6. Intrinsic LocalDiag Predicate

                                           IsLocalDiag(рќ’њ)

    holds if the current tag contains a forced equality, proportionality, repeated form, gcd-local
dependence, or collision between relevant affine/product forms which makes the contribution a
tagged local projection source rather than an oscillatory error term.
    The predicate is positive: it requires an explicit forced relation in рќ’ћ or in the recorded routing
tag. H4 later assembles the local projection; H4 is not used to define the predicate.
    вЂ”




                                                 26
F3P.7. Intrinsic LongAP/Local Predicate

                                         IsLongAPLocal(рќ’њ)

   holds if the tagged atom satisfies all of the following conditions.

  1. The remaining long variable is organized as a long arithmetic progression or a finite union of
     controlled AP fibres, with length at least a fixed power of рќ‘Ѓ in the current B1 scale.

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

  3. Every coefficient which still depends on a long AP variable belongs to Cloc (рќ‘„рќњЏ ).

  4. The remaining constraints are only residue-class, coprimality, fixed controlled-divisor, smooth-
     weight, or endpoint constraints recorded by рќњЏ .

  5. There is no unresolved ordinary divisor predicate, quotient equation, balanced reciprocal-
     phase structure, marked Liouville/Mobius coefficient, nonlocal finite-convolution coefficient,
     Kloosterman phase, or nilsequence oscillation.

   Thus LongAP/Local is a positive local-coefficient condition:

                           IsLongAPLocal(рќ’њ) =в‡’ рќ’Іlong (рќ’њ) вЉ‚ Cloc (рќ‘„рќњЏ ).                       (F3P-L)
   D1 later evaluates such atoms by pure local AP counting and proves LPI-admissibility. D1 is
not used in the definition.
   вЂ”

F3P.8. Mutual Routing Adequacy At the terminal-labelling stage, an atom is tested against
the five predicates in the deterministic F3/F4 routing order. If none of the predicates holds, then
the atom still has a nonempty unresolved obstruction set:

                                             рќ’Є(рќ’њ) Мё= в€….
    Indeed, failure of the LongAP/Local predicate means either the long-variable coefficient is not in
Cloc (рќ‘„рќњЏ ), the modulus is uncontrolled, the AP length is not long, or an unresolved divisor/quotient
or oscillatory structure remains. These are precisely F3/F4 routing obstructions, not downstream
analytic questions.
    Therefore there is no sixth terminal predicate. A nonterminal atom is routed by the F3/F4
measure-decreasing procedure until one of the intrinsic terminal predicates holds.
    вЂ”

F3P.9. Output for D1        For every tagged terminal atom (в„¬, рќњЏ ),

                                        IsLongAPLocal(в„¬, рќњЏ )
   implies that every long-variable coefficient is local:

                                          рќ‘ЋрќњЏ (рќ‘ў) в€€ Cloc (рќ‘„рќњЏ ).
   Equivalently, after expanding the finite local algebra, рќ‘ЋрќњЏ (рќ‘ў) is a finite linear combination of
smooth dyadic weights multiplied by residue-class and coprimality indicators modulo рќ‘„рќњЏ , with tag
constants. This is the only structural input D1 needs before applying smooth AP counting.

                                                  27
8     Part 7. F3: Routing partition
Source file: Lemmas/f_3_ltx.md.

8.0.1    F3. Routing Exhaustion / No-Cycle Theorem
F3.0. Role Logical ID: F3.
    Lemma F3 is the routing-exhaustion theorem for typed B1 blocks after the B3 preliminary
classification. It uses the strengthened measure

                           Mв™Ї (рќ’њ) = (рќђЅfree , рќ‘…largeDiv , рќђ·unabsorbed , рќђ¶coll , рќђµamb )
    which is designed so that ordinary divisor expansion or variable quotienting cannot create a
routing cycle. Generic Cauchy/cube operations and Fourier expansion are not F3 routing opera-
tions; they are proof subroutines in the terminal E10, G8a, D1, and C1 packages.
    The theorem is

             RawBlock =в‡’ Edge вЉ” CKP вЉ” GoodAWACK вЉ” LocalDiag вЉ” LongAP/Local,
    with a genuine no-cycle proof using the strengthened measure

                                                     Mв™Ї .
    Used by: F4, F3A, F3T, BGS, HGO2R, E10L, I1, and the terminal branch assembly.
    Uses: B1, B3, F3P, F4, E5, LPI, and the proof parameter register. The terminal predicates are
structural predicates; the estimates for those terminal classes are proved later by C1, D1, G8a, E10L,
and H4.
    вЂ”

F3.1. Scope of F3        F3 applies to atoms obtained after:

    1. exact B1 typed HeathвЂ“Brown decomposition;

    2. smooth dyadic localization;

    3. preliminary B3 block classification.

    Each atom has a finite description:

                                          рќ’њ = рќ’њ(рќ’±, в„’, рќ’ћ, рќ’І, в„›),
    where:

    вЂў рќ’± is a finite list of variables;

    вЂў в„’ is a finite list of affine/product forms;

    вЂў рќ’ћ is a finite list of congruence/divisibility/coprimality conditions;

    вЂў рќ’І is the smooth dyadic weights and coefficient types;

    вЂў в„› is a finite list of unresolved routing alternatives.


                                                      28
    All complexity constants are bounded in terms of fixed рќђЅ0 .
    All routing steps in F3 are exact refinements of the current summation domain. No analytic
estimate and no рќ‘њ(рќ‘Ѓ ) error is introduced by F3 itself. Error terms appear only after a terminal
atom is sent to a terminal estimate such as C1, D1, G8a, E10L, or H4.
    вЂ”

F3.2. Terminal predicates The intrinsic terminal predicate catalogue is Lemma F3P. It defines
five structural terminal predicates without using the downstream estimates for the corresponding
terminal classes. The present section records the predicates in the shorthand form used by the
routing algorithm.

F3.2.1. Edge terminal predicate
                                             IsEdge(рќ’њ)
   holds if the routing data of рќ’њ contains one of the strict Edge-saving predicates later estimated
by C1:

  1. smooth boundary / dyadic tail;

  2. large square-divisor tail;

  3. large-gcd / large-content volume saving;

  4. high Fourier tail;

  5. small-conductor layer with C1 saving;

  6. short residual volume;

  7. Type I short-variable error.

   Important restriction:

                                              рќ‘‘ | рќђї(рќ‘§)
   alone is not Edge unless it triggers one of the above saving predicates.

F3.2.2. CKP terminal predicate
                                             IsCKP(рќ’њ)
   holds if рќ’њ has balanced finite-convolution bilinear form reducible to

                                          рќ‘ўрќ‘¦ + рќ‘ўвЂІ рќ‘¦ вЂІ = рќ‘Ѓ
   with two non-short grouped variables on each side, divisor-bounded coefficients, smooth dyadic
weights, and no forced local diagonal obstruction. This is a structural input class. The CKP
package later proves the estimate for this class.




                                                29
F3.2.3. GoodAWACK terminal predicate

                                          IsGoodAWACK(рќ’њ)

   holds if рќ’њ is a central-long affine WACLE atom with:

  1. bounded affine complexity;

  2. smooth weight of polylogarithmic complexity;

  3. no forced local diagonal relation;

  4. no unresolved ordinary large divisor condition;

  5. at least one marked affine Liouville-type form with controlled content;

  6. long fibre directions.

    This is a structural input class. The Branch B / GoodAWACK package later proves the estimate
for this class.

F3.2.4. LocalDiag terminal predicate

                                           IsLocalDiag(рќ’њ)

    holds whenever the current atom contains a forced equality, proportionality, gcd-local depen-
dence, or collision between relevant affine/product forms that makes the contribution a canonical
local term rather than an oscillatory error.
    All such atoms are terminal and are passed to H4.

F3.2.5. LongAP/Local terminal predicate

                                            IsLongAP(рќ’њ)

    is the predicate IsLongAPLocal(рќ’њ) from F3P. It holds if the atom is purely local smooth
arithmetic-progression counting with:

  1. smooth weights;

  2. controlled local moduli рќ‘„рќњЏ в‰¤ (log рќ‘Ѓ )рќђ¶рќњЏ ;

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

  4. no unresolved ordinary divisor or quotient predicate;

  5. no unresolved рќњ‡-, рќњ†-, Fourier-, Kloosterman-, reciprocal, finite-convolution, or nilsequence-
     type oscillation;

  6. long AP length.

   This is a structural input class. Lemma D1 later proves that the corresponding main term is
LPI-admissible and hence can be assembled by H4.
   вЂ”

                                                 30
F3.3. Residual obstruction set         For every nonterminal atom define a finite obstruction set

                                                     рќ’Є(рќ’њ)
   consisting of unresolved predicates of the following types:

  1. unresolved ordinary divisor condition;

  2. unresolved quotient equation;

  3. unresolved conductor decision;

  4. unresolved CRT/congruence restriction;

  5. unresolved grouping/balance alternative;

  6. unresolved local collision/dependence decision;

  7. unresolved choice between CKP and GoodAWACK normal form.

   Because the atom is produced from finite B1/B3 data, the set рќ’Є(рќ’њ) is finite and

                                             |рќ’Є(рќ’њ)| в‰ЄрќђЅ0 1.
   вЂ”

F3.4. Finite grouping set        Let

                                                     рќ’ў(рќ’њ)
   be the finite set of admissible unresolved product groupings inherited from the B1 typed block.
   A grouping is a choice of partition of product variables into grouped variables such as

                                       рќ‘ў=                     рќ‘Ј=
                                            в€ЏпёЃ                     в€ЏпёЃ
                                                  рќ‘Ґрќ‘– ,                   рќ‘Ґрќ‘– ,
                                            рќ‘–в€€рќђј                    рќ‘–в€€рќђј
                                                                    /

   and similarly on the second side.
   Since the number of product variables is bounded by 2рќђЅ0 on each side,

                                            |рќ’ў(рќ’њ)| в‰¤ рќђ¶(рќђЅ0 ).
   The regrouping protocol is:

  вЂў if a grouping yields Edge, CKP, GoodAWACK, LongAP/Local, or LocalDiag, the atom be-
    comes terminal;

  вЂў if the grouping is checked and fails all terminal predicates, that grouping is removed from
    рќ’ў(рќ’њ) and is not revisited.

   Thus every unsuccessful regrouping strictly decreases

                                                    |рќ’ў(рќ’њ)|.
   вЂ”

                                                         31
F3.5. Complexity measure           Define the strengthened lexicographic measure

                  Mв™Ї (рќ’њ) = (рќ‘‚unresolved , рќ‘…largeDiv , рќђ·unabsorbed , |рќ’ў(рќ’њ)|, рќђ¶coll , рќђЅfree ),
   where:

                                          рќ‘‚unresolved = |рќ’Є(рќ’њ)|;
    рќ‘…largeDiv counts ordinary large-divisor predicates assigned to F4 processing;
    рќђ·unabsorbed counts unresolved controlled CRT/congruence restrictions;
    |рќ’ў(рќ’њ)| counts unresolved grouping alternatives;
    рќђ¶coll counts unresolved collision/local-dependence decisions;
    рќђЅfree counts remaining free finite-convolution/product variables.
    The order is lexicographic. Therefore increasing рќђЅfree is harmless if some earlier obstruction
component decreases.
    Since all entries are nonnegative integers bounded in terms of рќђЅ0 and the dyadic data, there is
no infinite strictly decreasing sequence.
    вЂ”

F3.6. Allowed routing-level operations             In Lemma F3, only the following are generic routing-
level operations:

  1. controlled CRT absorption;

  2. F4 large-divisor decision;

  3. square-divisor routing;

  4. finite grouping selection/elimination;

  5. terminal LocalDiag detection;

  6. terminal Edge detection by C1 predicates;

  7. terminal class labelling into CKP, GoodAWACK, LongAP/Local, Edge, LocalDiag.

   The following are not generic F3 routing operations:

                                Cauchy/cube,           Fourier expansion.
   They are post-terminal proof subroutines:

          GoodAWACK в†’ рќђё10,              CKP в†’ рќђє8рќ‘Ћ,            LongAP в†’ рќђ·1,             Edge в†’ рќђ¶1.
   вЂ”




                                                     32
F3.7. Controlled CRT Absorption           Suppose рќ’њ contains a controlled congruence

                              рќђї(рќ‘§) в‰Ў рќ‘Ћ   (mod рќ‘ћ),        рќ‘ћ в‰¤ (log рќ‘Ѓ )рќђ¶ .
   If the congruence is incompatible, the atom is empty and hence Edge-zero.
   If compatible, replace the lattice coset О› by the subcoset

                                О›вЂІ = {рќ‘§ в€€ О› : рќђї(рќ‘§) в‰Ў рќ‘Ћ     (mod рќ‘ћ)}.
   Then one unresolved congruence is removed:

                                рќђ·unabsorbed (рќ’њвЂІ ) < рќђ·unabsorbed (рќ’њ),
    and no earlier component of Mв™Ї increases. Content may increase by at most a polylogarithmic
factor, which is allowed by E5.
    Therefore

                                         Mв™Ї (рќ’њвЂІ ) < Mв™Ї (рќ’њ).
   If рќ‘ћ is not controlled, CRT absorption is not allowed as a generic F3 step. Such a case must be
routed through C1, F4, CKP, or LocalDiag depending on the source of the large modulus.
   вЂ”

F3.8. F4 Large-Divisor Decision        Suppose рќ’њ contains an unresolved ordinary divisor condition

                                             рќ‘‘ | рќђї(рќ‘§).
   F3 does not expand it blindly. It invokes F4 as a decision procedure.
   F4 has the following exhaustive output:

  1. if the divisor condition gives a strict C1 saving, route to Edge;

  2. if it creates balanced multiplicative structure, route to CKP;

  3. if it creates forced local dependence, route to LocalDiag;

  4. otherwise, after fixed quotienting/content stabilization, route to GoodAWACK.

  Thus either the atom is terminal, or the unresolved large-divisor predicate is removed from
рќ’Є(рќ’њ). In the nonterminal case:

                                 рќ‘‚unresolved (рќ’њвЂІ ) < рќ‘‚unresolved (рќ’њ)
   or at least

                                   рќ‘…largeDiv (рќ’њвЂІ ) < рќ‘…largeDiv (рќ’њ)
    with no earlier increase.
    The operation may introduce quotient variables and therefore may increase рќђЅfree , but this is
irrelevant because рќђЅfree is the last component of Mв™Ї .
    Therefore every nonterminal F4 decision strictly decreases Mв™Ї .
    вЂ”


                                                 33
F3.9. Square-Divisor Routing          If the obstruction is square-divisor type

                                              рќ‘‘2 | рќђї(рќ‘§),
   then either:

  1. рќ‘‘ > рќђ·, in which case C1 square-divisor Edge applies;

  2. рќ‘‘ в‰¤ рќђ·, in which case the condition is a controlled CRT/divisibility restriction and can be
     absorbed.

    In case 1 the atom is terminal Edge. In case 2 controlled absorption removes an unresolved
divisibility predicate, so Mв™Ї decreases.
    Thus square-divisor routing is terminal or decreasing.
    вЂ”

F3.10. Finite Grouping Selection/Elimination               Suppose the atom is not terminal but has
unresolved grouping alternatives

                                             рќ’ў(рќ’њ) Мё= в€….
   Choose one grouping рќђє в€€ рќ’ў(рќ’њ).
   After applying this grouping, exactly one of the following happens:

  1. terminal Edge predicate holds;

  2. terminal CKP predicate holds;

  3. terminal GoodAWACK predicate holds;

  4. terminal LongAP/Local predicate holds;

  5. terminal LocalDiag predicate holds;

  6. no terminal predicate holds.

   In cases 1вЂ“5, routing terminates.
   In case 6, remove рќђє from the unresolved grouping set:

                                        рќ’ў(рќ’њвЂІ ) = рќ’ў(рќ’њ) в€– {рќђє}.
   Thus

                                        |рќ’ў(рќ’њвЂІ )| = |рќ’ў(рќ’њ)| в€’ 1.
   No earlier obstruction component increases: the failed grouping is recorded as eliminated, not
converted into a new obstruction. Therefore

                                         Mв™Ї (рќ’њвЂІ ) < Mв™Ї (рќ’њ).
   вЂ”




                                                 34
F3.11. LocalDiag Detection If any forced equality, proportionality, gcd-local dependence, or
unavoidable collision is detected, then

                                           IsLocalDiag(рќ’њ)
   holds and рќ’њ is terminal.
   F3 does not perform indefinite partial diagonal extraction. LocalDiag detection is terminal.
   This avoids cycles of the form:

             partial collision extraction в†’ new collision в†’ partial extraction again.
   вЂ”

F3.12. Edge Detection       If any strict C1 Edge predicate holds, then

                                             IsEdge(рќ’њ)
   and the atom is terminal.
   F3 uses C1 only as a terminal detector. It does not label ordinary divisor conditions as Edge
unless a C1 saving predicate is explicitly satisfied.
   вЂ”

F3.13. Terminal Class Labelling If none of the unresolved obstruction operations applies and
no grouping alternative remains, then the atom has no unresolved divisor, congruence, grouping,
collision, conductor, or balance decision.
    Then B3 structural classification plus the terminal predicates imply exactly one of:


       IsEdge(рќ’њ),     IsCKP(рќ’њ),    IsGoodAWACK(рќ’њ),          IsLocalDiag(рќ’њ),   IsLongAP(рќ’њ).

   The only possible residual alternative would be a MixedResidual atom: not Edge, not CKP,
not GoodAWACK, not LocalDiag, not LongAP/Local.
   But such a MixedResidual atom would necessarily contain at least one unresolved item:

  вЂў unresolved ordinary divisor;

  вЂў unresolved quotient equation;

  вЂў unresolved grouping alternative;

  вЂў unresolved conductor decision;

  вЂў unresolved local collision decision;

  вЂў unresolved choice between multiplicative balanced and affine WACLE form.

   This contradicts

                                    рќ’Є(рќ’њ) = в€…,        рќ’ў(рќ’њ) = в€….
   Therefore no MixedResidual terminal class exists.



                                                35
Decidability at termination       At the terminal-labelling stage there is no circular call back into
F4. Indeed, when

                                     рќ’Є(рќ’њ) = в€…,          рќ’ў(рќ’њ) = в€…,
    all conditions appearing in F3.2.2вЂ“F3.2.3 are decidable from the finite atom data.
    The phrase "no unresolved ordinary large divisor condition" in IsGoodAWACK means exactly
that the large-divisor component of рќ’Є(рќ’њ) is zero. If such a condition were still present, F3.8 would
call F4 before terminal labelling.
    The phrase "no forced local diagonal obstruction" in IsCKP and IsGoodAWACK means that
the collision/local dependence component of рќ’Є(рќ’њ) is zero. If a forced equality, proportionality,
gcd-local dependence, or conductor collapse were present, F3.11 would have already labelled the
atom LocalDiag or sent it to the appropriate F4/C1 branch.
    The remaining decisions are dyadic scale comparisons, coefficient type labels, and whether the
B3 grouping is multiplicative-balanced or affine-WACLE. These are read from the finite B1/B3
atom description and require no further routing operation. Hence the terminal predicates are
genuine predicates at termination, not requests for another pass through F4.
    вЂ”

F3.14. Theorem F3вЂ™

Theorem 8.1 (Theorem F3вЂ™). Let рќ’њ be any atom produced by B1 typed decomposition and B3
preliminary classification. Then after finitely many F3 routing steps, рќ’њ is written as a finite
disjoint sum of terminal atoms belonging to

             Edge,     CKP,       GoodAWACK,             LocalDiag,    LongAP/Local.
   No other terminal class occurs.

Proof. If рќ’њ is already terminal, there is nothing to prove.
   Otherwise рќ’њ has at least one unresolved obstruction or grouping alternative:

                                     рќ’Є(рќ’њ) Мё= в€…   or     рќ’ў(рќ’њ) Мё= в€….
   Apply the appropriate routing operation:

  вЂў controlled CRT absorption for controlled congruences;

  вЂў F4 decision for ordinary large divisors;

  вЂў square-divisor routing for square-divisor obstructions;

  вЂў finite grouping selection/elimination for unresolved groupings;

  вЂў terminal LocalDiag detection for forced dependence;

  вЂў terminal Edge detection for strict C1-saving predicates.

   By Sections F3.7вЂ“F3.12, every nonterminal operation strictly decreases

                                                 Mв™Ї .



                                                 36
    Since Mв™Ї takes values in N6 with lexicographic order, no infinite strictly decreasing sequence
exists. Hence the routing process terminates after finitely many steps.
    At termination, no unresolved obstruction and no unresolved grouping alternative remains. By
Section F3.13, the terminal atom must be one of

                       Edge, CKP, GoodAWACK, LocalDiag, LongAP/Local.
   Thus terminal exhaustion holds and no sixth terminal class exists. The theorem is proved.
   Lemma F3T expands this theorem into a finite row-by-row routing table indexed by B1 block
type, B3 grouping type, dyadic regime, divisor/conductor regime, coefficient type, terminal class,
and exclusion reason. Lemma F3T is a tabular restatement of the F3.6вЂ“F3.14 routing mechanism,
not an additional routing operation.
   вЂ”


F3.15. Partition Identity For every typed B1 block в„¬, B3/F3/F4 routing produces a finite
family of tagged terminal atoms

                                            {(в„¬, рќњЏ )}рќњЏ в€€рќ’Ї (в„¬)
   such that the exact identity

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

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

   holds before any terminal estimates are applied.

Proof. The routing process is an iterated finite partition of the summation domain. B3 first parti-
tions a typed B1 block into finitely many grouping/candidate cells. Each subsequent F3/F4 step
is one of the following exact operations:

  1. terminal labelling of the current cell;

  2. controlled CRT restriction, using the exact union over residue classes;

  3. divisibility or square-divisibility splitting, using identities such as 1 = 1рќ‘‘|рќђї + 1рќ‘‘в€¤рќђї ;

  4. F4 quotient/divisor decision, where every branch carries the inherited routing tag;

  5. finite grouping selection/elimination, which partitions the finite set of available grouping
     alternatives;

  6. LocalDiag, Edge, CKP, GoodAWACK, or LongAP terminal detection.

    No step discards mass. When a branch is later proved negligible, that estimate is made by the
corresponding terminal package, not by F3. Since F3.14 proves finite termination by the strictly
decreasing measure Mв™Ї , the iterated finite partition reaches terminal cells after finitely many steps.
The tag рќњЏ records the complete splitting history, so distinct terminal tags correspond to disjoint
cells of the parent B1 block. Summing the terminal cell contributions gives (F3-partition). Lemma
proved.
    вЂ”


                                                   37
F3.16. Output to Terminal Packages Lemma F3 does not prove terminal estimates. It only
routes terminal atoms to the correct packages:

                                           Edge в†’ рќђ¶1,


                                           CKP в†’ рќђє8рќ‘Ћ,


                                      GoodAWACK в†’ рќђё10,


                                    LongAP/Local в†’ рќђ·1/рќђ»4,


                                         LocalDiag в†’ рќђ»4.
   The proof-subroutines are external to F3:

  вЂў Fourier expansion is used inside G2a, D1, C1;

  вЂў Cauchy/cube/Gowers machinery is used inside E10;

  вЂў local projection algebra is used inside H4.

   This separation is part of the no-cycle proof.
   вЂ”

F3.17. Consequence for the Proof Tree

               F3 proves routing exhaustion using the strengthened measure Mв™Ї .

    Generic Cauchy/cube operations and Fourier expansion are not F3 routing operations. They
are treated inside the terminal packages. F4 remains the large-divisor decision subroutine used by
F3.
    вЂ”

F3.18. Dependency Check          The no-cycle routing proof uses the following supporting state-
ments:

  1. B3 preliminary classification gives a finite set of admissible grouping alternatives.

  2. F4 large-divisor decision is exhaustive.

  3. the structural Edge predicates are strict terminal tags for genuine saving mechanisms;

  4. the structural predicates CKP, GoodAWACK, LongAP/Local, and LocalDiag are mutually
     adequate to classify atoms with no unresolved obstruction.

   Thus F3 is a routing theorem. It labels terminal branches but does not use the later estimates
that discharge those branches.
   Lemma F3T is the finite table associated with this theorem. It is a child of F3, not a new
hypothesis for F3.

                                                  38
F3.19. Logical Dependencies Internal dependencies: B1, B3, F4, E5, LPI, and the proof
parameter register.
   Internal nodes served: F4, F3A, F3T, BGS, HGO2R, E10L, I1, and the terminal branch assembly.


9     Part 8. F3A: Routing interface completeness
Source file: Lemmas/f3_routing_interface_completeness_ltx.md.

9.0.1    F3A. Completeness of the F3.6 Routing Interface
F3A.0. Role Logical ID: F3A.
   This verification addresses the routing-interface condition needed in the Branch B / GoodAWACK
source check:

             E10M depends on F3.6 being the exhaustive list of F3 routing operations.
   The verification does not introduce a new routing procedure. It records the exact contract later
used by E10Y/E10M/E10X/E10K/E10L:


 every actual terminal GoodAWACK skeleton is generated by B1/B3 data, F3.6 routing operations, F4 decisions,
                                                                                  (F3-COMPLETE)
     Here "actual" has the same non-circular meaning as in E10Y: the object lies in the image of the
independently defined B1/B3/F3/F4 construction. The word does not mean "accepted by E10Y."
     The F3.6 list includes square-divisor routing, matching the square-divisor step used in the F3
decrease check and routing theorem.
     Lemma F3T gives the associated finite routing table. F3T does not add a new operation to the
list below; it expands the same operation list by B1 block type, B3 grouping type, dyadic regime,
divisor/conductor regime, coefficient type, terminal class, and exclusion reason.
     Used by: E10Y, E10M, E10K, E10L, and E10X.
     Uses: B1, B3, F3, F3T, F4, and E5. The E10 lemmas consume this interface; they are not
prerequisites for it.
     вЂ”

F3A.1. Complete F3.6 Operation List             The generic F3 routing-level operations are exactly:

    1. controlled CRT absorption;

    2. F4 large-divisor decision;

    3. square-divisor routing;

    4. finite grouping selection/elimination;

    5. terminal LocalDiag detection;

    6. terminal Edge detection by C1 predicates;

    7. terminal class labelling into CKP, GoodAWACK, LongAP/Local, Edge, or LocalDiag.

    The explicitly excluded operations are:

                                                  39
  1. Cauchy/cube operations;

  2. Fourier expansion;

  3. primitive analytic slicing after the terminal tensor-verification skeleton is fixed.

   Those excluded operations may occur inside post-terminal estimates, but they do not generate
new terminal GoodAWACK skeletons.
   вЂ”

F3A.2. Occurrence Map

   Interface location              Operation class                         Post-terminal interpretation
   Lemma F3, F3.7                  controlled CRT absorption               Full-rank finite-index restriction or
                                                                           impossible fibre; content controlled
                                                                           by E5.
   Lemma F3, F3.8                  F4 large-divisor decision               Delegates ordinary large-divisor and
                                                                           quotient cases to F4; output is Edge,
                                                                           CKP, LocalDiag, GoodAWACK with
                                                                           tags, or a decreasing continuation.
   Lemma F3, F3.9                  square-divisor routing                  Large square divisors are C1 Edge;
                                                                           small square divisors are controlled
                                                                           divisibility/CRT restrictions.
   Lemma F3, F3.10                 finite grouping selection/elimination   Selects among B3 finite product
                                                                           groupings; failed groupings are re-
                                                                           moved and not converted into new
                                                                           affine operations.
   Lemma F3, F3.11                 LocalDiag detection                     Terminal detection; the atom leaves
                                                                           GoodAWACK.
   Lemma F3, F3.12                 Edge detection                          Terminal C1 detection; the atom
                                                                           leaves GoodAWACK.
   Lemma F3, F3.13                 terminal class labelling                Labelling only; no coordinate opera-
                                                                           tion is performed.
   Lemma F3, F3.14                 routing theorem                         Uses exactly the operations above to
                                                                           prove termination and terminal ex-
                                                                           haustion.




    This table is the interface used by E10M. In particular, any rank drop in an actual terminal
GoodAWACK record must come from F4 quotient/divisor data, LocalDiag/Edge/CKP tags, con-
trolled CRT/divisibility data, or post-terminal analytic slicing after terminality. None of these is
an untagged free affine regrouping.
    вЂ”

F3A.3. Exhaustiveness Theorem for the F3 Interface Let рќ’њ be a nonterminal atom
produced by B1 and B3. By F3.3 and F3.4, any reason why рќ’њ is not terminal belongs to:

  1. an unresolved ordinary divisor or quotient condition;

  2. an unresolved conductor/CRT/congruence restriction;

  3. an unresolved square-divisor obstruction;

  4. an unresolved product grouping or balance alternative;

  5. an unresolved local collision or dependence decision;

                                                     40
  6. an unresolved choice between CKP and GoodAWACK normal form.

   The F3.6 list covers these cases as follows.

      Nonterminal reason                               Covered by
      ordinary divisor or quotient condition           F4 large-divisor decision
      conductor/CRT/congruence restriction             controlled         CRT         absorption,   or
                                                       F4/C1/CKP/LocalDiag if uncontrolled
      square-divisor obstruction                       square-divisor routing
      grouping or balance alternative                  finite grouping selection/elimination
      local collision or dependence                    terminal LocalDiag detection
      strict saving predicate                          terminal Edge detection
      no unresolved obstruction remains                terminal class labelling




   Therefore an atom with no applicable F3.6 operation has no unresolved obstruction and no
unresolved grouping alternative. F3.13 then forces one of the five terminal classes. This is exactly
the terminal exhaustion theorem F3.14.
   The same implication is tabulated in Lemma F3T.

Proof of interface completeness. Let рќ’њ be an actual nonterminal atom after B1/B3. By Lemma
F3.3, every unresolved reason preventing terminal classification belongs to the finite obstruction
set рќ’Є(рќ’њ), whose labels are:

  1. ordinary divisor;

  2. quotient;

  3. conductor;

  4. CRT/congruence;

  5. grouping/balance;

  6. local collision;

  7. CKP/GoodAWACK choice.

   By Lemma F3.4 every unresolved product regrouping belongs to the finite grouping set рќ’ў(рќ’њ).
The F3.6 operations act on exactly these two finite sources of nonterminality:

  1. controlled CRT absorption acts on the CRT/congruence part of рќ’Є(рќ’њ);

  2. F4 large-divisor decision acts on ordinary divisor, quotient and conductor entries of рќ’Є(рќ’њ);

  3. square-divisor routing acts on square-divisor obstructions;

  4. finite grouping selection/elimination acts on рќ’ў(рќ’њ);

  5. LocalDiag detection acts on forced local collision or dependence entries;

  6. Edge detection acts on strict C1-saving predicates;

  7. terminal class labelling applies when both рќ’Є(рќ’њ) and рќ’ў(рќ’њ) are empty.

                                                  41
   No other nonterminal datum is present in the F3 atom description of Lemma F3.1. Thus any
proposed additional F3 routing operation would have to act on a datum outside рќ’Є(рќ’њ) в€Є рќ’ў(рќ’њ), or
on a datum already covered by one of the seven cases above. The first possibility is not an actual
B1/B3/F3 atom; the second is not a new operation. Hence the F3.6 list is complete for actual F3
routing.
   вЂ”


F3A.4. Consequence for E10Y/E10X/E10K E10Y may cite F3.6 as the routing-level part
of the skeleton-generating grammar. E10M, E10X, and E10K may then use E10Y as the formal
completeness input. Under the operation list above:

  1. square-divisor routing is explicit and therefore no longer a hidden F3 operation;

  2. Cauchy/cube/Fourier/slicing operations are post-terminal estimates, not terminal-skeleton
     generators;

  3. arbitrary untagged rank-dropping affine regrouping is not an allowed routing operation.

     Thus:


         F3A + E10Y + E10M =в‡’ the F3-complete routing premise used by E10K is explicit.

     вЂ”

F3A.5. Stability Rule Any change to F3 that adds, renames, or reinterprets a routing-level
operation must update this verification, E10Y, E10M.3, and E10K. Without that check, the F3-
complete routing premise is not valid for the changed routing interface.

F3A.6. Logical Dependencies Internal dependencies: B1, B3, F3, F3T, F4, and E5.
  Internal nodes served: E10Y, E10M, E10K, E10L, and E10X.


10       Part 9. F3T: Complete routing exhaustion
Source file: Lemmas/f3_complete_routing_exhaustion_ltx.md.

10.0.1       F3T. Finite Routing Table for B1-Origin Atoms
F3T.0. Role Logical ID: F3T.
    Lemma F3T is the tabular routing lemma associated with Lemmas B1, B3, F3P, F3, F4, E5,
and the LPI terminal-class interface. It does not introduce a new routing operation. It records
the finite case distinction which is implicit in F3.6вЂ“F3.15 and makes explicit where every B1-origin
atom goes.
    Associated with F3; used by F3A, E10M, E10K, E10L, I1, and the manuscript routing appendix.
    Uses: B1, B3, the intrinsic predicate catalogue F3P, the F3 routing definitions F3.1вЂ“F3.15, F4,
E5, LPI, and the proof parameter register. The branch theorems C1, D1, G8a, E10L, and H4 estimate
or assemble the terminal classes after F3T has labelled them.
    The purpose is to prove the following interface statement.

                                                42
 For fixed рќђЅ0 , every B1-origin atom is routed into exactly one of Edge, CKP, GoodAWACK, LocalDiag, or LongA
                                                                                          (F3T)
    The word "exactly" refers to the tagged partition produced by Lemma F3. If a cell satisfies
more than one terminal predicate, the routing tag records the first applicable terminal class in
the deterministic order stated in F3T.2; the other predicates are retained only as supplementary
verification information and do not create additional terminal atoms.
    вЂ”

F3T.1. Finite input data Fix рќђЅ0 . A B1 block consists of two HeathвЂ“Brown finite-convolution
sides. Each side has 2рќ‘— variables with 1 в‰¤ рќ‘— в‰¤ рќђЅ0 , hence the total number of elementary variables
is at most 4рќђЅ0 . After the exact dyadic partition, each elementary coefficient is of type

                                      рќњ‡ В· 1в‰¤рќ‘¦ ,      1,    log .
   Thus a B1 block has only the following finite structural data:

  1. the two finite lists of elementary variables;

  2. their coefficient types;

  3. their dyadic scales;

  4. the Goldbach equation relating the two sides;

  5. the finite set of admissible product groupings generated by B3.

   B3 supplies the finite grouping set

                                      рќ’ў(в„¬),       |рќ’ў(в„¬)| в‰¤ 24рќђЅ0 ,
   and the preliminary candidate labels TypeI/Edge, LongAP/Local, CKP, BranchB, and Local-
Diag. Candidate labels may overlap at this stage; uniqueness is produced only after the F3 tagged
routing partition.
   вЂ”

F3T.2. Canonical tagged routing order             The F3 routing table is read in the following deter-
ministic order on each current tagged cell.

  1. Empty or incompatible cells are discarded as zero Edge cells.

  2. Strict C1 saving predicates are routed to Edge.

  3. Forced equality, proportionality, repeated factors, or local dependence is routed to LocalDiag.

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

  5. Square-divisor obstructions are processed by the square-divisor routing of F3.

  6. Controlled CRT/congruence restrictions are absorbed if they are full-rank and controlled by
     E5; otherwise they are routed through F4, C1, CKP, or LocalDiag according to the source of
     the restriction.

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

     8. A cell with no unresolved obstruction and no unresolved grouping alternative is terminally
        labelled as CKP, GoodAWACK, LongAP/Local, Edge, or LocalDiag by the intrinsic F3P
        terminal predicates as implemented by F3.

   Each nonterminal application is one of the allowed F3.6 operations and strictly decreases the
F3 measure Mв™Ї . Therefore the table cannot be read indefinitely.
   вЂ”

F3T.3. Complete finite routing table                 The table below uses the following abbreviations:

     вЂў B1 type records the relevant finite-convolution source;

     вЂў B3 grouping is the preliminary grouping/candidate pattern;

     вЂў Regime is the dyadic or structural condition visible on the current tagged cell;

     вЂў Divisor/conductor state records whether F4, square-divisor routing, or controlled CRT
       absorption is needed;

     вЂў Coefficient type records the surviving arithmetic coefficient shape;

     вЂў Terminal class is the class assigned by the canonical routing order;

     вЂў Exclusion reason explains why the other terminal classes do not receive the same tagged
       cell.

 Row           B1     block   B3 grouping    Dyadic/structural
                                                            Divisor/conductor
                                                                           Remaining          Routed ter-   Reason          Structural
               type           type           regime         state          coefficient        minal class   other termi-    source
                                                                           type                             nal classes
                                                                                                            are excluded
 1             Any typed      Any group-     Empty            Inconsistent    None            Edge-zero     The        cell F3
               B1 block       ing            support          CRT/divisibility                              has       zero
                                             or    incom-     constraints                                   mass, so no
                                             patible                                                        analytic ter-
                                             congruences                                                    minal class
                                                                                                            is created.
 2             Any typed      TypeI/Edge     Boundary         The      strict   Divisor-      Edge                          F3,
                                                                                                            CKP/GoodAWACK/LongAP    C1A-
               B1 block       or       any   tail,   short    Edge predi-       bounded                     require         interface
                              grouping       residual vol-    cate E1вЂ“E7        finite-                     a        non-
                                             ume, large       is      struc-    convolution                 negligible
                                             square-          turally           coefficient                 central     or
                                             divisor          present                                       long     local
                                             tail,   large                                                  cell;      Lo-
                                             gcd/content                                                    calDiag
                                             layer, high                                                    requires
                                             Fourier                                                        forced local
                                             tail, small-                                                   dependence.
                                             conductor
                                             layer,     or
                                             Type I sav-
                                             ing




                                                         44
3   Any typed   LocalDiag      Forced            Any associ-     Local            LocalDiag    Edge        re- F3, F4, LPI
    B1 block    flag from B3   equality,         ated divisor    congruence-                   quires        a
                or later F4    propor-           relation  is    only data                     strict saving
                cell           tionality,        part of the                                   predicate;
                               repeated          local depen-                                  CKP/GoodAWACK
                               factor, fixed     dence tag                                     require non-
                               local depen-                                                    diagonal
                               dence,      or                                                  indepen-
                               one     active                                                  dent      vari-
                               form deter-                                                     ables; Lon-
                               mined       by                                                  gAP/Local
                               another                                                         requires
                                                                                               a         one-
                                                                                               dimensional
                                                                                               AP/local
                                                                                               cell   rather
                                                                                               than          a
                                                                                               diagonal
                                                                                               relation.
4   Any typed   LongAP/Local After fixing        No       un-    Local     AP     LongAP/Local A surviving     B3, F3P, F3,
    B1 block    candidate    auxiliary           resolved        weight                        nonlocal        LPI
                             variables,          ordinary        whose long-                   oscillatory
                             one       long      divisor   or    variable co-                  factor pre-
                             AP variable         uncontrolled    efficients lie                vents F3P-
                             remains             conductor       in Cloc (рќ‘„рќњЏ )                 LongAP/Local
                             and        the      remains         and with no                   and routes
                             F3P      local                      surviving                     to CKP or
                             coefficient                         nonlocal рќњ‡-,                  GoodAWACK;
                             predicate                           рќњ†-, Fourier-,                 short/boundary
                             holds                               Kloosterman-                  loss routes
                                                                 ,          or                 to       Edge;
                                                                 nilsequence-                  forced     de-
                                                                 type oscilla-                 pendence
                                                                 tion                          routes       to
                                                                                               LocalDiag.
5   Any typed   CKP-           Two      long     No     small-   Arbitrary        CKP          Edge exclu-     B3, F3
    B1 block    balanced       grouped           conductor,      divisor-                      sions     have
                grouping       variables on      large-рќ‘”,        bounded                       already been
                               each side are     high-           finite-                       removed
                               central and       frequency,      convolution                   structurally;
                               balanced          boundary, or    coefficients                  LocalDiag
                                                 LocalDiag       allowed by                    was tested
                                                 obstruction     the      CKP                  earlier;
                                                 remains         structural                    GoodAWACK
                                                                 predicate                     is excluded
                                                                                               by balanced
                                                                                               bilinear
                                                                                               CKP struc-
                                                                                               ture;     Lon-
                                                                                               gAP/Local
                                                                                               is excluded
                                                                                               by two-sided
                                                                                               bilinear
                                                                                               shape.




                                            45
6    BranchB         Non-short,      No ordinary       Controlled       Bounded        GoodAWACK Edge, Local-     F3, E5
     candidate       nonlocal,       large-divisor     content and      affine/finite-           Diag, CKP,
                     non-CKP         predicate is      controlled       convolution              and       Lon-
                     central-long    unresolved;       CRT data         coefficient              gAP/Local
                     affine group-   no      local                      with      con-           have         all
                     ing             dependence;                        trolled                  failed       by
                                     no      CKP                        content                  the previous
                                     balance                                                     rows;       the
                                                                                                 cell is passed
                                                                                                 to          the
                                                                                                 GoodAWACK
                                                                                                 finite-
                                                                                                 grammar
                                                                                                 package for
                                                                                                 the      rank-
                                                                                                 dropping
                                                                                                 AFF        clo-
                                                                                                 sure.
7    Any typed       Any      B3     Divisor    or     F4 Case I:       Divisor-       Edge      F4        sup-   F4
     B1     block    grouping        quotient          short divi-      bounded                  plies       the
     with    ordi-                   condition         sor,    short    finite-                  structural
     nary divisor                    рќ‘‘ | рќђї or          quotient,        convolution              Edge tag; no
     predicate                       рќђї    =    рќ‘‘рќ‘       or    explicit   coefficient              central ter-
                                     remains           saving pred-                              minal class
                                     unresolved        icate                                     is entered.
8    Any typed       Any      B3     Divisor    or     F4 Case II:      Local          LocalDiag The divisor      F4, LPI
     B1     block    grouping        quotient          quotienting      congru-                  relation
     with    ordi-                   condition         forces local     ence/diagonal            identi-
     nary divisor                    remains           dependence       data                     fies     active
     predicate                       unresolved                                                  forms,       so
                                                                                                 independent
                                                                                                 CKP/GoodAWACK
                                                                                                 variables are
                                                                                                 absent.
9    Any typed       CKP-            Divisor and       F4 Case III:     Divisor-       CKP       Short/local      F4
     B1     block    compatible      quotient          balanced         bounded                  cases were
     with    ordi-   after quoti-    variables         multiplica-      bilinear co-             removed
     nary divisor    enting          remain long       tive divisor     efficient                by           F4
     predicate                       and       bal-    structure                                 Cases IвЂ“II;
                                     anced                                                       GoodAWACK
                                                                                                 is excluded
                                                                                                 by balanced
                                                                                                 bilinear
                                                                                                 structure.
10   BranchB or      Non-short,      Central-          F4 Case IV:      Controlled     GoodAWACK F4         has   F4, E5
     affine resid-   nonlocal,       long affine       quotient tag     affine finite-           already
     ual after F4    non-CKP         residual          recorded;        convolution              excluded
                     after quoti-    with     con-     no untagged      coefficient              Edge, Local-
                     enting          trolled quo-      variable                                  Diag,      and
                                     tient/content     divisor sur-                              CKP; Lon-
                                                       vives                                     gAP/Local
                                                                                                 is      absent
                                                                                                 because the
                                                                                                 residual      is
                                                                                                 not a one-
                                                                                                 dimensional
                                                                                                 local      AP
                                                                                                 cell.
11   Any typed       Any group-      Large square      Square-          Divisor-       Edge      The struc-       F3
     B1 block        ing             divisor рќ‘‘2 |      divisor tail     bounded                  tural square-
                                     рќђї with рќ‘‘ >                         finite-                  divisor Edge
                                     рќђ·                                  convolution              predicate
                                                                        coefficient              applies.




                                                  46
 12               Any typed         Any group-      Small square       Controlled    Same coef-       Nonterminal   No     termi-      F3, E5
                  B1 block          ing             divisor      or    full-rank     ficient type     decrease      nal      class
                                                    controlled         divisibil-    with polylog                   is assigned
                                                    divisibility       ity/CRT       content loss                   yet;       the
                                                    condition          absorption                                   unresolved
                                                                                                                    divisor com-
                                                                                                                    ponent       is
                                                                                                                    removed and
                                                                                                                    F3 continues
                                                                                                                    with smaller
                                                                                                                    Mв™Ї .
 13               Any typed         Any group-      Controlled      Full-rank        Same       co-   Nonterminal   The cell re-       F3, E5
                  B1 block          ing             CRT/congruencefinite-index       efficient        decrease      mains in the
                                                    restriction     restriction      type      with                 routing pro-
                                                    with      full-                  controlled                     cess; if the
                                                    rank lattice                     content                        restriction is
                                                    image                                                           incompati-
                                                                                                                    ble Row 1
                                                                                                                    applies.
 14               Any typed         Any       un-   Candidate     No new divi-  Same coeffi-          Nonterminal   The selected       B3, F3
                  B1 block          resolved        overlap, e.g. sor/conductor cient type            decrease or   grouping ei-
                                    grouping        TypeI/CKP     operation                           one of Rows   ther triggers
                                    alternative     or                                                2вЂ“6           a terminal
                                                    CKP/BranchB                                                     row or is
                                                                                                                    eliminated
                                                                                                                    from       the
                                                                                                                    finite     B3
                                                                                                                    grouping
                                                                                                                    set.




   Rows 12вЂ“14 are not terminal rows. They are included because they are the only nonterminal
operations that can occur before a terminal row is reached. In each case Lemma F3 proves strict
decrease of Mв™Ї .
   вЂ”

F3T.4. Residual Exclusion Table The table F3T.3 is the formal routing table. The following
refinement records the same exhaustion in the order in which an external reader can check a putative
mixed residual. The last column is the reason why the row cannot produce a sixth terminal class.


 Surviving cell after        Active scale profile        Surviving coefficient      Terminal destination     Why no mixed residual
 earlier tests                                                                                               remains
 Empty support or in-        none                        none                       Edge-zero                The tagged cell has
 compatible CRT                                                                                              zero summation do-
                                                                                                             main.
 Boundary, short im-         noncentral or too small     divisor-bounded finite-    Edge                     C1A supplies one strict
 age, large content/gcd,     for a main term             convolution coefficient                             predicate E1вЂ“E7 be-
 square-divisor      tail,                                                                                   fore any central termi-
 high Fourier tail, small                                                                                    nal label is allowed.
 conductor
 Forced equality, re-        diagonal/local fibre        congruence-only local      LocalDiag                The        independent
 peated form, propor-                                    coefficient                                         variables needed for
 tional active forms, or                                                                                     CKP/GoodAWACK
 local dependence                                                                                            are absent; H4 admits
                                                                                                             the cell only as a
                                                                                                             tagged canonical local
                                                                                                             projection.




                                                                  47
 One          F3P-long      one-dimensional    long    local residue-density     LongAP/Local           The     positive    F3P
 AP/local fibre with        local fibre                weight                                           predicate excludes sur-
 no nonlocal arithmetic                                                                                 viving рќњ‡, рќњ†, Fourier,
 coefficient                                                                                            Kloosterman, or nilse-
                                                                                                        quence      coefficients;
                                                                                                        D1.2A then expands
                                                                                                        this local algebra into
                                                                                                        the tagged LPI projec-
                                                                                                        tion.
 Balanced      two-sided    central balanced рќ‘Ћ, рќ‘ћ      divisor-bounded bilin-    CKP                    The defining CKP bal-
 multiplicative bilinear    and dual variables         ear coefficients                                 ance and gcd split
 structure                                                                                              are present; noncen-
                                                                                                        tral or excluded fre-
                                                                                                        quency ranges have al-
                                                                                                        ready been sent to
                                                                                                        C1/G8a local.
 Central-long      affine   full central image, non-   bounded affine finite-    GoodAWACK              The cell is passed
 Branch B cell after all    local, non-CKP             convolution coefficient                          to the GoodAWACK
 strict savings, local                                 with controlled content                          finite-grammar pack-
 dependence, and CKP                                                                                    age. F3T itself only
 balance have failed                                                                                    records the structural
                                                                                                        terminal label and
                                                                                                        does not use the down-
                                                                                                        stream E10 estimate.
 Ordinary           divi-   depends on quotient        divisor-bounded coeffi-   Edge,    LocalDiag,    F4 is a decision tree,
 sor/quotient        cell   case                       cient                     CKP, GoodAWACK,        not a new terminal
 before F4 finishes                                                              or nonterminal de-     class; each outcome is
                                                                                 crease                 one of the existing des-
                                                                                                        tinations.
 Controlled    full-rank    unchanged after finite-    same coefficient with     nonterminal decrease   E5/F3 only transport
 CRT     or    grouping     index restriction          controlled content                               the existing cell; the
 ambiguity                                                                                              F3 measure decreases
                                                                                                        and terminal labelling
                                                                                                        is postponed.




    Thus the apparently broad fallback phrase "central-long affine residual" has a precise meaning
in the active routing table. It is not "whatever remains". It is the row in which:

  1. C1A has not supplied a strict Edge predicate;

  2. F3/F4 have not found a LocalDiag relation;

  3. the positive F3P LongAP/Local predicate has failed, so the cell is not a one-dimensional
     local-coefficient AP fibre;

  4. G8a/CKP balance is absent;

  5. all ordinary divisor, square-divisor, CRT, and grouping operations have either been absorbed
     with controlled content or have strictly decreased the routing measure; and

  6. the remaining affine data is an actual B1/B3/F3/F4-origin terminal GoodAWACK skeleton.

   If any one of these six checks fails, the cell is routed by an earlier row and does not enter
GoodAWACK. If all six checks pass, the cell is structurally a nonlocal central affine macro-template
with controlled content. The later GoodAWACK package proves that no untagged rank-dropping
AFF source survives in such actual terminal skeletons. This is why F3T does not create a hidden
MixedResidual class.
   вЂ”

                                                              48
F3T.5. Finiteness of the table        For fixed рќђЅ0 , the table is finite for three reasons.

  1. B1 has at most 4рќђЅ0 elementary variables and only three elementary coefficient types.

  2. B3 has at most 24рќђЅ0 admissible product groupings.

  3. F3.6 has exactly seven allowed routing-level operation types, and F4 has exactly the four ter-
     minal outcomes Edge, LocalDiag, CKP, GoodAWACK, plus the controlled absorption/decrease
     case.

    All dyadic thresholds used in the rows are qualitative comparisons against fixed powers of рќ‘Ѓ
or log рќ‘Ѓ determined by the global parameter hierarchy. Therefore, after dyadic localization, each
row represents only finitely many tagged subcases, with polylogarithmic total multiplicity.
    вЂ”

F3T.6. Exhaustion theorem

Lemma 10.1 (Lemma F3T). Let рќ’њ be any atom produced by Lemma B1 and preliminarily classified
by Lemma B3. Applying the canonical routing order of F3T.2 and the case table F3T.3 writes рќ’њ
as a finite disjoint sum of tagged terminal atoms in exactly the five terminal classes

             Edge,      CKP,       GoodAWACK,           LocalDiag,        LongAP/Local.
   No sixth terminal class occurs.

Proof. Start with the finite B3 grouping set of рќ’њ. If a terminal row 2вЂ“11 applies, the current cell is
labelled by the corresponding terminal tag. If a nonterminal row 12вЂ“14 applies, then the operation
is one of the allowed F3.6 operations and Lemma F3 proves that Mв™Ї strictly decreases.
    Since Mв™Ї is lexicographically well-founded and the grouping set is finite, the process terminates.
At termination no controlled CRT, ordinary divisor, square-divisor, grouping, saving, or local-
dependence question remains unresolved. The terminal-labelling rows 2вЂ“6 are then exhaustive by
the B3 preliminary classification, the F4 decision tree, and the residual exclusion argument in
F3T.4.
    The deterministic order in F3T.2 assigns a unique terminal tag to each terminal cell. Candidate
overlaps do not create duplicate mass because F3.15 records the exact tagged partition identity.
Hence every B1-origin atom is partitioned into the five named terminal classes and no additional
MixedResidual class exists. Lemma proved.
    вЂ”


Remark 10.2 (F3T.7. Output).

      B1 + B3 + F3 + F4 + E5 =в‡’ complete finite routing exhaustion for B1-origin atoms.

   The terminal estimates are not part of F3T. They are:


Edge в†’ рќђ¶1рќђґ в†’ рќђ¶1,       CKP в†’ рќђє8рќ‘Ћ,       GoodAWACK в†’ GoodAWACK package,                  LongAP/Local в†’ LPI-admissib

   Thus F3T is the finite exhaustion statement that every B1-origin atom has a named terminal
destination.

                                                  49
F3T.8. Logical Dependencies Internal dependencies: B1, B3, the F3 routing definitions F3.1вЂ“
F3.15, F4, E5, LPI, and the proof parameter register.
    Internal nodes served: F3A, E10M, E10K, E10L, I1, and the manuscript routing appendix. F3T
is associated with F3 as its finite routing table; it is not a new hypothesis needed to prove F3.


11       Part 10. F4: Large-divisor and quotient routing
Source file: Lemmas/f_4_ltx.md.

11.0.1    F4. Large Divisor Routing Lemma
F4.0. Role Logical ID: F4.
    Lemma F4 is the exhaustive large-divisor decision procedure used by Lemma F3. It proves the
following statement:

              ordinary large divisor predicates are never left as unresolved residual atoms.
     In other words, if an atom contains a condition

                                                 рќ‘‘ | рќђї(рќ‘§)
     or a quotient equation

                                                рќђї(рќ‘§) = рќ‘‘рќ‘ ,
     then it must be routed to one of the terminal classes

                          Edge,      CKP,       LocalDiag,           GoodAWACK,
    or it must strictly decrease the obstruction measure Mв™Ї from Lemma F3.
    The purpose of Lemma F4 is to close precisely this decision step. LongAP/Local is not an
output of F4 itself; it is a separate terminal branch of the B3/F3 routing layer when the ordinary
large-divisor obstruction handled by F4 is absent or has already been removed.
    Used by: F3, F3T, BGS, HGO2R, E10L, and the GoodAWACK finite-grammar closure layer.
    Uses: the F3 atom interface and routing-measure definitions F3.1вЂ“F3.6, E5, LPI, X6, and
standard lattice/content algebra. The terminal outputs of F4 are structural tags; their estimates
are proved later by C1, D1, G8a, E10L, and H4.
    вЂ”

F4.1. What counts as an ordinary large-divisor predicate                 An ordinary large-divisor pred-
icate means a structural condition of one of the following types:

                                                 рќ‘‘ | рќђї(рќ‘§),


                                                рќђї(рќ‘§) = рќ‘‘рќ‘ ,


                                          рќ‘‘ | gcd(рќђї1 (рќ‘§), рќђї2 (рќ‘§)),
     where:


                                                    50
  вЂў рќђї, рќђї1 , рќђї2 are affine or product-grouped forms already produced by B1/B3;

  вЂў рќ‘‘ is not a square-divisor variable already covered by C1;

  вЂў the predicate does not by itself produce a summable tail of type


                                                      рќ‘‘в€’2 ;
                                                в€‘пёЃ

                                                рќ‘‘>рќђ·

  вЂў the density of the condition is ordinarily of size 1/рќ‘‘, hence not automatically Edge.

   Important exclusion:

                                       рќ‘‘ | рќђї(рќ‘§)       Мёв‡’      Edge.
   F4 exists precisely because the harmonic tail
                                                  в€‘пёЃ 1

                                                  рќ‘‘>рќђ·
                                                        рќ‘‘
   is not small.
   вЂ”

F4.2. Decision parameters        Let

                                            рќђїрќ‘Ѓ = log рќ‘Ѓ.
   We use three qualitative scale regimes for a divisor/quotient pair

                                            рќђї(рќ‘§) = рќ‘‘рќ‘ .

  1. Controlled/local divisor:


                                                рќ‘‘ в‰¤ рќђїрќђµ
                                                     рќ‘Ѓ.

  1. Short-volume regime:

   one of the variables or resulting fibres has effective volume

                                   в‰¤ рќ‘Ѓ рќњЂ(рќ‘Ѓ ),               рќ‘Ѓ в†’ 0.
                                                      рќњЂ(рќ‘Ѓ )рќђїрќђ¶

  1. Central non-short regime:

   both the divisor variable and quotient variable are long enough that neither produces short-
volume Edge.
   The exact constants рќђµ, рќђ¶ are fixed after B1/B3 and depend only on рќђЅ0 . The word "long" always
means long enough to avoid C1 short-volume / Type-I saving.
   вЂ”



                                                   51
F4.3. Fixed divisor absorption           Suppose рќ‘‘ is fixed on the current atom and

                                                  рќ‘‘ | рќђї(рќ‘§).
   Define the restricted lattice coset

                                О›рќ‘‘ = {рќ‘§ в€€ О› : рќђї(рќ‘§) в‰Ў 0           (mod рќ‘‘)},
   and the quotient form

                                               рќђїрќ‘‘ (рќ‘§) = рќђї(рќ‘§)/рќ‘‘.
           рќ‘Ѓ , this is controlled CRT absorption. It is handled by Lemma F3.7, and decreases
   If рќ‘‘ в‰¤ рќђїрќђµ

                                                 рќђ·unabsorbed .
           рќ‘Ѓ , fixed-divisor absorption is not automatically local. Then either:
   If рќ‘‘ > рќђїрќђµ
  1. the fibre volume is short and the atom is Edge by C1;
  2. the restriction forces local dependence and the atom is LocalDiag;
  3. the quotient produces a central-long affine atom with controlled content, hence GoodAWACK;
  4. or it produces balanced multiplicative bilinear structure, hence CKP.
   The exact alternative is decided by the scale and dependency tests below.
   вЂ”

F4.4. Content quotient lemma             Let

                                                рќ‘” = contО› (рќђї).
   On the restricted lattice О›рќ‘‘ , the quotient form satisfies
                                                             рќ‘”
                                     contО›рќ‘‘ (рќђї/рќ‘‘) =               в‰¤ рќ‘”.
                                                           (рќ‘”, рќ‘‘)
Proof. The image of the linear part on the original difference lattice is

                                                 в„“(О›0 ) = рќ‘”Z.
   After imposing рќ‘‘ Мё= 0 and рќ‘‘ | рќђї(рќ‘§), the difference lattice satisfies

                                   в„“(О›рќ‘‘,0 ) = рќ‘”Z в€© рќ‘‘Z = lcm(рќ‘”, рќ‘‘)Z.
   Dividing by рќ‘‘, the image of the quotient linear part is
                                         1                рќ‘”
                                           lcm(рќ‘”, рќ‘‘)Z =        Z.
                                         рќ‘‘              (рќ‘”, рќ‘‘)
   Hence the quotient content is
                                                    рќ‘”
                                                         в‰¤ рќ‘”.
                                                  (рќ‘”, рќ‘‘)
   Lemma proved.
   вЂ”


                                                      52
F4.5. Variable divisor equation        Suppose the ordinary divisor predicate is represented as

                                             рќђї(рќ‘§) = рќ‘‘рќ‘ .
    This is the delicate case because it can introduce a new free variable.
    In Lemma F3, this is handled by placing рќђЅfree last in Mв™Ї . Therefore F4 only needs to prove that
the unresolved divisor predicate is either terminally classified or removed from the obstruction set.
    We split into cases.
    вЂ”

F4.6. Case I: short divisor or short quotient           If either рќ‘‘ or рќ‘  lies in a short range such that
the resulting effective atom volume satisfies

                                       Voleff (рќ’њрќ‘‘,рќ‘  ) в‰Є рќ‘Ѓ рќђїв€’рќђ¶
                                                           рќ‘Ѓ ,

   then the atom is Edge by C1 short-volume or Type-I criteria.
   More explicitly, if after fixing the long variables the remaining sum has at most

                                                рќ‘Ѓ 1в€’рќњЊ
   choices for some fixed \{}( \{}rho>0 \{}), then with divisor-bounded coefficients

                                                     рќ‘Ѓ = рќ‘њ(рќ‘Ѓ ).
                                    |рќ’њрќ‘‘,рќ‘  | в‰Є рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶
   Therefore:

                              ShortDivisor/ShortQuotient =в‡’ Edge.
   вЂ”

F4.7. Case II: forced local dependence          If the equation

                                             рќђї(рќ‘§) = рќ‘‘рќ‘ 
   or a gcd condition

                                        рќ‘‘ | gcd(рќђї1 (рќ‘§), рќђї2 (рќ‘§))
   forces two active forms to satisfy a relation on the current lattice,

                                            рќђїрќ‘– = рќ‘ђрќђїрќ‘— + рќ‘Џ
    or forces a fixed local congruence class that determines one form from another, then the atom
is LocalDiag.
    This includes:

  1. proportional forms;

  2. repeated factors after quotienting;

  3. fixed gcd layers causing a local diagonal relation;

  4. quotient equations where рќ‘  is forced by another active affine form.

                                                  53
   Thus:

                              ForcedLocalDependence =в‡’ LocalDiag.
   No further routing is performed inside F4.
   вЂ”

F4.8. Case III: balanced multiplicative divisor structure Suppose neither short-volume
nor LocalDiag applies, and the quotient equation produces two genuinely long multiplicative vari-
ables or grouped products. Then after grouping, the atom has a balanced bilinear finite-convolution
form of the type

                                            рќ‘ўрќ‘¦ + рќ‘ўвЂІ рќ‘¦ вЂІ = рќ‘Ѓ,
   or equivalently after gcd splitting,

                                   рќ‘Ћрќ‘¦ + рќ‘ћрќ‘¦ вЂІ = рќ‘Ѓрќ‘” ,       (рќ‘Ћ, рќ‘ћ) = 1.
   This is precisely the CKP terminal class, provided the ranges are central/balanced and the
coefficients remain finite-convolution/divisor-bounded.
   The coefficient condition is preserved because the divisor/quotient variables arise from B1 finite-
convolution factors and quotienting does not increase content by F4.4.
   Thus:

                        BalancedMultiplicativeDivisorStructure =в‡’ CKP.
   The subsequent Fourier/Kloosterman-fraction analysis is not part of F4; it is handled by G8a.
   вЂ”

F4.9. Case IV: central-long affine residual            Suppose none of the previous cases applies:

  1. not Edge by short volume or C1-saving;
  2. not LocalDiag by forced dependence;
  3. not CKP by balanced multiplicative grouping.

    Then all multiplicative/divisor ambiguity has been absorbed or resolved, and the remaining
atom has central-long affine structure with Liouville-type factors. The quotient/content conditions
are controlled by F4.4 and E5. Therefore the atom satisfies the GoodAWACK terminal predicate
of Lemma F3:

                                          IsGoodAWACK(рќ’њ).
   So:

                          CentralLongAffineResidual =в‡’ GoodAWACK.
   This is the crucial no-MixedResidual clause:

                                          MixedResidual = в€…
    because any residual non-short, nonlocal, non-CKP atom must by definition be central-long
affine GoodAWACK after F4 resolution.

                                                  54
Quotient-tag completeness for BRS This residual case also records the quotient-tag condition
needed later by BRS/X16BRS. After all F4 routing steps, every divisor рќ‘‘ appearing in a quotient
equation

                                             рќђї = рќ‘‘рќ‘ 
   that survives inside a GoodAWACK terminal routing cell is one of the following:

  1. a fixed controlled divisor absorbed by F4.3;

  2. a variable divisor carrying the F4 quotient tag from F4.5;

  3. a divisor/quotient relation already used to route the atom to Edge, LocalDiag, CKP, or empty
     support by F4.6вЂ“F4.8.

   No untagged variable divisor survives into GoodAWACK terminal labelling. If it did, the atom
would still contain an unresolved ordinary divisor predicate or quotient equation, contradicting
F4.11 and the terminal-labelling criterion of F3.13.
   вЂ”

F4.10. Decision tree      For every ordinary large divisor predicate, apply the following decision
tree:

                                      рќ‘‘ | рќђї(рќ‘§) or рќђї(рќ‘§) = рќ‘‘рќ‘ 

   First ask:

                                  Does it have strict C1 saving?
   If yes:

                                              Edge.
   If no, ask:

                                 Does it force local dependence?
   If yes:

                                           LocalDiag.
   If no, ask:

                    Does it expose balanced multiplicative bilinear structure?
   If yes:

                                              CKP.
   If no, then the remaining atom is central-long affine with controlled content:

                                         GoodAWACK.


                                                55
    Thus:

                   OrdinaryLargeDivisor =в‡’ Edge вЉ” LocalDiag вЉ” CKP вЉ” GoodAWACK.
    вЂ”

F4.10A. Complete Quotient/Divisor Case Table The F4 decision tree is equivalently the
following finite table. This table is the explicit case split used by E10Y and E10M when they assert
that no F4 quotient or divisor survives as an untagged rank-dropping affine operation.

 F4 situation                Operation                  Rank effect                Tag                      Terminal destination
                                                                                                            or continuation
 controlled fixed divisor    restrict to О›рќ‘‘ and re-     finite-index CRT re-       CRT and FixedDiv         F3 continues with Mв™Ї
 рќ‘‘ в‰¤ рќђїрќђµрќ‘Ѓ with рќ‘‘ | рќђї(рќ‘§)       place рќђї by рќђї/рќ‘‘             striction; quotient con-                            decreased
                                                        tent controlled by F4.4
 uncontrolled fixed divi-    apply C1 short-volume      no             terminal    Edge                     terminal Edge
 sor with short fibre        or Type-I saving           GoodAWACK skeleton
 fixed divisor forcing       record local depen-        rank collapse is local     LocalDiag                terminal LocalDiag
 equality, proportional-     dence
 ity, repeated form, or
 fixed local relation
 fixed divisor produc-       expose grouped vari-       rank relation is CKP-      CKP                      terminal CKP
 ing balanced bilinear       ables рќ‘Ћрќ‘¦ + рќ‘ћрќ‘¦ вЂІ = рќ‘Ѓрќ‘”       origin
 structure
 fixed    divisor    with    absorb             quo-    no unresolved quotient     FixedDiv or inherited    terminal
 central-long       affine   tient/content      data    predicate remains          controlled-content tag   GoodAWACK
 residual                    and keep affine resid-
                             ual
 variable quotient equa-     route by strict saving     no       terminal          Edge                     terminal Edge
 tion рќђї(рќ‘§) = рќ‘‘рќ‘  with                                    GoodAWACK skeleton
 short рќ‘‘, short рќ‘ , or
 short effective fibre
 variable quotient forc-     record forced local        rank collapse is local     LocalDiag                terminal LocalDiag
 ing local dependence        quotient relation
 variable        quotient    group into CKP vari-       rank relation is CKP-      CKP                      terminal CKP
 producing       balanced    ables                      origin
 multiplicative/bilinear
 structure
 variable quotient pro-      record the quotient ori-   possible rank effect is    VarQuot                  terminal
 ducing       central-long   gin and controlled con-    tagged by F4                                        GoodAWACK
 affine residual             tent
 quotient or divisor         discard cell               empty support              impossible/empty         zero contribution
 condition incompati-
 ble with the current
 lattice/cell
 divisor predicate ab-       remove predicate from      no unresolved rank-        inherited F3/F4 origin   F3 continues with Mв™Ї
 sorbed without termi-       the obstruction set        affecting residual re-                              strictly decreased
 nal classification                                     mains




    There is no row whose output is an untagged GoodAWACK quotient residual. If a divisor or
quotient remains visible in a GoodAWACK terminal cell, it is either fixed and controlled, carries
the F4 quotient tag, or has already been used to route the atom to Edge, CKP, LocalDiag, empty
support, or a measure-decreasing continuation.
    The table is read with the deterministic F3/F4 routing precedence. If a single algebraic config-
uration visually satisfies more than one row, the earliest applicable terminal predicate in the F3/F4
decision order is chosen and recorded in the origin tag. Later algebraic similarity to another row
does not create a second terminal skeleton and does not leave an additional untagged quotient or
divisor residual.

                                                                56
   вЂ”

F4.11. Exhaustiveness proof

Lemma 11.1 (Lemma F4). Let рќ’њ be an atom produced by B1/B3/F3 containing an unresolved
ordinary large divisor predicate

                                               рќ‘‘ | рќђї(рќ‘§)
   or quotient equation

                                             рќђї(рќ‘§) = рќ‘‘рќ‘ .
   Then after applying the F4 decision procedure, рќ’њ is routed to one of

                       Edge,      LocalDiag,       CKP,       GoodAWACK,
   or the ordinary divisor predicate is absorbed/removed and the F3 measure Mв™Ї strictly decreases.

Proof. If the divisor predicate has an explicit C1 saving mechanism, registered in the C1A admission
ledger, the atom is Edge. This covers square-divisor, short-volume, large-content/gcd, Type-I, high-
frequency and small-conductor saving cases.
    If no C1 saving exists but the divisor relation forces equality, proportionality, fixed gcd-local
dependence, or determines one active form from another on the current lattice, the atom is Local-
Diag.
    If neither Edge nor LocalDiag applies, examine the quotient equation рќђї(рќ‘§) = рќ‘‘рќ‘ . If both the
divisor and quotient variables remain long and the structure is multiplicative/balanced, B3 grouping
converts the atom into a CKP atom. The coefficient and content conditions are preserved by the
content quotient lemma.
    If the multiplicative/balanced CKP structure is absent, then all remaining non-short, nonlocal
structure is central-long affine. The content of marked forms remains controlled by the quotient
lemma and E5 stability. Hence the atom satisfies the GoodAWACK terminal predicate. The
quotient-tag completeness statement in F4.9 ensures that this GoodAWACK atom carries every
surviving quotient divisor as fixed/controlled or as an explicit F4 quotient tag.
    If a controlled fixed divisor is simply absorbed into the lattice, then the unresolved divisor
predicate is removed from рќ’Є(рќ’њ). Under the measure Mв™Ї of Lemma F3, this strictly decreases the
measure, even if an auxiliary quotient variable is introduced.
    Therefore no unresolved ordinary large divisor predicate remains, and no MixedResidual class
survives. Lemma proved.
    вЂ”


F4.12. Relation to F3       Lemma F3 uses F4 as follows:
                                   рќђ№4
         UnresolvedLargeDivisor в€’в€’в†’ Edge/LocalDiag/CKP/GoodAWACK                or   Mв™Ї в†“ .
   Thus F4 supplies the exhaustive decision required by F3.
   With Lemma F4, the large-divisor branch of Lemma F3 is discharged.
   вЂ”



                                                 57
F4.13. What remains outside F4 F4 does not prove analytic estimates for terminal classes.
It only routes ordinary large-divisor atoms.
    Subsequent branch responsibilities:

  вЂў Edge estimates are C1;

  вЂў CKP analysis is G8a;

  вЂў GoodAWACK cancellation is E10;

  вЂў LocalDiag/main assembly is H4.

     F4 also does not replace the analytic inputs in the CKP and GoodAWACK branches.
     вЂ”
Remark 11.2 (F4.14. Output).

                      F4 exhausts ordinary large-divisor predicates for F3.

    Every ordinary divisor predicate is routed to Edge, LocalDiag, CKP, or GoodAWACK, or else
removed with strict decrease of the F3 measure Mв™Ї . No MixedResidual class remains at the F3/F4
interface.

  вЂў F3 dependency on F4 is discharged at the internal routing level;

  вЂў ordinary divisors receive an Edge tag only when a strict Edge-saving predicate is structurally
    present;

  вЂў E5 content stability supports the GoodAWACK residual case;

  вЂў CKP and LocalDiag are structural terminal outputs, whose estimates or local assembly are
    proved later.

F4.15. Logical Dependencies Internal dependencies: the F3 atom interface and routing-
measure definitions F3.1вЂ“F3.6, E5, LPI, X6, and standard lattice/content algebra.
    Internal nodes served: F3, F3T, BGS, HGO2R, E10L, and the GoodAWACK finite-grammar closure
layer.


12       Part 11. C1A: Edge admission ledger
Source file: Lemmas/c1_edge_admission_ledger_ltx.md.

12.0.1    C1A. Admission of Terminal Edge Atoms
C1A.0. Role Logical ID: C1A.
    Used by: C1, F3T, F4, G8a, X10, BRS, TTH, E10L, I1.
    Uses: B1, B3, F3, F3T, F4, C1, G2a, G8a, X10, BRS, X16BRS, X16C, and the proof parameter
register.
    Lemma C1 proves that a terminal atom satisfying one of the strict Edge predicates E1вЂ“E7
contributes рќ‘њ(рќ‘Ѓ ). Lemma C1A records the complementary admission statement: every proof-tree
branch that is routed to Edge carries one of those strict predicates, or is an empty zero cell.


                                               58
   The conclusion is:


Every nonzero terminal Edge atom in the proof tree satisfies one of the strict C1 predicates E1вЂ“E7.
                                                                                           (C1A)
  Thus C1 is used in the proof only in the form

                     EdgeAdmission(рќ’њ) =в‡’ StrictEdgePredicateрќђёрќ‘– (рќ’њ) =в‡’ рќ’њ = рќ‘њ(рќ‘Ѓ ).
   вЂ”

C1A.1. Edge predicates recalled                    The strict C1 predicates are:


    Predicate                                Meaning                               Saving supplied by C1
    E1                                       boundary / partition tail budget      рќ‘Ѓ рќђїв€’рќђ¶0 в€’10
    E2                                       large square-divisor tail             рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 , after the C1 square-tail
                                                                                   hypotheses
    E3                                       large gcd/content volume budget       рќ‘Ѓ рќђїрќђ¶1 /рќ‘” 2 , summable over large рќ‘”
    E4                                       high Fourier frequency budget         рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 by rapid Fourier decay
    E5                                       small-conductor budget                рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 or рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 after full
                                                                                   normalization
    E6                                       short residual volume budget          divisor-bounded mass on volume в‰¤
                                                                                   рќ‘Ѓ рќђїв€’рќђ¶0 в€’рќђ¶1 в€’10
    E7                                       Type I short-variable error budget    рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1




   The following labels are not Edge admissions by themselves:


рќ‘‘ | рќђї(рќ‘§),        рќђї(рќ‘§) = рќ‘‘рќ‘ ,          рќ‘ћ/(рќ‘ћ, рќ‘) в‰¤ рќђїрќђµ ,          вЂњshort variableвЂќ without a quantified residual volume budget.

   They become Edge only through one of the table rows below.
   вЂ”

C1A.2. Admission table

 Source node     Active           C1 predicate    Saving      /    Non-Edge
                 source con-      admitted        summability      alternatives
                 dition                           check            excluded
 B3              A B3 group-      E7 for the      Type I error     The       lo-
 TypeI/Edge      ing exposes      error; E6 if    contributes      cal     main
 candidate       a       short    the    whole    рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 ;      part is not
                 factor or a      residual cell   short-           Edge     and
                 short resid-     has     short   volume cells     is    routed
                 ual cell, and    volume.         contribute       to      Lon-
                 F3 separates                     within the       gAP/Local
                 the      local                   E6 budget.       and H4.
                 main term
                 from       the
                 error term.
 F3        in-   The current      Edge-zero,      Contribution     No terminal
 compatible      tagged lat-      no nonzero      is    exactly    analytic
 CRT/divisibilitytice cell is     C1 predicate    zero.            class is cre-
 cell            empty.           required.                        ated.




                                                              59
F3 square-     A     square-     E2.           C1.2     con-      If рќ‘‘ в‰¤ рќђ·,
divisor        divisor                         trols     the      F3 performs
routing        obstruction                     large square-      controlled
               рќ‘‘2 | рќђї0 (рќ‘Ў)                     divisor tail;      divisibil-
               has рќ‘‘ > рќђ· =                     any zero or        ity/CRT
               рќђїрќђµ .                            short excep-       absorption
                                               tional fibre       and contin-
                                               is charged to      ues;    it is
                                               E6.                not terminal
                                                                  Edge.
F3    strict   The       cur-    The     de-   C1.5 sums          If no strict
Edge detec-    rent       cell   tected        over all such      predicate
tion           satisfies one     E1вЂ“E7 pred-   terminal           holds,      F3
               of C1 E1вЂ“         icate.        cells    with      cannot label
               E7      before                  polylog-           the        cell
               terminal                        arithmic           Edge.
               labelling.                      multiplicity.
F4 Case I:     An ordinary       E6 or E7.     F4 records         If the quo-
short divi-    divisor     or                  the     short      tient is local,
sor/quotient   quotient                        fibre;             F4      routes
               equation                        C1.6/C1.7          LocalDiag;
               leaves only                     gives рќ‘њ(рќ‘Ѓ )        if         bal-
               short resid-                    after coeffi-      anced, CKP;
               ual volume,                     cient losses.      otherwise
               or a Type                                          GoodAWACK.
               I       short-
               variable
               error.
F4       Case  The      ordi-    E2 or E3.     E2     covers      If no quan-
I:    explicit nary divisor                    square tails;      tified saving
               predicate
square/gcd/content                             E3      gives      is    present,
saving         becomes                         рќ‘Ѓ рќђїрќђ¶1 /рќ‘” 2 ,       F4 is not
               a        large                  summable           allowed     to
               square-                         over large рќ‘”.      route       to
               divisor,                                           Edge.
               large gcd, or
               large     con-
               tent layer.
F4       Case  The       divi-   E4 or E5.     E4        uses     Small con-
I:      high-  sor/conductor                   rapid              ductor alone
frequency      condition                       Fourier            is not Edge;
or     small-  appears                         decay after        absent the
conductor      inside CKP-                     coefficient        budget, the
saving         normalized                      losses;     E5     cell remains
               oscillatory                     requires           CKP or is
               scale      and                  the        full    routed    by
               has an ex-                      conductor-         another F4
               plicit     full                 volume             case.
               normalized                      estimate.
               budget.
G8a / X10      The      CKP      E3.           GCD split-         Balanced
CKP excep-     gcd       split                 ting supplies      central    рќ‘”-
tional large-  produces                        the    рќ‘Ѓ/рќ‘” 2 -     layers    are
рќ‘” layers       рќ‘”-layers                        type volume        not     Edge;
               outside the                     saving;            they      are
               balanced                        C1 E3 is           handled
               central                         summable           by X10 or
               range with                      over      the      CKP zero-
               volume sav-                     divisor-           frequency
               ing.                            bounded            local analy-
                                               рќ‘”-layers.          sis.




                                                             60
 G8a        /    The      CKP     h                g>(\{}log          E4.              G2a Fourier      Central          h   g\{}le(\{}log
 X10    high-    Fourier                           N)Л†B\{}).                           decay,           frequencies          N)Л†B\{})
 frequency       frequency                                                             after finite-    \{}(                 are      not
 layers          satisfies \{}(                                                        convolution                           Edge; they
                                                                                       coefficient                           are sent to
                                                                                       losses,                               X10.
                                                                                       supplies
                                                                                       рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .
 G8a       /     The     CKP      E5.              The        full    Without the
 X10 small-      conduc-                           CKP       nor-     full budget,
 conductor       tor satisfies                     malization         the   small-
 layers          рќ‘ћ/(рќ‘ћ, в„Ћрќ‘Ѓрќ‘” ) в‰¤                     and        co-     conductor
                 рќђїрќђµ and the                        efficient          label alone
                 normalized                        weights are        is not an
                 conductor-                        included           Edge admis-
                 volume                            before     ap-     sion.
                 estimate is                       plying      C1
                 available.                        E5.
 G8a / X10       Smooth AP        E1 or E6.        Boundary           CKP в„Ћ = 0
 boundary        expansion,                        tails      are     is not Edge;
 and short-      dyadic trun-                      рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 ;       it   is  lo-
 volume          cation,    or                     short resid-       cal/main
 layers          endpoint                          ual volume         and goes to
                 cells   leave                     is within E6.      H4 through
                 boundary or                                          G8a.
                 short resid-
                 ual volume.
 BRS singu-      A B1-origin                  <X_m(\{}log E6.
                                  L_m(\{}Omega)                                        X16-BRS          If the image
 lar    short-   TC1 coarea                   X_m)Л†{-                                  gives            is       near-
 image           image satis-                 B}\{}) after                             рќ‘Ѓ (log рќ‘Ѓ )рќђ¶16 рќ‘Њ16global,
                                                                                                        /рќ‘‹рќђ¶ + the
 subcell         fies \{}(                    ROC/BRS                                  рќ‘Ѓ 1в€’рќњЊ16 (log рќ‘Ѓ )рќђ¶cell
                                                                                                         16 ;     pro-
                                              filtering.                               choosing рќђµ       ceeds       to
                                                                                       beyond the       TTH/X9L;
                                                                                       C1 and X16       if it has a
                                                                                       losses puts      routing tag,
                                                                                       this inside      it goes to
                                                                                       the strict E6    the     corre-
                                                                                       budget.          sponding
                                                                                                        non-Edge
                                                                                                        terminal
                                                                                                        branch.
 B1/B3/F3/F4     Boundary         E1, and E6 if    The parti-         Interior cells
 boundary        pieces cre-      the residual     tion/transport     continue
 removal         ated        by   cell is short.   multiplicity       to      CKP,
 before          dyadic                            is polylog-        GoodAWACK,
 terminal        partition,                        arithmic           Lon-
 packets         smoothing                         and the C1         gAP/Local,
                 extension,                        boundary           or     Local-
                 CRT       sub-                    budget has         Diag.
                 division,                         a     margin
                 or      affine                    рќђїв€’рќђ¶0 в€’10 .
                 transport.




   вЂ”

C1A.3. Exhaustion of Edge admissions

Lemma 12.1 (Lemma C1A). Every nonzero terminal Edge atom produced by the proof tree appears
in one of the rows of C1A.2 and therefore satisfies one of the strict C1 predicates E1вЂ“E7.

Proof. By Lemma F3T, every B1-origin atom is routed by the finite B1/B3/F3/F4 table. The only
rows of F3T that produce Edge are:

                                                                 61
  1. zero cells;

  2. strict C1 saving predicates detected directly by F3;

  3. F4 Case I cells with an explicit C1 saving mechanism;

  4. large square-divisor tails;

  5. boundary/short-volume or Type I error cells.

    These are exactly the first six rows of C1A.2. The CKP package contributes additional Edge
admissions only for ranges explicitly excluded from the central X10 call: large рќ‘”, high Fourier
frequency, small conductor with full budget, and boundary/short-volume cells. These are the
G8a/X10 rows of C1A.2. The GoodAWACK/TC1 route contributes Edge admissions only through
the BRS singular short-image subcell or through ordinary boundary removal; these are the BRS
and boundary rows of C1A.2.
    There is no other source of Edge routing in the proof tree. Ordinary divisor labels, quo-
tient equations, small conductors, or informal short-variable descriptions are explicitly excluded by
Lemma C1 unless they satisfy one of E1вЂ“E7. Therefore every nonzero terminal Edge atom carries
a strict C1 predicate. Lemma proved.
    вЂ”


C1A.4. Consequence for C1          Combining Lemma C1A with Theorem C1 gives

                                                рќ’њ(рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ),
                                         в€‘пёЃ

                                       рќ’њв€€Edge

     where the sum is over all terminal Edge atoms in the proof tree.
     Thus C1 is now both an implication theorem and an admission-verified terminal branch:

                        EdgeAdmission =в‡’ StrictEdgePredicate =в‡’ рќ‘њ(рќ‘Ѓ ).

C1A.5. Logical Dependencies Internal dependencies: B1, B3, F3, F3T, F4, C1, G2a, G8a, X10,
BRS, X16BRS, X16C.
   Children served: C1, F3T, F4, G8a, X10, BRS, TTH, E10L, I1.


13       Part 12. C1: Unified Edge estimate
Source file: Lemmas/c_1_ltx.md.

13.0.1    C1. Unified Edge Estimate
C1.0. Role Logical ID: C1.
    Used by: C1A, F3T, F4, G8a, X10, BRS, TTH, E10L, I1.
    Uses: B1, B3, F3, F4, C1A, and the proof parameter register.
    C1 proves that every terminal atom satisfying a strict Edge predicate contributes рќ‘њ(рќ‘Ѓ ) after
summation over all B1/B3/F3/F4 cells. It is not a residual class: an atom is Edge only when one
of the budgeted saving predicates below has been verified.



                                                  62
   Lemma C1A records the complementary admission ledger: every proof-tree branch routed to
terminal Edge carries one of the strict predicates E1вЂ“E7, or is an empty zero cell. Thus this file
proves the estimates, while C1A records the admissibility of the Edge inputs.
   In particular:

  1. ordinary divisor condition


                                             рќ‘‘ | рќђї(рќ‘§)
   is not Edge unless there is a separate summable saving;

  1. small-conductor layers are Edge only when an explicit conductor-budget saving is present;

  1. Type I atoms are Edge only for the error part, while their local main term is passed to H4;

  1. every Edge type must have an estimate summable over all typed/dyadic/routing cells.

   The target is:

                                       рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   вЂ”

C1.1. Global bookkeeping convention          Let

                                           рќђї = log рќ‘Ѓ.
   After B1/B3/F3/F4, the number of typed, dyadic, and routing cells is bounded by

                                          #рќ’ћcells в‰¤ рќђїрќђ¶0 ,
   where рќђ¶0 = рќђ¶0 (рќђЅ0 ) is fixed.
   Therefore it is enough to prove for each individual terminal Edge atom рќ’њ:

                                      |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 ,
   or a power-saving estimate

                                       |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1
   for some fixed рќњЊ > 0. After summing over all cells, such contributions remain рќ‘њ(рќ‘Ѓ ).
   This is the Edge budget principle.
   вЂ”

C1.2. Strict Edge predicate       An atom рќ’њ is terminal Edge only if at least one of the following
strict predicates holds.

E1. Boundary / partition tail budget

                                      |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .


                                                63
E2. Square-divisor tail budget        The atom contains

                                               рќ‘‘2 | рќђї0 (рќ‘Ў)
   with рќ‘‘ > рќђ· = рќђїрќђµ , controlled affine content, and the total square-divisor tail is bounded by

                                         |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .

E3. Large-gcd / large-content volume budget                  The atom lies on a large gcd/content layer
рќ‘” > рќђє = рќ‘Ѓ рќњ‚ and satisfies

                                                        рќ‘Ѓ рќђїрќђ¶1
                                          |рќ’њрќ‘” (рќ‘Ѓ )| в‰Є         .
                                                         рќ‘”2

E4. High Fourier frequency budget            The atom is a high-frequency tail whose Fourier weights
satisfy enough rapid decay to give

                                    |рќ’њhigh-в„Ћ (рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .

E5. Small-conductor budget The atom lies in a small-conductor DFI-form layer and satisfies
a separate conductor-volume estimate

                           |рќ’њsmallcond (рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10      or   рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 .
  Small conductor is not Edge merely because рќ‘ћ/(рќ‘ћ, рќ‘) в‰¤ рќђїрќђµ . The estimate must include the full
ambient normalization and all coefficient weights.

E6. Short residual volume budget            The effective residual volume satisfies

                                    Voleff (рќ’њ) в‰¤ рќ‘Ѓ рќђїв€’рќђ¶0 в€’рќђ¶1 в€’10 ,
   so that divisor-bounded coefficients still give

                                            |рќ’њ(рќ‘Ѓ )| = рќ‘њ(рќ‘Ѓ ).

E7. Type I error budget        The atom is a Type I local-counting error with short variable length

                                              рќ‘€ в‰¤ рќ‘Ѓ 1в€’рќњЊ
   and per-fibre error рќ‘‚(рќђїрќђ¶1 ), giving

                               |рќ’њTypeI-рќ‘’рќ‘џрќ‘џ (рќ‘Ѓ )| в‰Є рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 = рќ‘њ(рќ‘Ѓ ).
   The Type I local main part is not Edge; it is routed to LongAP/Local and then H4.
   вЂ”




                                                   64
C1.3. Non-Edge exclusions         The following conditions do not define Edge by themselves:

                                                рќ‘‘ | рќђї(рќ‘§),


                                             рќђї(рќ‘§) = рќ‘‘рќ‘ ,


                                           рќ‘ћ/(рќ‘ћ, рќ‘) в‰¤ рќђїрќђµ ,


           one variable is called "short" without a quantified residual volume budget.
   Such atoms must be routed by F4/F3 to CKP, GoodAWACK, LocalDiag, LongAP/Local, or
to Edge only after an explicit C1 saving predicate is verified.
   вЂ”

C1.4. Edge estimates
Lemma 13.1 (Lemma C1.1. Boundary / partition tails). If

                                     Massboundary (рќ’њ) в‰Є рќ‘Ѓ рќђїв€’рќђµ ,
   and coefficients are bounded by рќђїрќђ¶1 , then

                                        |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђµ+рќђ¶1 .
   Choosing

                                         рќђµ > рќђ¶0 + рќђ¶1 + 10,
   we obtain

                                        |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .
Proof. This is immediate from the mass bound and divisor-bounded/polylogarithmic coefficients.
Lemma proved.
   вЂ”


Lemma 13.2 (Lemma C1.2. Large square-divisor tails). Let

                                            рќђї0 (рќ‘Ў) = рќ‘Ћрќ‘Ў + рќ‘Џ
   on a fibre of length рќ‘‡ , with controlled content

                                          gcd(рќ‘Ћ, рќ‘‘2 ) в‰¤ рќђїрќђ¶1
   uniformly on the relevant support. Then for рќ‘‘ > рќђ· = рќђїрќђµ , the square-divisor tail satisfies

                           #{рќ‘Ў в‰¤ рќ‘‡ : рќ‘‘2 | рќђї0 (рќ‘Ў)} в‰Є рќ‘‡ рќђїрќђ¶1 рќђ·в€’1 + рќ‘Ѓ 1/2+рќ‘њ(1) рќђїрќђ¶1 .
                      в€‘пёЃ

                     рќ‘‘>рќђ·

    Consequently, after restoring the ambient scale, it is Edge whenever the second term is within
the short-volume budget; in particular for fibres satisfying

                                                   65
                                             рќ‘‡ в‰« рќ‘Ѓ 1/2+рќњЊ
   or after summing over complementary short fibres via E6, the square tail gives рќ‘њ(рќ‘Ѓ ).

Proof. For fixed рќ‘‘, the congruence

                                                рќ‘‘2 | рќ‘Ћрќ‘Ў + рќ‘Џ
   has at most рќ‘‚(gcd(рќ‘Ћ, рќ‘‘2 )) residue classes modulo рќ‘‘2 . Thus

                                                                          рќ‘‡
                                                                     (пё‚       )пё‚
                               #{рќ‘Ў в‰¤ рќ‘‡ : рќ‘‘2 | рќ‘Ћрќ‘Ў + рќ‘Џ} в‰Є рќђїрќђ¶1                  +1 .
                                                                          рќ‘‘2
   Split the sum over рќ‘‘ > рќђ· at \{}(d\{}le TЛ†{1/2} \{}) and \{}(d>TЛ†{1/2} \{}).
   For the main range,

                                                      рќ‘‡
                                                         в‰Є рќ‘‡ рќђїрќђ¶1 рќђ·в€’1 .
                                       в€‘пёЃ
                                                рќђїрќђ¶1
                                                      рќ‘‘2
                                    рќђ·<рќ‘‘в‰¤рќ‘‡ 1/2

   The +1 contribution in the range \{}(d\{}le TЛ†{1/2} \{}) gives

                                             рќ‘‚(рќ‘‡ 1/2 рќђїрќђ¶1 ).
    For рќ‘‘ > рќ‘‡ 1/2 , one must also isolate the possible zero of рќђї0 . If рќђї0 (рќ‘Ў) = 0 for some integer рќ‘Ў in
the fibre, there is at most one such point. That point is a zero-volume/forced local fibre and is
routed to E6 (or LocalDiag if the zero condition is structural), with contribution bounded by the
coefficient polylogarithmic budget.
    Away from this possible zero, рќ‘‘2 | рќђї0 (рќ‘Ў) forces |рќђї0 (рќ‘Ў)| в‰Ґ рќ‘‘2 > рќ‘‡ . Hence such terms can occur
only where the affine image escapes the ordinary fibre scale, or in a residual short/exceptional fibre
near the zero. The first case is already outside the long-fibre square-divisor range; the second is
explicitly part of the E6 short-volume budget. Equivalently, the large-рќ‘‘ part is not discarded: it is
either empty on the long regular fibre, a single zero-fibre point, or an E6-routed short residual.
    Hence the square-tail estimate is valid under the strict Edge definition. Lemma proved.


Proof note. The +1-term is not discarded. It is either absorbed by a long-fibre condition or routed
to short-volume Edge E6.
    вЂ”


Lemma 13.3 (Lemma C1.3. Large gcd / content layers). Suppose a layer parameter рќ‘” > рќђє = рќ‘Ѓ рќњ‚
gives the trivial volume estimate

                                                           рќ‘Ѓ рќђїрќђ¶1
                                          |рќ’њрќ‘” (рќ‘Ѓ )| в‰Є            .
                                                            рќ‘”2
   Then

                              |рќ’њрќ‘” (рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїрќђ¶1         рќ‘” в€’2 в‰Є рќ‘Ѓ рќђїрќђ¶1 рќђєв€’1 = рќ‘њ(рќ‘Ѓ ).
                        в€‘пёЃ                        в€‘пёЃ

                        рќ‘”>рќђє                       рќ‘”>рќђє




                                                      66
Proof. Since рќђє = рќ‘Ѓ рќњ‚ ,

                                 рќ‘Ѓ рќђїрќђ¶1 рќђєв€’1 = рќ‘Ѓ 1в€’рќњ‚ рќђїрќђ¶1 = рќ‘њ(рќ‘Ѓ ).
   Lemma proved.
   вЂ”


Lemma 13.4 (Lemma C1.4. High Fourier frequency tails). Assume a Fourier expansion contributes
weights satisfying, for every рќђґ > 0,
                                 вѓ’1
                                 вѓ’
                                    М‚пёЃрќ‘Њ в„Ћ вѓ’ в‰Єрќђґ рќ‘”(1 + |в„Ћ|рќ‘”)в€’рќђґ .
                                       (пё‚ )пё‚вѓ’
                                            вѓ’
                                 вѓ’ рќ‘Љ
                                 вѓ’рќ‘ћ      рќ‘ћ вѓ’
   Let high frequency be defined by

                                           |в„Ћ| > рќђ» = рќђїрќђµ .
   Then choosing рќђґ в‰Ґ рќђ¶0 + рќђ¶1 + 20, the total high-frequency contribution is

                                            в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10
   provided the remaining normalized coefficient sums satisfy the standard CKP/LongAP divisor-
bound budget

                                              в‰Є рќ‘Ѓ рќђїрќђ¶1 .

Proof. For fixed рќ‘” в‰Ґ 1,

                                       рќ‘”(1 + |в„Ћ|рќ‘”)в€’рќђґ в‰Єрќђґ рќђ» 1в€’рќђґ рќ‘” 1в€’рќђґ .
                                в€‘пёЃ

                               |в„Ћ|>рќђ»

   For рќ‘” в‰Ґ 1, this is

                                             в‰Єрќђґ рќђ» 1в€’рќђґ .
   Multiplying by the remaining divisor-bounded mass \{}(N LЛ†{C_1} \{}) and choosing рќђґ and
рќђµ sufficiently large gives

                                      рќ‘Ѓ рќђїрќђ¶1 рќђ» 1в€’рќђґ в‰¤ рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .
   Summing over polylogarithmic cells is harmless. Lemma proved.
   вЂ”


Lemma 13.5 (Lemma C1.5. Small-conductor budget). Let a Kloosterman-fraction phase have
conductor
                                                      рќ‘ћ
                                             рќ‘ћ1 =          .
                                                    (рќ‘ћ, рќ‘)
   A layer with

                                            рќ‘ћ1 в‰¤ рќ‘„0 = рќђїрќђµ


                                                    67
    is terminal Edge only if, after all ambient normalizations and coefficient weights are included,
it satisfies

                            |рќ’њрќ‘ћ1 в‰¤рќ‘„0 (рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10      or   рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 .
   Under this strict predicate, small-conductor layers give рќ‘њ(рќ‘Ѓ ).

Proof. This is by definition of the small-conductor Edge predicate. The point is that small con-
ductor alone does not automatically imply Edge. If the estimate is not available, the layer remains
in the CKP analysis and is not terminal C1 Edge.


Proof note. The shortcut bound

                                       рќ‘Ѓ 1/2+рќ‘њ(1) рќђїрќђµ+1 = рќ‘њ(рќ‘Ѓ )
   by counting possible denominators may miss ambient scale factors. C1 therefore requires an
explicit conductor-volume budget.
   вЂ”


Lemma 13.6 (Lemma C1.6. Short residual volume atoms). If an atom satisfies

                                     Voleff (рќ’њ) в‰¤ рќ‘Ѓ рќђїв€’рќђ¶0 в€’рќђ¶1 в€’10 ,
   and coefficients are bounded by рќђїрќђ¶1 , then

                                        |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 .

Proof. Immediate from the definition of effective volume and coefficient bounds. Lemma proved.
   вЂ”


Lemma 13.7 (Lemma C1.7. Type I short-variable error). Consider a Type I configuration whose
error part has the form
                                            в€‘пёЃ
                                                 рќ›ј(рќ‘ў)рќђё(рќ‘ў),
                                           рќ‘ўв€јрќ‘€
   where

                                            |рќђё(рќ‘ў)| в‰Є рќђїрќђ¶1
   and

                                             рќ‘€ в‰¤ рќ‘Ѓ 1в€’рќњЊ
   for fixed рќњЊ > 0. Then

                                     |рќ›ј(рќ‘ў)рќђё(рќ‘ў)| в‰Є рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 = рќ‘њ(рќ‘Ѓ ).
                               в€‘пёЃ

                               рќ‘ўв€јрќ‘€

Proof. Use divisor-boundedness of рќ›ј and the per-fibre error bound. Lemma proved.


                                                  68
Important distinction Only the error part is Edge. The local main part of Type I counting is
routed to LongAP/Local and H4.
   вЂ”

C1.5. Unified Edge theorem

Theorem 13.8 (Theorem C1). Let \{}(R_{\{}mathrm{Edge}}(N) \{}) be the total contribution
of all terminal Edge atoms produced by Lemmas B1, B3, F3, and F4, together with the CKP and
TC1 excluded Edge ranges registered in Lemma C1A, where Edge is defined by the strict predicates
E1вЂ“E7 above. Then

                                         рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).

Proof. Each terminal Edge atom satisfies either a logarithmic saving

                                      |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ рќђїв€’рќђ¶0 в€’10
   or a power saving

                                        |рќ’њ(рќ‘Ѓ )| в‰Є рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 .
   The number of typed/dyadic/routing cells is at most рќђїрќђ¶0 . Hence logarithmically saved atoms
contribute

                               в‰Є рќђїрќђ¶0 рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 = рќ‘Ѓ рќђїв€’10 = рќ‘њ(рќ‘Ѓ ).
   Power-saved atoms contribute

                                    в‰Є рќђїрќђ¶0 рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 = рќ‘њ(рќ‘Ѓ ).
   Summing over the seven strict Edge types proves

                                         рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   The theorem is proved.
   вЂ”


C1.6. Relation to F3/F4       The F3/F4 interface uses C1 only in the following form:

                             StrictEdgePredicate(рќ’њ) =в‡’ рќ’њ = рќ‘њ(рќ‘Ѓ ).
   Ordinary divisor conditions are not Edge unless one of the strict C1 predicates applies. Other-
wise F4 routes them to LocalDiag, CKP or GoodAWACK.
   Thus the interface is now:
                                        вЋ§
                                        вЋЄ
                                        вЋЄ
                                        вЋЄ Edge,                if strict C1 saving exists,
                                        вЋЄ
                                        вЋЁLocalDiag,
                                        вЋЄ
              рќђ№ 4 : OrdinaryDivisor в†’
                                        вЋЄ
                                        вЋЄ
                                        вЋЄ CKP,
                                          GoodAWACK.
                                        вЋЄ
                                        вЋЄ
                                        вЋ©
   вЂ”

                                                 69
C1.7. Interface refinements

  1. Square-divisor tails explicitly acknowledge the +1-term and require it to be handled by long-
     fibre or short-volume budget.

  1. Small-conductor layers are Edge only with a full conductor-volume budget.

  1. High Fourier tails include a full budget after remaining coefficient mass.

  1. Type I main terms are separated from Type I error terms.

  1. Edge is now a strict predicate with a budget, not a descriptive label.

     вЂ”
Remark 13.9 (C1.8. Output).

Every terminal Edge atom carries either logarithmic saving рќ‘Ѓ рќђїв€’рќђ¶0 в€’10 or power saving рќ‘Ѓ 1в€’рќњЊ рќђїрќђ¶1 .

     Ordinary divisor and small-conductor labels alone are not Edge without explicit saving.
     Consequences:

  вЂў F3/F4 may route to Edge only after a strict C1 predicate is verified;

  вЂў small-conductor Edge routing is allowed only after a budgeted condition is verified;

  вЂў Type I local main terms are routed to H4, not counted as Edge.

C1.9. Logical Dependencies Internal dependencies: B1, B3, F3, F4, C1A, proof parameter
register.
    Children served: all terminal routing branches, especially F4, BRS/TTH, X10, C1A, and I1.


14       Part 13. I1: Final weighted assembly
Source file: Lemmas/i_1_ltx.md.

14.0.1    I1. Final Weighted Assembly
I1.0. Statement and Role Lemma I1 is the final weighted assembly theorem. It combines
the exact B1 decomposition, the B3/F3/F4 terminal routing, the Edge/Local/CKP/GoodAWACK
terminal estimates, and the LPI local projection assembled by H4 to prove

                                     рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ )
    for all sufficiently large even рќ‘Ѓ . The Branch B input is Lemma E10L, which proves рќ‘…GoodAWACK (рќ‘Ѓ ) =
рќ‘њ(рќ‘Ѓ ) without using X8.
    Logical dependencies: PAR, GEB, B1, B3, F3, F4, C1, D1, G8a, E10L, and H4. Outputs
served: G1 and G0H.
    вЂ”



                                                70
I1.1. Setup: Inputs     Let рќ‘Ѓ be a sufficiently large even integer. The proof-level inputs are:

                                       рќђµ1,       рќђµ3,        рќђ№ 3,   рќђ№ 4,


                       рќђ¶1,   рќђ·1,      рќђє8рќ‘Ћ,       рќђё10рќђї,        рќђ»4,        рќ‘ѓ рќђґрќ‘…,   рќђєрќђёрќђµ.
   The external/standard inputs still visible through these inputs are:

  1. X1, the HeathвЂ“Brown identity used in B1;

  2. X9L-GT, the averaged linear/Fourier Liouville input used by E10L through the TC1 coarea
     route after TTH supplies the near-global Davenport/AP range;

  3. X10, the DFI Kloosterman-fraction input used by G8a, with the smooth-weight derivative
     interface supplied by CKPD;

  4. X16, only through the BRS/X16 carrier-slice interface supplied by X16BRS and X16C.

   The I1 proof does not use X8.
   вЂ”

I1.2. Statement: Theorem I1

Theorem 14.1 (Theorem I1). For all sufficiently large even рќ‘Ѓ ,

                        рќ‘…О› (рќ‘Ѓ ) =               О›(рќ‘›1 )О›(рќ‘›2 ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
                                      в€‘пёЃ

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

   Here
                                     в€ЏпёЃ рќ‘ќ в€’ 1                      в€ЏпёЃ (пё‚         1
                                                                                     )пё‚
                      S(рќ‘Ѓ ) = 2рќђ¶2                ,       рќђ¶2 =              1в€’          .
                                     рќ‘ќ|рќ‘Ѓ
                                           рќ‘ќв€’2                     рќ‘ќ>2
                                                                              (рќ‘ќ в€’ 1)2
                                     рќ‘ќ>2
   вЂ”

I1.3. Setup: Exact B1 Decomposition                  By Lemma B1, for fixed sufficiently large рќђЅ0 в‰Ґ рќђЅ* ,

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

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

   where

                                        #BрќђЅ0 в‰ЄрќђЅ0 (log рќ‘Ѓ )4рќђЅ0 .
   This decomposition is exact. No error term is introduced at this stage.
   вЂ”




                                                       71
I1.4. Setup: Terminal Routing         By Lemma B3, each typed B1 block enters one of the prelim-
inary routing families:

                     TypeI/Edge,       LongAP/Local,             BranchB,   CKP.
   By Lemma F3, together with the exhaustive large-divisor decision in Lemma F4, every descen-
dant is finally routed into one of the terminal tagged classes:

             Edge,      LongAP/Local,        CKP,             GoodAWACK,     LocalDiag.
   These terminal classes are disjoint at the tagged routing-history level and exhaust all descen-
dants. The exact identity used here is Lemma F3.15: for each parent B1 block в„¬,
                                     рќ‘…в„¬ (рќ‘Ѓ ) =              рќ‘…в„¬,рќњЏ (рќ‘Ѓ ),
                                                   в€‘пёЃ

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

before any terminal estimate is applied. Therefore the total weighted sum decomposes as


       рќ‘…О› (рќ‘Ѓ ) = рќ‘…Edge (рќ‘Ѓ ) + рќ‘…LongAP (рќ‘Ѓ ) + рќ‘…CKP (рќ‘Ѓ ) + рќ‘…GoodAWACK (рќ‘Ѓ ) + рќ‘…LocalDiag (рќ‘Ѓ ).
   вЂ”

I1.5. Proof: Edge Contribution By Lemma C1, every terminal Edge atom carries one of the
strict C1 saving mechanisms. Hence, after summing over the polylogarithmic family of B1/B3/F3
descendants,

                                         рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   Ordinary divisor labels are not counted as Edge unless a strict C1 saving predicate is verified;
otherwise F4 routes them to CKP, LocalDiag, or GoodAWACK.
   вЂ”

I1.6. Proof: LongAP/Local Contribution By Lemma D1, including the coefficient-exclusion
Lemma D1.2A, every tagged LongAP/Local atom contains only controlled local AP/congruence
data and equals the explicit LPI local projection of the same tagged B1/F3 cell plus an error рќ‘њ(рќ‘Ѓ ).
In particular, the only local replacement is О›(рќ‘›) в†¦в†’ О›рќ‘„ (рќ‘› mod рќ‘„). Thus

                               рќ‘…LongAP (рќ‘Ѓ ) = рќ‘ЂLongAP (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
    The local main term рќ‘ЂLongAP (рќ‘Ѓ ) is passed to H4 with its parent B1 tag and routing-history
tag.
    вЂ”

I1.7. Proof: CKP Contribution By Lemma G8a, every tagged CKP atom equals its LPI-
admissible canonical local projection plus an error рќ‘њ(рќ‘Ѓ ). Therefore

                                   рќ‘…CKP (рќ‘Ѓ ) = рќ‘ЂCKP (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
    The nonzero-frequency CKP contribution is handled by the G8a package, whose external ana-
lytic input is the DFI theorem X10. The zero-frequency term is the canonical local term admitted
by H4.
    вЂ”

                                                   72
I1.8. Proof: Branch B / GoodAWACK Contribution                      By Lemma E10L,

                                        рќ‘…GoodAWACK (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   Its proof route is:


TC1 split+TC1 Fourier closure+HighTC rerouting+AFF-OC/E10K =в‡’ рќ‘…GoodAWACK (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).

   The GoodAWACK contribution does not use X8. The Branch B external input is the citation-
grade X9L-GT averaged Liouville/Fourier estimate in the near-global Davenport/AP range.
   вЂ”

I1.9. Proof: LocalDiag Contribution Terminal LocalDiag atoms are not error terms. They
are canonical local/main terms admitted by H4. Let

                                              рќ‘ЂLocalDiag (рќ‘Ѓ )
   be their total tagged local contribution. These terms are included in the local main sum together
with LongAP/Local and CKP zero-frequency terms.
   вЂ”

I1.10. Proof: Local/Main Compatibility              Collect all canonical local terms:

                         рќ‘Ђlocal (рќ‘Ѓ ) = рќ‘ЂLongAP (рќ‘Ѓ ) + рќ‘ЂCKP (рќ‘Ѓ ) + рќ‘ЂLocalDiag (рќ‘Ѓ ).
   There is no fourth local summand. By LPI and H4, every auxiliary local-looking term produced
by controlled CRT absorption, fixed-divisor quotienting, or primitive local slicing is a tagged sub-
term of one of the three displayed classes. Endpoint and smooth-boundary localizations are C1
Edge errors and are not part of рќ‘Ђlocal .
   By Lemma H4, all active local/main terms satisfy the explicit tagged admission condition
                                  local
                                 рќ‘Ђв„¬,рќњЏ   (рќ‘Ѓ ) = Locрќ‘„ рќ‘…в„¬,рќњЏ (рќ‘Ѓ ) + рќ‘њв„¬,рќњЏ (рќ‘Ѓ ),

where Locрќ‘„ is the single О›рќ‘„ -replacement inside the same parent B1 block and routing cell. H4
reconstructs the local Goldbach model by tagged linearity over the exact B1/F3 partition, proves
no double counting of local terms, and computes the finite CRT local factors. Thus there is no
branch-specific local surrogate and

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

I1.11. Proof: Final Summation             Using the terminal decomposition and the branch estimates:


       рќ‘…О› (рќ‘Ѓ ) = рќ‘…Edge (рќ‘Ѓ ) + рќ‘…LongAP (рќ‘Ѓ ) + рќ‘…CKP (рќ‘Ѓ ) + рќ‘…GoodAWACK (рќ‘Ѓ ) + рќ‘…LocalDiag (рќ‘Ѓ ),


                            рќ‘…Edge (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ),     рќ‘…GoodAWACK (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ),


                                                    73
              рќ‘…LongAP (рќ‘Ѓ ) = рќ‘ЂLongAP (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ),      рќ‘…CKP (рќ‘Ѓ ) = рќ‘ЂCKP (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ),
   and LocalDiag contributes only canonical local terms. GEB records that the branch рќ‘њ(рќ‘Ѓ )
terms above, including all polylogarithmic terminal summations, CKP derivative losses, TC1 Dav-
enport/AP losses, X16/BRS slice-floor losses, and H4 boundary terms, combine to a single рќ‘њ(рќ‘Ѓ )
remainder. Hence

                                    рќ‘…О› (рќ‘Ѓ ) = рќ‘Ђlocal (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
     By H4,

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

                                     рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
     This proves Theorem I1.
     вЂ”

I1.12. Output: Positivity Handoff to G1/G2             For even рќ‘Ѓ ,

                                          S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 > 0.
     Therefore I1 implies

                                             рќ‘…О› (рќ‘Ѓ ) > 0
   for all sufficiently large even рќ‘Ѓ , once the рќ‘њ(рќ‘Ѓ ) error is smaller than рќђ¶2 рќ‘Ѓ . This is only the
weighted positivity statement; the genuine prime representation uses G2 to remove nontrivial prime
powers and G1/G0H to convert positive genuine prime-pair weight into an actual prime pair.
   The final passage from the weighted asymptotic to a representation by two primes uses:

     1. Lemma G2, prime powers negligible;

     2. Lemma G1, passage from the genuine prime-pair asymptotic to strong Goldbach.

     вЂ”
Remark 14.2 (I1.13. Output).

              I1 proves the final weighted assembly using E10L as the Branch B input.

     Thus

                                     рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
     Together with G2 and G1, this proves the root Goldbach statement for all sufficiently large even
рќ‘Ѓ.




                                                  74
I1.14. Logical Dependencies External dependencies: X1 through B1, X9L-GT through E10L/TTH,
and X10 through G8a/CKPD.
   Internal dependencies: PAR, GEB, B1, B3, F3, F4, C1, D1, G8a, E10L, and H4.
   Children served: G1 and G0H.


15       Part 14. G2: Prime powers negligible
Source file: Lemmas/g_2_ltx.md.

15.0.1     G2. Prime Powers Negligible Lemma
G2.0. Statement and Role           Lemma G2 is needed to pass from the weighted asymptotic

                          рќ‘…О› (рќ‘Ѓ ) =                О›(рќ‘›1 )О›(рќ‘›2 ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ )
                                         в€‘пёЃ

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

   to an actual representation of рќ‘Ѓ as a sum of two primes. The von Mangoldt function is
supported not only on primes, but also on prime powers:

                                                   log рќ‘ќ,    рќ‘› = рќ‘ќрќ‘ , рќ‘ в‰Ґ 1,
                                              {пёѓ
                                   О›(рќ‘›) =
                                                   0,        otherwise.
    Therefore we have to show that the contribution of representations in which at least one sum-
mand is a nontrivial prime power рќ‘ќрќ‘ , рќ‘ в‰Ґ 2, is small compared with the main term в‰Ќ рќ‘Ѓ .
    Logical dependencies: elementary prime-power counting. If combined with I1, the output served
is G1/G0H.
    вЂ”

G2.1. Setup: Prime-Prime and Prime-Power Decomposition                              Define

                                   рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) =                     log рќ‘ќ1 log рќ‘ќ2 .
                                                       в€‘пёЃ

                                                    рќ‘ќ1 +рќ‘ќ2 =рќ‘Ѓ
                                                   рќ‘ќ1 ,рќ‘ќ2 prime

     The sum is over ordered positive prime pairs, matching the ordered convention for рќ‘…О› (рќ‘Ѓ ).
     This is the genuine prime-prime contribution.
     Denote the contribution of nontrivial prime powers by

                                      рќ‘…pow (рќ‘Ѓ ) = рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ).
     Then рќ‘…pow (рќ‘Ѓ ) consists of pairs

                                                   рќ‘›1 + рќ‘› 2 = рќ‘Ѓ
     such that at least one of рќ‘›1 , рќ‘›2 has the form

                                               рќ‘ќрќ‘ ,          рќ‘ в‰Ґ 2.
     The lemma aims to prove:

                                рќ‘…pow (рќ‘Ѓ ) = рќ‘‚(рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 ) = рќ‘њ(рќ‘Ѓ ).
     вЂ”

                                                            75
G2.2. Proof: Counting Nontrivial Prime Powers                 Let

                              рќ’«2 (рќ‘Ѓ ) = {рќ‘ќрќ‘ в‰¤ рќ‘Ѓ : рќ‘ќ prime, рќ‘ в‰Ґ 2}.
   Then

                                         #рќ’«2 (рќ‘Ѓ ) в‰Є рќ‘Ѓ 1/2 .
   Indeed, if рќ‘ќрќ‘ в‰¤ рќ‘Ѓ and рќ‘ в‰Ґ 2, then

                                               рќ‘ќ в‰¤ рќ‘Ѓ 1/2 .
   For each prime рќ‘ќ в‰¤ рќ‘Ѓ 1/2 , the number of possible exponents рќ‘ в‰Ґ 2 is at most

                                               рќ‘‚(log рќ‘Ѓ ).
   A crude bound therefore gives

                                     #рќ’«2 (рќ‘Ѓ ) в‰Є рќ‘Ѓ 1/2 log рќ‘Ѓ.
   A sharper elementary bound removes the extra logarithm:

               #рќ’«2 (рќ‘Ѓ ) в‰¤ #{рќ‘ќ2 в‰¤ рќ‘Ѓ } +         #{рќ‘ќрќ‘ в‰¤ рќ‘Ѓ } в‰Є рќ‘Ѓ 1/2 +
                                         в€‘пёЃ                           в€‘пёЃ
                                                                            рќ‘Ѓ 1/рќ‘ в‰Є рќ‘Ѓ 1/2 .
                                         рќ‘в‰Ґ3                          рќ‘в‰Ґ3

   Indeed, the dominant contribution is from squares.
   вЂ”

G2.3. Proof: Weighted Bound for Bad Pairs                For every рќ‘› в‰¤ рќ‘Ѓ , we have

                                           О›(рќ‘›) в‰¤ log рќ‘Ѓ.
   If a representation counted in рќ‘…pow (рќ‘Ѓ ) has рќ‘›1 в€€ рќ’«2 (рќ‘Ѓ ), then рќ‘›2 = рќ‘Ѓ в€’ рќ‘›1 is determined. Its
contribution is at most

                                     О›(рќ‘›1 )О›(рќ‘›2 ) в‰¤ (log рќ‘Ѓ )2 .
   Thus the contribution of pairs with first coordinate a nontrivial prime power is

                              в‰Є #рќ’«2 (рќ‘Ѓ )(log рќ‘Ѓ )2 в‰Є рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 .
   The same estimate holds for pairs with second coordinate a nontrivial prime power. Hence, by
the union bound,

                                   рќ‘…pow (рќ‘Ѓ ) в‰Є рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 .
   Therefore

                                         рќ‘…pow (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   вЂ”




                                                   76
G2.4. Output: Consequence for the Genuine Prime-Prime Sum                      Since

                                  рќ‘…О› (рќ‘Ѓ ) = рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) + рќ‘…pow (рќ‘Ѓ ),
   and

                                         рќ‘…pow (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ),
   we get

                                    рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   Using I1,

                                    рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ),
   we obtain

                                    рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   Thus the weighted contribution from genuine prime pairs has the same main term as the full
von Mangoldt sum. The singular series is the H4/I1 Goldbach singular series; G2 only removes
nontrivial prime-power support and does not alter the local factor.
   вЂ”

G2.5. Statement and Proof: Lemma G2
Lemma 15.1 (Lemma G2). Let

                                 рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) =                  log рќ‘ќ1 log рќ‘ќ2 .
                                                  в€‘пёЃ

                                               рќ‘ќ1 +рќ‘ќ2 =рќ‘Ѓ
                                              рќ‘ќ1 ,рќ‘ќ2 prime

   Then

                          рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘‚(рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 ) = рќ‘њ(рќ‘Ѓ ).
   Consequently, if

                                    рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ),
   then

                                    рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
Proof. The difference рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) is the nonnegative contribution of representations where
at least one summand is a nontrivial prime power рќ‘ќрќ‘ , рќ‘ в‰Ґ 2. There are рќ‘‚(рќ‘Ѓ 1/2 ) such possible
summands up to рќ‘Ѓ , and for each such summand the other summand is uniquely determined. Since
О›(рќ‘›) в‰¤ log рќ‘Ѓ , each weighted contribution is at most (log рќ‘Ѓ )2 . Therefore the total contribution is

                                     рќ‘‚(рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 ) = рќ‘њ(рќ‘Ѓ ).
   The consequence follows by subtracting this negligible term from I1. Lemma proved.
   вЂ”


                                                   77
Remark 15.2 (G2.6. Output).

                            рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘‚(рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 ) = рќ‘њ(рќ‘Ѓ ).

   Hence the genuine prime-prime weighted sum has the same main term as рќ‘…О› (рќ‘Ѓ ). This is the
input from G2 used by G1 and G0H.

G2.7. Logical Dependencies External dependencies: elementary prime-power counting and
the bound О›(рќ‘›) в‰¤ log рќ‘Ѓ .
   Internal dependencies: I1 only for the stated consequence рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   Children served: G1 and G0H.


16       Part 15. G1: Weighted asymptotic to strong Goldbach
Source file: Lemmas/g_1_ltx.md.

16.0.1    G1. Passage from Weighted Asymptotic to Strong Goldbach
G1.0. Statement and Role Theorem G1 is the final passage from the weighted asymptotic to
the strong Goldbach statement for all sufficiently large even integers.
   From I1 we have:

                                      рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
  The singular series here is the Goldbach Euler product obtained in H4 from the finite local
model, not a branch-specific local surrogate.
  From G2 we have:

                                      рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ),
     where

                                   рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) =                  log рќ‘ќ1 log рќ‘ќ2 .
                                                    в€‘пёЃ

                                                 рќ‘ќ1 +рќ‘ќ2 =рќ‘Ѓ
                                                рќ‘ќ1 ,рќ‘ќ2 prime

     The sum is over ordered positive prime pairs, matching the convention in рќ‘…О› (рќ‘Ѓ ) =    рќ‘›1 +рќ‘›2 =рќ‘Ѓ О›(рќ‘›1 )О›(рќ‘›2 ).
                                                                                          в€‘пёЂ

     We have to prove that, for all sufficiently large even рќ‘Ѓ ,

                                             рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) > 0.
     This immediately implies the existence of primes рќ‘ќ1 , рќ‘ќ2 such that

                                             рќ‘Ѓ = рќ‘ќ1 + рќ‘ќ2 .
     Logical dependencies: I1 and G2. Output served: G0 and G0H.
     вЂ”




                                                     78
G1.1. Setup: Positivity of the Singular Series                 For even рќ‘Ѓ , the Goldbach singular series is
                                                         в€ЏпёЃ рќ‘ќ в€’ 1
                                       S(рќ‘Ѓ ) = 2рќђ¶2                      ,
                                                         рќ‘ќ|рќ‘Ѓ
                                                             рќ‘ќв€’2
                                                         рќ‘ќ>2

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

   Each factor
                                                   рќ‘ќв€’1
                                                   рќ‘ќв€’2
   is positive for рќ‘ќ > 2. Therefore

                                                 S(рќ‘Ѓ ) > 0
   for every even рќ‘Ѓ .
   Moreover, since each factor (рќ‘ќ в€’ 1)/(рќ‘ќ в€’ 2) > 1, we have the uniform lower bound

                                           S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 > 0
   for even рќ‘Ѓ .
   вЂ”

G1.2. Proof: Positivity of the Genuine Prime-Pair Weighted Sum                        By I1 and G2,

                                      рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
   Since \{}(\{}mathfrak S(N) \{}ge2C_2>0\{}), we have

                                           S(рќ‘Ѓ )рќ‘Ѓ в‰Ґ 2рќђ¶2 рќ‘Ѓ.
   The error term рќ‘њ(рќ‘Ѓ ) satisfies, for sufficiently large рќ‘Ѓ ,

                                            |рќ‘њ(рќ‘Ѓ )| в‰¤ рќђ¶2 рќ‘Ѓ.
   Hence for sufficiently large even рќ‘Ѓ ,

                                рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) в‰Ґ 2рќђ¶2 рќ‘Ѓ в€’ рќђ¶2 рќ‘Ѓ = рќђ¶2 рќ‘Ѓ > 0.
   Thus

                                             рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) > 0.
   вЂ”




                                                    79
G1.3. Proof: From Positivity to a Prime Representation                          By definition,

                                  рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) =                  log рќ‘ќ1 log рќ‘ќ2 .
                                                   в€‘пёЃ

                                                рќ‘ќ1 +рќ‘ќ2 =рќ‘Ѓ
                                               рќ‘ќ1 ,рќ‘ќ2 prime

   Each summand is nonnegative, and it is strictly positive exactly when there is a representation

                                               рќ‘Ѓ = рќ‘ќ1 + рќ‘ќ2
   with рќ‘ќ1 , рќ‘ќ2 prime.
   If no such representation existed, then the sum would be empty and

                                             рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = 0.
   But for sufficiently large even рќ‘Ѓ we have shown

                                             рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) > 0.
   Therefore at least one prime pair exists.
   вЂ”

G1.4. Statement and Proof: Theorem G1

Theorem 16.1 (Theorem G1). Assume I1 and G2:

                                     рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ),
   and

                                     рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ).
   Then every sufficiently large even integer рќ‘Ѓ can be represented as a sum of two primes:

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

Proof. By G2,

                                     рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ).
   By I1,

                                     рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).
    For even рќ‘Ѓ , the singular series satisfies S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 > 0. Therefore рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) > 0 for all
sufficiently large even рќ‘Ѓ . Since рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) is a sum of positive weights log рќ‘ќ1 log рќ‘ќ2 over prime repre-
sentations рќ‘ќ1 + рќ‘ќ2 = рќ‘Ѓ , positivity implies that at least one such representation exists. The theorem
is proved.
    вЂ”




                                                    80
Remark 16.2 (G1.5. Output).

                 I1 and G2 imply strong Goldbach for all sufficiently large even рќ‘Ѓ.

     The only ingredients used at this final stage are:

  1. the asymptotic рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ) from I1;

  2. the prime-power removal рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘њ(рќ‘Ѓ ) from G2;

  3. positivity of the Goldbach singular series for even рќ‘Ѓ .

G1.6. Logical Dependencies External dependencies: standard positivity of the singular series
Euler product.
   Internal dependencies: I1 and G2.
   Children served: G0 and G0H.


17       Part 16. G0H: Final handoff verification
Source file: Lemmas/g0_final_handoff_verification_ltx.md.

17.0.1     G0H. Final Handoff from I1/G2 to Strong Goldbach
G0H.0. Statement and Role            Lemma G0H records the final proof-tree handoff

                                       рќђј1 + рќђє2 =в‡’ рќђє1 =в‡’ рќђє0.
   It proves that the weighted von Mangoldt asymptotic in I1 implies the existence of a genuine
prime representation after the prime-power contribution is removed by G2.
   Logical dependencies: I1, G2, and G1. Output served: G0.

G0H.1. Setup: Ordered-Pair Conventions                     All Goldbach sums below are over ordered posi-
tive pairs.

                                   рќ‘…О› (рќ‘Ѓ ) :=                 О›(рќ‘›1 )О›(рќ‘›2 ),
                                                    в€‘пёЃ

                                                 рќ‘›1 +рќ‘›2 =рќ‘Ѓ
                                                  рќ‘›1 ,рќ‘›2 в‰Ґ1

     and

                                   рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) :=                  log рќ‘ќ1 log рќ‘ќ2 .
                                                     в€‘пёЃ

                                                  рќ‘ќ1 +рќ‘ќ2 =рќ‘Ѓ
                                                 рќ‘ќ1 ,рќ‘ќ2 prime

   This convention matches B1, I1, G2, and G1. Using unordered pairs would only change the
normalization by a bounded factor, but the proof tree uses the ordered convention throughout.




                                                      81
G0H.2. Setup: Input from I1          I1 proves that for all sufficiently large even рќ‘Ѓ ,

                                     рќ‘…О› (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).                                         (1)
    Here S(рќ‘Ѓ ) is the singular series reconstructed in H4 from the finite local model and then used
in I1:
                                   в€ЏпёЃ рќ‘ќ в€’ 1                 в€ЏпёЃ (пё‚           1
                                                                                    )пё‚
                     S(рќ‘Ѓ ) = 2рќђ¶2               ,     рќђ¶2 =           1в€’                   > 0.
                                   рќ‘ќ|рќ‘Ѓ
                                         рќ‘ќв€’2                рќ‘ќ>2
                                                                         (рќ‘ќ в€’ 1)2
                                   рќ‘ќ>2

   The positivity of рќђ¶2 follows from convergence of рќ‘ќ>2 (рќ‘ќ в€’ 1)в€’2 .
                                                          в€‘пёЂ

   For even рќ‘Ѓ , every factor (рќ‘ќ в€’ 1)/(рќ‘ќ в€’ 2) with рќ‘ќ > 2 is > 1, hence

                                           S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 > 0.                                            (2)

G0H.3. Setup: Input from G2              G2 proves

                          рќ‘…О› (рќ‘Ѓ ) в€’ рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘‚ рќ‘Ѓ 1/2 (log рќ‘Ѓ )2 = рќ‘њ(рќ‘Ѓ ).                              (3)
                                                     (пёЂ              )пёЂ


   The support of the difference consists exactly of ordered pairs (рќ‘›1 , рќ‘›2 ) with рќ‘›1 + рќ‘›2 = рќ‘Ѓ ,
О›(рќ‘›1 )О›(рќ‘›2 ) Мё= 0, and at least one coordinate a nontrivial prime power рќ‘ќрќ‘ , рќ‘ в‰Ґ 2.
   Indeed, if both coordinates are primes, the pair is counted in рќ‘…рќ‘ќрќ‘ќ ; otherwise any nonzero О›-
contribution has at least one nontrivial prime-power coordinate.
   The elementary count is:

              #{рќ‘ќрќ‘ в‰¤ рќ‘Ѓ : рќ‘ќ prime, рќ‘ в‰Ґ 2} в‰¤ рќњ‹(рќ‘Ѓ 1/2 ) +                      рќњ‹(рќ‘Ѓ 1/рќ‘ ) в‰Є рќ‘Ѓ 1/2 .
                                                                    в€‘пёЃ

                                                               3в‰¤рќ‘в‰¤log2 рќ‘Ѓ

   For each selected nontrivial prime power, the other coordinate is determined, and the weight is
at most (log рќ‘Ѓ )2 . A union bound over the two coordinates gives (3). Double-counting pairs where
both coordinates are nontrivial prime powers is harmless because this is only an upper bound.

G0H.4. Proof: Positivity of the Genuine Prime-Pair Sum                        Combining (1) and (3),

                           рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = рќ‘…О› (рќ‘Ѓ ) + рќ‘њ(рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ).                                (4)
   By (2),

                                           S(рќ‘Ѓ )рќ‘Ѓ в‰Ґ 2рќђ¶2 рќ‘Ѓ.
    The total рќ‘њ(рќ‘Ѓ ) error in (4) is eventually bounded in absolute value by рќђ¶2 рќ‘Ѓ . Therefore, for all
sufficiently large even рќ‘Ѓ ,

                               рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) в‰Ґ 2рќђ¶2 рќ‘Ѓ в€’ рќђ¶2 рќ‘Ѓ = рќђ¶2 рќ‘Ѓ > 0.                                     (5)




                                                     82
G0H.5. Proof: Positivity Implies a Prime Representation Every summand in рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) is
nonnegative, and it is strictly positive for every actual prime pair because log рќ‘ќ > 0 for every prime
рќ‘ќ. If no prime pair рќ‘ќ1 + рќ‘ќ2 = рќ‘Ѓ existed, then рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) would be an empty sum and hence would
equal 0.
    But (5) gives рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) > 0. Hence there exists at least one ordered pair of primes (рќ‘ќ1 , рќ‘ќ2 ) such
that

                                            рќ‘Ѓ = рќ‘ќ1 + рќ‘ќ2 .
   This is exactly strong Goldbach for sufficiently large even рќ‘Ѓ .

Parameter check 17.1 (G0H.6. Parameter and Interface Checks).              1. The ordered-pair conven-
    tion is consistent across B1, I1, G2 and G1.

  2. The use of G2 is essential: positivity of рќ‘…О› (рќ‘Ѓ ) alone would not exclude the possibility that
     the mass came from prime powers, while (3) excludes this at рќ‘њ(рќ‘Ѓ ) scale.

  3. No cancellation is hidden in G2, since О›(рќ‘›) в‰Ґ 0.

  4. The lower bound S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 is uniform for even рќ‘Ѓ , so the final positivity is not vulnerable
     to the size of the prime divisors of рќ‘Ѓ .

  5. The theorem obtained is only the ledger target рќђє0: sufficiently large even рќ‘Ѓ . No finite
     verification for small even рќ‘Ѓ is included here.

Remark 17.2 (G0H.7. Output).

                        The final handoff from I1 and G2 to G0 is proved.

   I1 plus G2 gives рќ‘…рќ‘ќрќ‘ќ (рќ‘Ѓ ) = S(рќ‘Ѓ )рќ‘Ѓ + рќ‘њ(рќ‘Ѓ ). Since S(рќ‘Ѓ ) в‰Ґ 2рќђ¶2 > 0 for even рќ‘Ѓ , the genuine
prime-pair sum is positive for all sufficiently large even рќ‘Ѓ . Therefore G1 derives the existence of a
prime representation, and the root target G0 follows.

G0H.8. Logical Dependencies External dependencies: elementary positivity of the singular
series Euler product and О›(рќ‘›) в‰Ґ 0.
    Internal dependencies: I1, G2, and G1.
    Children served: G0.




                                                 83

