   GoodAWACK Finite Grammar Independent Theorem Package
                               Denis Saltykov (ds1678@gmail.com)

                                              May 2026


Contents
1 Abstract                                                                                            2

2 Introduction and Statement of Results                                                               2
  2.1 Purpose of the Package . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      2
  2.2 Package Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     2
       2.2.1 Theorem GoodAWACK-Finite-Grammar . . . . . . . . . . . . . . . . . . . .                 2
  2.3 What This Package Imports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .       2

3 Parameters, Notation, and Error Bookkeeping                                                         2

4 External Analytic Inputs                                                                            3
  4.1 Finite algebraic inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .   3
  4.2 No external analytic estimate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     3
  4.3 Reproducibility records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .     3

5 Full Proof Body                                                                                      3
  5.1 Part 1. E5: Affine transport and content stability . . . . . . . . . . . . . . . . . . . .       4
  5.2 Part 2. BGS: B1-to-GoodAWACK skeleton normal form . . . . . . . . . . . . . . . .                8
  5.3 Part 3. HGO2R: HighTC obstruction reduction . . . . . . . . . . . . . . . . . . . . .           16
  5.4 Part 4. BAOC: Affine-origin catalogue . . . . . . . . . . . . . . . . . . . . . . . . . .       21
  5.5 Part 5. E10G: Strong BAOC catalogue . . . . . . . . . . . . . . . . . . . . . . . . . .         28
  5.6 Part 6. E10H: Rigidity interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . .      36
  5.7 Part 7. E10I: Matrix-origin rigidity . . . . . . . . . . . . . . . . . . . . . . . . . . . .    43
  5.8 Part 8. E10J: Rank-dropping AFF origin verification . . . . . . . . . . . . . . . . . .         48
  5.9 Part 9. E10Y: GoodAWACK routing grammar completeness . . . . . . . . . . . . . .                53
  5.10 Part 10. E10M: No untagged rank-dropping AFF . . . . . . . . . . . . . . . . . . . .           63
  5.11 Part 11. E10X: Master finite-grammar closure . . . . . . . . . . . . . . . . . . . . . .       69
  5.12 Part 12. E10K: AFF-origin completeness . . . . . . . . . . . . . . . . . . . . . . . . .       75
  5.13 Part 13. E10L: Clean Branch B closure . . . . . . . . . . . . . . . . . . . . . . . . .        80

6 Package Dependency Ledger and Synchronization Notes                                              85
  6.1 Compact Package Dependency Graph . . . . . . . . . . . . . . . . . . . . . . . . . . 85
  6.2 Local Ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

7 Bibliography                                                                                        86

8 References                                                                                          86

                                                   1
1     Abstract
This package proves the finite combinatorial GoodAWACK grammar brick. It establishes that
every actual terminal GoodAWACK skeleton is generated by the certified B1/B3/F3/F4/E5 routing
grammar, that rank-dropping affine operations carry an allowed origin tag, and that no untagged
rank-dropping AFF residual survives into the HighTC GoodAWACK branch.


2     Introduction and Statement of Results
2.1     Purpose of the Package
The package isolates the structural, non-analytic part of the GoodAWACK closure. It does not
prove the TC1 near-global estimate; that is imported from the TNG/TC1 package. Its role is to
close the HighTC residual by a finite grammar theorem.

2.2     Package Theorem
2.2.1    Theorem GoodAWACK-Finite-Grammar
For every actual B1-origin terminal GoodAWACK skeleton, every skeleton- generating operation
belongs to the finite B1/B3/F3/F4/E5 grammar certified by E10Y. Along every such derivation,
E10X supplies a grammar invariant which forces every rank-dropping AFF operation to carry an
allowed origin tag. Therefore no untagged rank-dropping AFF occurrence survives in an actual
terminal GoodAWACK skeleton, and the HighTC FreeAffine residual is eliminated.
    Together with the imported TNG/TC1 theorem, E10L gives

                                         𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).

2.3     What This Package Imports
    1. The B1/B3/F3/F4 routing interface from the final modular assembly package.

    2. The TC1 no-rogue-short-interval theorem from the TNG/TC1 package.

    3. Edge, CKP, and local interfaces only as terminal routing destinations.


3     Parameters, Notation, and Error Bookkeeping
This package is finite and combinatorial. Its parameters are the fixed Heath–Brown depth 𝐽0 , the
finite routing grammar, and the finite list of allowed origin tags. It does not choose new analytic
exponents.
    The error bookkeeping is structural:


        Source                                          Output
        TC1 branch                                      imported 𝑜(𝑁 ) from TNG/TC1
        HighTC certified grammar                        no untagged AFF residual
        Edge/CKP/Local alternatives                     routed to corresponding theorem packages
        actual terminal GoodAWACK residual              eliminated by E10Y/E10X/E10M/E10K




                                                    2
    The local objects are:


       Object                                         Meaning in this package
       terminal GoodAWACK skeleton                    the affine skeleton remaining after the B1/B3/F3/F4
                                                      routing layer
       grammar transition                             one of the finite operations certified by E10Y
       origin tag                                     the certificate that an affine regrouping came from an
                                                      allowed B1/B3/F3/F4/E5 operation
       rank-dropping AFF                              an affine regrouping step which can lower the effective
                                                      affine rank
       HighTC residual                                the branch which would remain if an untagged rank-
                                                      dropping AFF survived




    The induction in E10X is finite. It runs over the certified derivation of a terminal skeleton,
not over scales of 𝑁 , and it does not create an infinite descent. At each transition the invariant
records either a terminal routing class or an allowed origin tag. The output form is the exclusion
of untagged rank-dropping AFF in actual terminal GoodAWACK skeletons.


4     External Analytic Inputs
This package invokes no deep external analytic theorem. It uses standard finite lattice/content
algebra through E5 and standard finite combinatorial induction on a certified routing grammar.
E10S and E10S-MECH are separate non-logical reproducibility records; the proof does not depend
on a search script or on source-file hashes.

4.1    Finite algebraic inputs
The only algebraic inputs are finite affine-form operations: fixing, projection, CRT restriction, fixed
divisor quotient, variable quotient residual, bounded affine regrouping, primitive slicing, auxiliary
inheritance, and the square-divisor routing operation recorded in F3/F4. E10Y proves that these
are exactly the skeleton-generating operations needed for actual terminal GoodAWACK atoms.

4.2    No external analytic estimate
The package does not use Gowers inverse theory, Green–Tao orthogonality, or a new higher-order
analytic estimate. The TC1 analytic subbranch is imported from TNG/TC1. The HighTC part is
closed by finite grammar completeness and rank-dropping AFF origin exclusion.

4.3    Reproducibility records
The optional E10S and E10S-MECH records make the source-maintenance check reproducible for
the maintained proof-source files. They are not logical premises of this package. The mathematical
proof of closure is the combination E10Y + E10M + E10X + E10K, not a search script.


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

    1. Lemmas/e_5_ltx.md – Affine transport and content stability

                                                  3
  2. Lemmas/b1_to_goodawack_skeleton_normal_form_ltx.md – B1-to-GoodAWACK skeleton
     normal form

  3. Lemmas/bgs_hgo2_reduction_ltx.md – HighTC obstruction reduction

  4. Lemmas/baoc_affine_origin_catalogue_ltx.md – Affine-origin catalogue

  5. Lemmas/e10g_strong_baoc_catalogue_ltx.md – Strong BAOC catalogue

  6. Lemmas/e10h_e10g_rigidity_ltx.md – Rigidity interface

  7. Lemmas/e10i_mor_matrix_origin_rigidity_ltx.md – Matrix-origin rigidity

  8. Lemmas/e10j_rda_rank_dropping_aff_origin_verification_ltx.md – Rank-dropping AFF
     origin verification

  9. Lemmas/e10y_goodawack_routing_grammar_completeness_ltx.md – GoodAWACK routing
     grammar completeness

 10. Lemmas/e10m_no_untagged_rank_dropping_aff_ltx.md – No untagged rank-dropping AFF

 11. Lemmas/e10_master_source_exhaustion_closure_ltx.md – Master finite-grammar closure

 12. Lemmas/e10k_aff_oc_affine_regrouping_origin_completeness_ltx.md – AFF-origin com-
     pleteness

 13. Lemmas/e10l_e10_clean_branch_b_ltx.md – Clean Branch B closure

5.1   Part 1. E5: Affine transport and content stability
Source file: Lemmas/e_5_ltx.md.

E5. Content Stability Lemma

E5.0. Role Logical ID: E5.
   Lemma E5 is the content-stability lemma used by Branch B / GoodAWACK. It ensures that
admissible routing, lattice restriction, quotienting, slicing, and clean affine coordinate changes do
not lose controlled content for a marked affine form.
   The phrase "affine regrouping" in this file is not an additional terminal routing operation. It
means either a full-rank affine coordinate change, or a rank-dropping map whose origin has already
been recorded by the earlier B1/B3/F3/F4 routing data as fixing/projection, quotient/divisor/local,
CKP, Edge, impossible, or post-terminal analytic slicing. E5 does not classify these origins and
does not introduce a new terminal GoodAWACK generator; it only preserves controlled content for
transports whose source is already present in the routing record.
   The output needed by the subsequent branches is that, after slicing, one obtains a form

                                           𝐿(𝑢) = 𝑔𝑢 + 𝑏
   with

                                           𝑔 ≤ (log 𝑁 )𝐶 ,
   and can then apply the TC1/X9L linear input to 𝜆(𝑔𝑢 + 𝑏).

                                                 4
   Used by: BRS, TTH, TGT, TNG, E10M, E10K, and E10L.
   Uses: F3, F4, and standard bounded-minor/content algebra.
   —

E5.1. Content on a lattice coset         Let

                                               Λ = 𝑧0 + Λ0
   be an affine lattice coset, where Λ0 ⊆ Z𝑟 is a lattice. Let

                                            𝐿(𝑧) = ℓ(𝑧) + 𝑏
   be an affine-linear form. Define the content relative to Λ by

                                   contΛ (𝐿) = gcd{ℓ(𝑣) : 𝑣 ∈ Λ0 }.
   Form 𝐿 has controlled content if

                                        contΛ (𝐿) ≤ (log 𝑁 )𝐶 .
   —

E5.2. CRT restriction
Lemma 5.1 (Lemma E5.1). Let

                                 Λ′ = {𝑧 ∈ Λ : 𝐿0 (𝑧) ≡ 𝑎        (mod 𝑞)}
   be a nonempty CRT restriction with

                                            𝑞 ≤ (log 𝑁 )𝐶 .
   Then, for every affine form 𝐿,

                                     contΛ′ (𝐿) ≤ 𝑞 𝑂(1) contΛ (𝐿).
   In particular, controlled content remains controlled.
Proof. The difference lattice Λ′0 = Λ′ − Λ′ is a sublattice of Λ0 of index at most 𝑞 𝑂(1) . If

                                             ℓ(Λ0 ) = 𝑔Z,
   then ℓ(Λ0 ) is a sublattice of 𝑔Z of index at most 𝑞 𝑂(1) . Hence
           ′


                                               ℓ(Λ′0 ) = 𝑔 ′ Z
   with

                                               𝑔 ′ ≤ 𝑞 𝑂(1) 𝑔.
   Thus

                                     contΛ′ (𝐿) ≤ 𝑞 𝑂(1) contΛ (𝐿).
   Since \{}(q\{}le( \{}log N)ˆC\{}), the new content remains polylogarithmic. Lemma proved.
   —


                                                     5
E5.3. Fixed divisor absorption          Suppose an atom is restricted by

                                                 𝑑 | 𝐿(𝑧),
   where 𝑑 is fixed on the atom. Define

                     Λ𝑑 = {𝑧 ∈ Λ : 𝐿(𝑧) ≡ 0       (mod 𝑑)},        𝐿𝑑 (𝑧) = 𝐿(𝑧)/𝑑.

Lemma 5.2 (Lemma E5.2). If

                                             𝑔 = contΛ (𝐿),
   then
                                                          𝑔
                                       contΛ𝑑 (𝐿𝑑 ) =          ≤ 𝑔.
                                                        (𝑔, 𝑑)
Proof. On the difference lattice,

                                              ℓ(Λ0 ) = 𝑔Z.
   The restricted difference lattice satisfies

                                    ℓ(Λ𝑑,0 ) = 𝑔Z ∩ 𝑑Z = lcm(𝑔, 𝑑)Z.
   After dividing the form by 𝑑, the image lattice is
                                        1                𝑔
                                          lcm(𝑔, 𝑑)Z =        Z.
                                        𝑑              (𝑔, 𝑑)
   This proves the formula. Lemma proved.
   —


E5.4. Primitive slicing      Primitive slicing chooses coordinates on a lattice coset so that a marked
affine form becomes

                                             𝐿(𝑧) = 𝑔𝑢 + 𝑏
    on a one-dimensional fibre. The coefficient 𝑔 is precisely the content of the linear part on the
fibre lattice. Therefore, if

                                         contΛ (𝐿) ≤ (log 𝑁 )𝐶 ,
   then

                                             𝑔 ≤ (log 𝑁 )𝐶 .
   If the resulting fibre is short, the atom is routed to Edge/Local by F3/C1. If the fibre is long,
the form 𝑔𝑢 + 𝑏 is admissible for the active TC1/X9L linear input.
   —




                                                    6
                                                                 ′
E5.5. Affine changes and regrouping Let 𝑇 : Z𝑟 → Z𝑟 be an integer affine map with
coefficients and relevant minors bounded by powers of log 𝑁 . For

                                           𝐿′ (𝑥) = 𝐿(𝑇 𝑥),
   we have

                                    cont(𝐿′ ) ≤ (log 𝑁 )𝐶 cont(𝐿).
    If 𝑇 is unimodular or full-rank on the active affine span, content is preserved exactly or changes
only by the bounded-minor factor already displayed above. Thus clean bounded affine regrouping
preserves controlled content.
    If 𝑇 is rank-dropping, it is allowed in the proof tree only when the rank drop carries an explicit
origin tag already produced by the earlier routing record. Such a map is not a free terminal-vector
generator; it is either routed by B1/B3/F3/F4 data or used only as a post-terminal analytic slicing
operation after the terminal affine system has been fixed.

E5.5A. Clean full-rank criterion        Let

                                  𝑈ℒ = spanQ {ℓ𝑖 − ℓ𝑗 : 𝐿𝑖 , 𝐿𝑗 ∈ ℒ}
   be the active affine difference span on the current routing cell, and let

                                    𝑈TC = spanQ {ℓ𝜌 : 𝜌 ∈ ℒterm }
   be the terminal tensor-test vector span when the terminal GoodAWACK object has already
been fixed. An affine transport 𝑇 is E5-clean full-rank only if the linear part 𝑇lin satisfies

                                           ker(𝑇lin |𝑈ℒ ) = 0
   and, in the terminal GoodAWACK setting,

                                          ker(𝑇lin |𝑈TC ) = 0.
   If either kernel is nontrivial, the transport is not clean full-rank. It may then be used only if
the lost rank has already been produced and recorded by one of the routing origins

             Fix/Proj,    CRT,    FixedDiv,      VarQuot,        LocalDiag,   CKP,   Edge,
    or if the operation is post-terminal analytic slicing which does not replace the terminal tensor-
test vectors. Thus E5 never promotes a rank-dropping map to an independent terminal GoodAWACK
generator.
    —

E5.6. Cauchy and cube operations              Cauchy–Schwarz and cube operations introduce shifted
forms such as

                                     𝐿(𝑧 + 𝜔ℎ) = 𝐿(𝑧) + ℓ(𝜔ℎ).
   The linear part remains ℓ. Therefore

                                    cont(𝐿(𝑧 + 𝜔ℎ)) = cont(𝐿).

                                                   7
   If a cube operation produces equality, proportionality, or forced local dependence between forms,
the atom is routed to LocalDiag by F3. Otherwise at least one marked controlled-content form
survives.
   —

E5.7. Lemma E5

Lemma 5.3 (Lemma E5). Let 𝒜 be a Branch B atom with a marked affine form 𝐿* satisfying

                                       contΛ (𝐿* ) ≤ (log 𝑁 )𝐶 .
   Under any finite sequence of allowed F3 operations:


CRT,    fixed divisor absorption,   primitive slicing,   clean affine regrouping,   Cauchy/cube,    local diagonal ex

   one of the following holds:

  1. the atom becomes terminal LocalDiag;

  2. the atom is routed to Edge or CKP;

  3. the resulting Branch B atom still has a marked affine form of controlled content.

Proof. CRT restrictions increase content by at most a polylogarithmic factor by Lemma E5.1. Fixed
divisor absorption does not increase quotient content by Lemma E5.2. Primitive slicing writes the
form as 𝑔𝑢 + 𝑏 with controlled 𝑔. Clean bounded affine changes and regrouping multiply content by
at most a polylogarithmic factor. If a rank drop occurs, E5 requires that its origin tag is already
present in the routing record as fixing/projection, quotient/divisor/local, CKP, Edge, impossible,
or post-terminal analytic slicing; E5 itself does not create the tag. Cauchy/cube shifts preserve the
linear part and hence preserve content. If any operation creates forced local dependence, F3 routes
the atom to LocalDiag. Therefore every nonterminal Branch B descendant retains a controlled-
content marked form. Lemma proved.
    —


Remark 5.4 (E5.8. Output).

Controlled content is stable under the allowed E5 operations, with the clean routing-record interpretation of affin

    Thus Branch B descendants that are not routed to LocalDiag, Edge, or CKP retain a marked
affine form of controlled content.

E5.9. Logical Dependencies Internal dependencies: F3, F4, and standard bounded-minor/content
algebra.
    Internal nodes served: BRS, TTH, TGT, TNG, E10Y, E10M, E10K, and E10L.

5.2    Part 2. BGS: B1-to-GoodAWACK skeleton normal form
Source file: Lemmas/b1_to_goodawack_skeleton_normal_form_ltx.md.


                                                  8
BGS. Skeleton Normal Form for Terminal GoodAWACK Descendants

BGS.0. Statement and Role The skeleton record below is an intrinsic B1/B3/F3/F4/E5
normal form. It records B3 product groupings, full-rank coordinate changes, and rank drops with
explicit fixing/projection, quotient/divisor/local, CKP, Edge, impossible, or post-terminal analytic
origin tags. It does not obtain its meaning from E10L. The later E10Y/E10M/E10K/E10X finite-
grammar layer consumes this record to exclude untagged rank-dropping affine regrouping as a
terminal-vector generator.
    Lemma BGS extracts the normal form for terminal GoodAWACK atoms generated by the
B1/B3/F3/F4 routing interface.
    The purpose is to prepare the finite structural theorem HGO.2:

                     HighTC-cert =⇒ CKP ⊔ LocalDiag ⊔ Edge ⊔ Impossible.
   The output is a finite parameterized skeleton normal form that records:

  1. the parent B1 product block;

  2. the B3 grouping choice;

  3. the F3/F4 routing history;

  4. the active affine forms that survive into terminal GoodAWACK;

  5. the origin of each affine form;

  6. the exact tensor test needed for TC1/HighTC.

    This is the object used downstream by the E10Y/E10X/E10K/E10L finite-grammar and clean-
interface arguments.
    Logical dependencies: B1, B3, F3, F4, and E5. Outputs served: HGO2R, BAOC, E10Y, E10K,
E10L, and E10X.
    —

BGS.1. B1 parent block         Every terminal GoodAWACK atom has a parent typed B1 block

                                         ℬ = (𝑟, 𝑠, X, Y, t),
   where:

  1. 𝑟, 𝑠 ≤ 2𝐽0 ;

  2. X, Y are dyadic scale vectors;

  3. t records elementary coefficient types


                                       𝜇 · 1≤𝑦 ,       1,   log;

  1. the parent equation is



                                                   9
                                         𝑃𝐴 (𝑎) + 𝑃𝐵 (𝑏) = 𝑁,                                  (B1)
   with
                                            𝑟                             𝑠
                                𝑃𝐴 (𝑎) =                     𝑃𝐵 (𝑏) =
                                           ∏︁                            ∏︁
                                                 𝑎𝑖 ,                           𝑏𝑗 .
                                           𝑖=1                           𝑗=1

   The parent variable set is

                                   𝒳ℬ = {𝑎1 , . . . , 𝑎𝑟 , 𝑏1 , . . . , 𝑏𝑠 }.
   All later descendants keep the parent B1 tag. This is required by H4 and by the clean F3/F4
routing interface.
   —

BGS.2. B3 grouping skeleton          A B3 grouping skeleton is a finite partition of selected parent
variables into grouped factors:

                                   𝑢𝜈 =                      𝑣𝜈 =
                                            ∏︁                      ∏︁
                                                  𝑥,                       𝑥,
                                           𝑥∈𝐼𝜈                     𝑥∈𝐽𝜈

   and similarly on both sides of (B1).
   The grouping skeleton records:

  1. which grouped factors are short, long, or central;

  2. whether a balanced bilinear grouping is exposed;

  3. whether a local AP configuration is exposed;

  4. whether a forced local dependence/collision is exposed;

  5. which residual grouped variables remain available for BranchB/GoodAWACK.

   By Lemma B3, the set of possible grouping skeletons is finite:

                                            |𝒢(ℬ)| ≤ 𝐶(𝐽0 ).
    Only grouping skeletons that are not terminal Edge, CKP, LongAP/Local, or LocalDiag can
feed the GoodAWACK skeleton.
    —

BGS.3. F3/F4 routing skeleton Starting from a B1 block and a B3 grouping skeleton, F3/F4
perform only finitely many routing-level operations before terminality.
   For a terminal GoodAWACK descendant, the routing skeleton records the following data:

                                  r = (rCRT , rdiv , rquot , rgrp , rfail ).
   Here:

  1. rCRT records controlled CRT/congruence restrictions;


                                                        10
  2. rdiv records fixed divisor absorptions;

  3. rquot records variable quotient equations 𝐿(𝑧) = 𝑑𝑠 that were resolved without becoming
     Edge, LocalDiag, or CKP;

  4. rgrp records B3 product groupings, full-rank affine changes of variables, and only E10Y/E10M/E10L-
     tagged rank-dropping maps;

  5. rfail records failed terminal alternatives that were checked and eliminated.

   The GoodAWACK routing condition is:

                    ¬Edge,      ¬CKP,          ¬LongAP/Local,       ¬LocalDiag,              (G0)
   together with:

  1. no unresolved ordinary large-divisor predicate;

  2. central-long affine/WACLE residual structure;

  3. controlled content;

  4. at least one marked Liouville-type affine form.

   The important limitation is that the F3/F4 routing skeleton does not include the quadratic
tensor test
                                         ?
                                     𝑄𝑚 ∈ spanQ {𝑄𝑖 : 𝑖 ̸= 𝑚}.
   That test is added only at the TC1/HighTC dichotomy stage.
   —

BGS.4. Setup: Active Parameter Lattice After applying the F3/F4 routing skeleton, a
terminal GoodAWACK descendant is supported on a bounded-rank lattice coset

                                     𝑧 ∈ ΩS ⊂ 𝑧* + ΛS ⊂ Z𝑘S ,
   where:

  1. 𝑘S ≤ 𝐾(𝐽0 );

  2. ΩS is a smooth box-like region;

  3. every active long direction has length at least 𝑁 𝜃 , up to C1-routed boundary/short-volume
     exceptions;

  4. the lattice index and all contents are bounded by a power of log 𝑁 .

   We write the active parameter vector as

                                         𝑧 = (𝑧1 , . . . , 𝑧𝑘S ).
   The affine transformations from the parent variables to 𝑧 are recorded by an origin map


                                                   11
                                                    origS .
    This map is part of the skeleton. It is needed to decide whether a later algebraic relation
corresponds to CKP, genuine LocalDiag, Edge, or an impossible parent configuration.
    —

BGS.5. Setup: Active Affine Forms                The terminal GoodAWACK descendant has a finite
active affine system

                                       ℒS = {𝐿𝜌 (𝑧) : 𝜌 ∈ ℐS },
   where

                           𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 ,          ℓ𝜌 ∈ Z𝑘S ,    𝑐𝜌 ∈ Z,
   after clearing the controlled lattice denominator.
   Each 𝐿𝜌 has one of the following origins:

Type A. Parent coordinate / grouped factor

                                                    𝐿𝜌 (𝑧)

   is the affine representative of a surviving parent variable or grouped factor after CRT restriction
and affine change of variables.

Type B. Fixed divisor quotient          A controlled divisor relation

                                     𝑑 | 𝐿(𝑧),         𝑑 ≤ (log 𝑁 )𝐶 ,
   has been absorbed on a lattice coset, producing

                                            𝐿𝜌 (𝑧) = 𝐿(𝑧)/𝑑
   as an integer affine form on the restricted lattice.

Type C. Variable quotient residual           A quotient equation

                                                 𝐿(𝑧) = 𝑑𝑠
   has been resolved without short-volume Edge, without forced local dependence, and without
balanced CKP structure. The quotient variable 𝑠 survives as an affine form

                                             𝐿𝜌 (𝑧) = 𝑠(𝑧).

Type D. Primitive slice / fibre form           After primitive slicing, a marked form may be written
on a fibre as

                              𝐿𝜌 (𝑧0 + 𝑢𝑣) = 𝑔𝑢 + 𝑏,            𝑔 ≤ (log 𝑁 )𝐶 .
   This is used analytically in E7/E10, but the pre-slicing form remains in ℒS for the tensor test.


                                                      12
Type E. Auxiliary bounded affine factor                  An auxiliary divisor-bounded or smooth coefficient
factor depends on

                                                     𝐿𝜌 (𝑧)
   and is treated analytically as 𝑓𝜌 (𝐿𝜌 (𝑧)).
   Thus the terminal atom has model form

                           AS =           𝑊S (𝑧)          𝜆𝜌 (𝐿𝜌 (𝑧))          𝑓𝜌 (𝐿𝜌 (𝑧)),         (BGS)
                                   ∑︁               ∏︁                  ∏︁

                                   𝑧∈ΩS            𝜌∈ℳS                 𝜌∈𝒰S

   where ℳS ̸= ∅ is the set of marked Liouville-type forms and 𝒰S ⊆ ℐS is the set of auxiliary
bounded/smooth coefficient forms. In the E10 proof one marked form is selected and denoted 𝐿0 .
   All active forms satisfy

                                            cont(𝐿𝜌 ) ≤ (log 𝑁 )𝐶 .
   —

BGS.6. Definition: Skeleton Normal Form

Definition 5.5 (Definition. B1-to-GoodAWACK skeleton). A B1-to-GoodAWACK skeleton is a
tuple

                              S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S ),
   where:

  1. ℬ is a B1 parent block;

  2. Γ ∈ 𝒢(ℬ) is a B3 grouping skeleton;

  3. r is the F3/F4 routing skeleton;

  4. ΛS is the active lattice/coset data;

  5. ΩS is the smooth central-long domain;

  6. ℒS is the active affine system;

  7. ℳS ⊆ ℒS is the nonempty marked Liouville-form set;

  8. origS records the B1/F3/F4 origin of each affine form;

  9. 𝒲S records dyadic weights and coefficient types.

   It is admissible if:

                          ¬Edge,     ¬CKP,         ¬LongAP/Local,            ¬LocalDiag,          (Admiss)
   and the terminal GoodAWACK predicate of Lemma F3 holds.
   —




                                                         13
BGS.7. Lemma: terminal GoodAWACK atoms admit skeleton normal form

Lemma 5.6 (Lemma BGS.1). Every tagged terminal GoodAWACK atom produced by the chain

                                      𝐵1 → 𝐵3 → 𝐹 3/𝐹 4
   admits an admissible B1-to-GoodAWACK skeleton normal form S, and can be written as (BGS).

Proof. Start with the parent B1 block. By Lemma B1, it has the product equation (B1), finitely
many variables, dyadic weights, and coefficient types 𝜇, 1, and log.
    By Lemma B3, the block receives a finite set of grouping alternatives. Choose the grouping
history that leads to the given terminal descendant. This supplies Γ.
    By Lemma F3, every routing step is one of the allowed finite routing-level operations: con-
trolled CRT absorption, F4 large-divisor decision, square-divisor routing, finite grouping selec-
tion/elimination, LocalDiag detection, or strict Edge detection. Since the atom is terminal GoodAWACK,
all Edge, CKP, LongAP/Local, and LocalDiag outcomes have been checked and eliminated for this
descendant, and no unresolved ordinary large divisor predicate remains.
    By Lemma F4, any ordinary large divisor or quotient equation that survives without becoming
Edge, LocalDiag, or CKP is absorbed into a central-long affine residual with controlled content.
The content quotient lemma ensures that the quotient forms remain controlled on the active lattice.
    By Lemma E5, controlled content is stable under CRT restriction, fixed divisor absorption,
primitive slicing, clean full-rank affine regrouping, and Cauchy/cube operations. Therefore the
active forms that reach E10 are affine forms of controlled content, and every rank-changing operation
appearing in the skeleton record carries one of the explicit routing tags listed above.
    Finally, by the terminal GoodAWACK predicate in the F3/F4 interface, at least one active
affine form carries a Liouville-type oscillatory coefficient, the active directions are long, and the
atom has the model form (BGS).
    Collecting the parent block, grouping, routing history, active lattice, affine system, marked
forms, origin map and weights gives S. Lemma proved.
    —


BGS.8. Setup: Tensor Interface on a Skeleton             For each active affine form

                                       𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 ,
   define

                                  𝑄𝜌 = ℓ𝜌 ⊙ ℓ𝜌 ∈ Sym2 (Q𝑘S ).
   The TC1/HighTC test on the skeleton is:

                             ∃𝑚 ∈ ℳS         / spanQ {𝑄𝜌 : 𝜌 ̸= 𝑚}
                                          𝑄𝑚 ∈                                            (TC1-Skel)
   for TC1, and

                             ∀𝑚 ∈ ℳS      𝑄𝑚 ∈ spanQ {𝑄𝜌 : 𝜌 ̸= 𝑚}                     (HighTC-Skel)
   for HighTC.
   Equivalently, HighTC supplies for each marked 𝑚 a relation



                                                14
                                             𝑐𝜌 𝑄𝜌 = 0,      𝑐𝑚 ̸= 0.                            (H-cert)
                                       ∑︁

                                      𝜌∈ℐS

   Because 𝑘S and |ℐS | are bounded in terms of 𝐽0 , this is a bounded-size rational row-reduction
problem for each fixed skeleton.
   —

BGS.9. Output: What This Normal Form Resolves                           The skeleton normal form resolves
three issues needed before HGO.2:

  1. it separates the parent product equation from the terminal affine system;

  2. it records the origin of each affine form, so a HighTC certificate can be tested for CKP/LocalDiag/Edge
     meaning rather than treated as a bare linear-algebra relation;

  3. it makes clear that HighTC testing is finite and terminal, hence it does not create a new
     routing loop.

   In particular:

                                                    HighTC
   is now a certificate attached to a concrete skeleton

                                                      S,
   not an undefined terminal branch.
   —

BGS.10. Scope Boundary and Structural Closure Lemma BGS proves the skeleton normal
form. It does not by itself prove that all HighTC certificates reroute to CKP, LocalDiag, Edge, or
Impossible. That structural conclusion is supplied by HGO2R, E10M, E10K, and E10L.
    The reason is that the BGS normal form records the finite-parametric grammar of admissible
skeletons, rather than a literal list of all symbolic skeleton instances. It proves that the skeleton
set is finite for fixed 𝐽0 , but it does not by itself list:

  1. all possible affine coefficient vectors ℓ𝜌 ;

  2. all possible quotient-origin maps;

  3. all symbolic dependencies among the ℓ𝜌 ;

  4. all conditions under which a HighTC certificate forces CKP, LocalDiag, Edge, or impossibility.

   Moreover, some skeleton entries may depend on controlled divisor/CRT parameters. These
parameters are polylogarithmically bounded in size, but for structural proof they must be treated
symbolically, not by numerical enumeration.
   Thus the output of BGS is the finite-parametric input for the subsequent finite-grammar theo-
rem.
   —


                                                      15
BGS.11. Structural Use

Theorem 5.7 (Theorem BGS/HGO.2). For every admissible B1-to-GoodAWACK skeleton S, if
S has a HighTC certificate (H-cert), then one of the following holds:

  1. the origin map origS exposes an admissible balanced bilinear grouping, so the atom is CKP;

  2. the certificate forces equality, proportionality, fixed gcd-local dependence, or an H4-admissible
     canonical local projection, so the atom is LocalDiag;

  3. the certificate forces short residual volume, large content/gcd, or another strict C1 saving
     predicate, so the atom is Edge;

  4. the certificate is incompatible with the parent product equation (B1), the dyadic central-long
     constraints, and the routing history r.

   This theorem is supplied by the HGO2R/E10 closure chain. Once it is combined with the BGS
normal form, one obtains:

                                    𝑅HighTC-GoodAWACK (𝑁 ) = 0
    after rerouting, and Branch B closes using the already proved TC1 Fourier lemma.
    The role of Lemma BGS is to make the statement finite and symbolic; the exclusion of untagged
free-affine HighTC skeletons is handled by E10Y/E10X/E10K.
    —

BGS.12. Output for the Proof Tree

                         B1-to-GoodAWACK skeleton normal form proved.

   The normal form is:

                            S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   with terminal atom model (BGS).
   This is sufficient to formulate HGO.2 precisely as a finite-parametric skeleton theorem and to
pass the problem to HGO2R/E10Y/E10X/E10K/E10L.

BGS.13. Logical dependencies Internal dependencies: B1, B3, F3, F4, and E5.
  Children served: HGO2R, E10M, E10K, E10L.

5.3   Part 3. HGO2R: HighTC obstruction reduction
Source file: Lemmas/bgs_hgo2_reduction_ltx.md.

HGO2R. Reduction of BGS/HGO.2 to Free-Affine HighTC Exclusion




                                                 16
HGO2R.0. Statement and Role Lemma HGO2R proves the origin-degenerate rerouting state-
ment HGO2R.1. The free-affine class is treated by the finite-grammar closure theorems E10Y,
E10M, E10X, E10K, and E10L.
   The structural block is:

                     HighTC-cert =⇒ CKP ⊔ LocalDiag ⊔ Edge ⊔ Impossible                       (HGO.2)
   for admissible B1-to-GoodAWACK skeletons in the sense of Lemma BGS.
   The BGS/HGO2R part proves this implication for HighTC certificates whose quadratic depen-
dence is visible through the recorded origin map. The remaining free-affine case is delegated to
E10Y/E10X/E10K.
   The reduction statement is:


     HGO.2 reduces to excluding FreeAffine-HighTC skeletons from actual B1 descendants.

   Thus HGO2R is a reduction theorem with an explicit structural-closure dependency.
   Logical dependencies: BGS, C1, the CKP branch, the H4 LocalDiag admission criterion, E10Y,
E10X, E10K, and E10L. Outputs served: E10M, E10K, and E10L.
   —

HGO2R.1. Setup: Starting Point             Let

                            S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   be an admissible B1-to-GoodAWACK skeleton.
   Write

                              𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 ,       𝑄𝜌 = ℓ𝜌 ⊙ ℓ𝜌 .
   Assume that S is HighTC. Then for every marked form 𝑚 ∈ ℳS there is an integer relation

                                           𝑐𝜌 𝑄𝜌 = 0,       𝑐𝑚 ̸= 0.                           (H-cert)
                                    ∑︁

                                    𝜌∈ℐS

   The question is whether (H-cert), together with the origin map origS , forces terminal rerouting.
   —

HGO2R.2. Setup: Degenerate-Origin Certificates Call a HighTC certificate origin-degenerate
if at least one of the following is forced by the support of the relation and the origin data of the
participating forms.

D1. Repeated or proportional affine origin              There are 𝜌 ̸= 𝜎 in the support of (H-cert) such
that the current lattice forces

                                             𝐿𝜌 = 𝑎𝐿𝜎 + 𝑏
    with fixed rational 𝑎, 𝑏, or the corresponding parent/product factors are repeated after quoti-
enting.




                                                  17
D2. Fixed gcd-local dependence The forms in the support of (H-cert) are tied by a fixed
divisor/gcd relation recorded in rdiv or rquot , so that one active form is determined by another on
a fixed local residue class.

D3. Balanced multiplicative origin The support of (H-cert) splits through origS into two
long grouped multiplicative variables on each side of the parent B1 equation, with the B3 balance
predicates required by Lemmas B3 and F3.

D4. Strict saving origin The certificate forces one of the strict C1 predicates: short resid-
ual volume, large gcd/content budget, square-divisor budget, Type-I error budget, high-frequency
budget, or small-conductor budget with the full ambient normalization.

D5. Parent incompatibility The certificate forces a linear or congruence relation incompatible
with the parent B1 product equation, the dyadic scale cell, or the current CRT lattice. Then the
skeleton has empty support.
    The complementary case is called free-affine:

                                       FreeAffineHighTC(S)
   if (H-cert) holds but none of D1–D5 is forced by the current recorded origins.
   —

HGO2R.3. Lemma: origin-degenerate HGO.2
Lemma 5.8 (Lemma HGO2R.1). Let S be an admissible B1-to-GoodAWACK skeleton with a
HighTC certificate. If the certificate is origin-degenerate, then the corresponding terminal atom
reroutes to one of:

                         CKP,       LocalDiag,        Edge,     Impossible.
Proof. We use the cases D1–D5.
    In case D1, the current atom contains a forced equality, proportionality, or repeated factor after
quotienting. This is exactly within the terminal LocalDiag predicate of Lemma F3, provided the
resulting contribution is a canonical local term. The LPI admission condition consumed by H4 is
satisfied because the relation is tagged by the parent B1 block and routing history. Hence the atom
is LocalDiag.
    In case D2, the fixed gcd/divisor data determine one active form from another on the current
lattice. This is the fixed local dependence case of Lemmas F3 and F4. Again the term is admitted
only as a tagged canonical local projection, so it is LocalDiag rather than an arbitrary local-looking
term.
    In case D3, the origin map exposes a balanced finite-convolution bilinear structure. By the B3
CKP candidate criterion and the F3 CKP terminal predicate, this is a CKP atom. The coefficient
and content conditions are preserved by Lemmas F4 and E5. The CKP estimate and canonical
zero-frequency normalization are handled by Lemma G8a.
    In case D4, the certificate forces one of the strict C1 saving predicates. By Lemma C1, ordinary
large-divisor or small-conductor labels alone are not enough; but D4 assumes the full strict budget.
Therefore the atom is terminal Edge and contributes 𝑜(𝑁 ).
    In case D5, the active lattice/domain is empty, or the putative skeleton is incompatible with
the tagged B1 block. The contribution is zero. It can be recorded as Edge-zero or Impossible.

                                                 18
   These cases cover all origin-degenerate certificates. Lemma proved.
   —


HGO2R.4. Scope Boundary The origin-degenerate lemma leaves open the case where the
quadratic tensor relation is a genuine higher-true-complexity relation among distinct primitive
affine forms, with no forced local dependence, no balanced multiplicative origin, no strict saving
predicate, and no parent incompatibility visible from the recorded origin data.
    This is a genuine structural boundary of HGO2R. There is a standard model.
    Let

      𝐿0 (𝑥, 𝑟) = 𝑥,     𝐿1 (𝑥, 𝑟) = 𝑥 + 𝑟,       𝐿2 (𝑥, 𝑟) = 𝑥 + 2𝑟,    𝐿3 (𝑥, 𝑟) = 𝑥 + 3𝑟.       (4AP)
   The homogeneous coefficient vectors are

                                     ℓ𝑖 = (1, 𝑖) ∈ Z2 ,    0 ≤ 𝑖 ≤ 3.
   Their quadratic tensors satisfy

                                       𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.                                (4AP-cert)
   Indeed, this is the system

                  1 − 3 + 3 − 1 = 0,       0 − 3 + 6 − 3 = 0,       0 − 3 + 12 − 9 = 0
   for the (𝑥2 , 𝑥𝑟, 𝑟2 ) tensor coordinates.
   Thus if any 𝐿𝑖 is a marked Liouville-type form, the marked tensor lies in the span of the others.
The skeleton is HighTC.
   But the 4AP pattern has:
  1. no equality or proportionality among the forms;
  2. no fixed gcd-local dependence;
  3. no balanced CKP bilinear multiplicative structure;
  4. no short-volume or large-content saving by itself;
  5. no contradiction with being central-long affine.
   Therefore, under the safe F3/H4 interpretation of LocalDiag as a genuine canonical local term,
the relation (4AP-cert) is not a LocalDiag certificate.
   There is a related linear dependence

                                       𝐿0 − 3𝐿1 + 3𝐿2 − 𝐿3 = 0.
   If the broad B3 phrase "affine dependence among active forms" were read literally as automatic
LocalDiag, this pattern would be routed away. That reading is not part of the proof: Lemma H4
admits LocalDiag only when the term is a tagged canonical local projection, not merely because
an affine identity exists among oscillatory forms. Thus 4AP-like free-affine patterns cannot be
dismissed by the broad B3 phrase unless an additional canonical-local admission proof is supplied.
   This is exactly the interface true-complexity obstruction isolated by the GoodAWACK TC1/HighTC
analysis.
   —

                                                     19
HGO2R.5. Interface Example: Formal Free-Affine Skeleton The BGS normal form is
broad enough to allow the following formal skeleton unless the B1-origin exclusion lemma is used.
   Let the active lattice be a two-dimensional central-long box

                      Ω = {(𝑥, 𝑟) : 𝑥 ≍ 𝑋, 𝑟 ≍ 𝑅, 𝑥 + 3𝑟 ≍ 𝑋, 𝑋, 𝑅 ≥ 𝑁 𝜃 }.
   Let

                           ℒ = {𝑥, 𝑥 + 𝑟, 𝑥 + 2𝑟, 𝑥 + 3𝑟},    ℳ = {𝑥}.
   Let the remaining three forms be auxiliary bounded coefficient forms, and let the weight be
smooth and divisor-bounded. All affine contents are 1.
   This formal skeleton satisfies the explicit GoodAWACK-style features:

  1. central-long affine structure;

  2. bounded affine complexity;

  3. at least one marked Liouville-type form;

  4. controlled content;

  5. no unresolved ordinary large divisor predicate;

  6. no strict Edge predicate;

  7. no CKP-balanced multiplicative form;

  8. no H4-admissible LocalDiag relation.

    It is HighTC by (4AP-cert).
    Lemma HGO2R is the origin-degenerate part of the HGO.2 route. The formal skeleton above
is the free-affine class isolated by the interface. That class is routed to E10Y/E10X/E10K, which
supply the actual-origin exclusion needed to complete full HGO.2 for terminal GoodAWACK de-
scendants.
    —

HGO2R.6. Free-Affine Exclusion Full HGO.2 is equivalent, over the origin-degenerate lemma
proved here, to the following finite structural exclusion.

Lemma 5.9 (Lemma HGO2R.2. No free-affine HighTC skeletons). For every admissible B1-to-
GoodAWACK skeleton S produced by the chain

                                       𝐵1 → 𝐵3 → 𝐹 3/𝐹 4,
   every HighTC certificate is origin-degenerate in the sense of Section HGO2R.2.
   Equivalently:

            FreeAffineHighTC(S)       never occurs for actual B1 descendants.          (NoFAH)
   This exclusion is supplied by E10Y/E10X/E10K.
   —


                                                 20
HGO2R.7. Consequence for E10            The E10 decomposition after the TC1 Fourier closure is:

               𝑅GoodAWACK (𝑁 ) = 𝑅TC1-GoodAWACK (𝑁 ) + 𝑅HighTC-GoodAWACK (𝑁 ),
   with

                                  𝑅TC1-GoodAWACK (𝑁 ) = 𝑜(𝑁 ).
   By Lemma HGO2R.1, the origin-degenerate part of HighTC reroutes to already handled branches:

                    𝑅HighTC,deg (𝑁 ) ⊆ CKP ⊔ LocalDiag ⊔ Edge ⊔ Impossible.
   Thus the only obstruction left by HGO2R alone is

                                       𝑅FreeAffineHighTC (𝑁 ).
    This class is empty by E10Y/E10X/E10K, so HGO2R supplies the origin-degenerate HighTC
rerouting component of Branch B.
    —

HGO2R.8. Output for the Proof Tree

          Origin-degenerate HighTC reroutes to CKP, LocalDiag, Edge, or Impossible.

   The NoFAH/free-affine class is closed by E10X and E10K.
   What is proved here:

              OriginDegenerateHighTC =⇒ CKP ⊔ LocalDiag ⊔ Edge ⊔ Impossible.
    The surviving free-affine class is not a terminal output of Branch B; it is passed to the down-
stream E10Y/E10X/E10K/E10L finite-grammar layer.

HGO2R.9. Logical dependencies Internal dependencies: BGS, C1, CKP branch, Local-
Diag/LPI routing, and the F3/F4 terminal routing interface.
   Children served: E10M, E10K, E10L.

5.4   Part 4. BAOC: Affine-origin catalogue
Source file: Lemmas/baoc_affine_origin_catalogue_ltx.md.

BAOC. B1 Affine-Origin Catalogue

BAOC.0. Statement and Role Lemma BAOC supplies the B1/B3/F3/F4 transport cata-
logue for homogeneous coefficient vectors in terminal GoodAWACK skeletons. It is a provenance
grammar, not the final no-free-affine theorem. The decisive exclusion of untagged rank-dropping
AFF is supplied by E10Y, E10X, E10M, E10K, and E10L.
   The statement is:


every terminal GoodAWACK affine form is generated by a finite B1/B3/F3/F4 transport grammar.


                                                 21
     More precisely, for every terminal GoodAWACK skeleton S and every active affine form 𝐿𝜌 (𝑧) =
ℓ𝜌 ·𝑧+𝑐𝜌 , the vector ℓ𝜌 is obtained from B1/B3 grouped coordinates by finitely many of the transport
rules T1–T7 below.
     BAOC also records the scope boundary of this catalogue: provenance alone does not decide
every true-complexity relation among the ℓ𝜌 . The free-affine class isolated by that boundary is
routed to E10Y/E10X/E10K/E10L.
     Logical dependencies: B1, B3, F3, F4, E5, BGS, HGO2R, E10Y, E10X, E10M, E10K, and
E10L. Outputs served: HGO2R, E10Y, E10M, E10K, E10L, and E10X.
     —

BAOC.0a. Setup: What F4 Already Proves Lemma F4 already proves the core ordinary-
divisor part of BAOC.
    In F4.1, every ordinary large-divisor predicate has one of the forms

                         𝑑 | 𝐿(𝑧),     𝐿(𝑧) = 𝑑𝑠,        𝑑 | gcd(𝐿1 (𝑧), 𝐿2 (𝑧)),
   where 𝐿, 𝐿1 , 𝐿2 are affine or product-grouped forms already produced by B1/B3.
   F4.3 records fixed-divisor absorption:

                     Λ𝑑 = {𝑧 ∈ Λ : 𝐿(𝑧) ≡ 0      (mod 𝑑)},         𝐿𝑑 (𝑧) = 𝐿(𝑧)/𝑑.
   F4.4 proves the content quotient formula
                                                          𝑔
                                      contΛ𝑑 (𝐿/𝑑) =           ≤ 𝑔.
                                                        (𝑔, 𝑑)
   F4.5–F4.11 handle the variable quotient equation

                                               𝐿(𝑧) = 𝑑𝑠
   and prove the exhaustive alternative:

              OrdinaryLargeDivisor =⇒ Edge ⊔ LocalDiag ⊔ CKP ⊔ GoodAWACK,
     or else the corrected F3 measure strictly decreases.
     Thus the BAOC transport rules T3 and T4 below are not new results. They are F4 translated
into homogeneous-vector bookkeeping.
     What F4 does not do is decide every terminal true-complexity relation among the final active
list of vectors {ℓ𝜌 }. That structural decision is made by E10Y/E10X/E10K/E10L.
     —

BAOC.1. Setup: Coefficient-Vector Bookkeeping                     Let a terminal GoodAWACK skeleton
be

                             S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S ).
   Every active affine form is written on the active parameter lattice as

                                         𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 .
   BAOC must catalogue the homogeneous vectors



                                                   22
                                                     ℓ𝜌 ∈ Z𝑘S
   with enough origin data to decide whether a quadratic tensor relation

                                                    𝑐𝜌 (ℓ𝜌 ⊙ ℓ𝜌 ) = 0                                        (QRel)
                                               ∑︁

                                               𝜌

   is:

  1. CKP-origin;

  2. H4-admissible LocalDiag-origin;

  3. strict C1 Edge-origin;

  4. impossible;

  5. or genuinely free-affine.

   Only cases 1–4 close HGO.2 structurally.
   —

BAOC.2. Setup: Base B1 and B3 Coordinate Source                                   Lemma B1 supplies a parent product
block
                                  𝑟             𝑠
                                       𝑎𝑖 +         𝑏𝑗 = 𝑁,          𝑟, 𝑠 ≤ 2𝐽0 .                              (B1)
                                 ∏︁            ∏︁

                                 𝑖=1          𝑗=1

   Lemma B3 supplies a finite grouping set. For a grouping

                                                     Γ = (𝐼, 𝐽)
   one has grouped variables

                                       𝑢𝐼 =                      𝑣𝐼 =
                                               ∏︁                        ∏︁
                                                     𝑎𝑖 ,                      𝑎𝑖 ,
                                               𝑖∈𝐼                       𝑖∈𝐼
                                                                          /

   and

                                       𝑢′𝐽 =                     𝑣𝐽′ =
                                               ∏︁                        ∏︁
                                                     𝑏𝑗 ,                       𝑏𝑗 ,
                                               𝑗∈𝐽                       𝑗 ∈𝐽
                                                                           /

   with grouped parent relation

                                               𝑢𝐼 𝑣𝐼 + 𝑢′𝐽 𝑣𝐽′ = 𝑁.                                            (B3)
    At the affine-origin bookkeeping level, a selected grouped variable is treated as a coordinate in
a finite free coordinate system attached to (ℬ, Γ). Thus the base coefficient vectors are coordinate
vectors

                                                            𝑒𝛼
   for surviving grouped variables and residual product variables.


                                                            23
    This is a change of coordinates, not an assertion that 𝑒𝛼 is a linear form in the original factor
variables 𝑎𝑖 , 𝑏𝑗 . Product grouping is multiplicative, and the affine catalogue starts after a grouping
has been chosen and the descendant has entered an affine/WACLE regime.
    —

BAOC.3. Setup: Allowed Coefficient Transport Rules The B1/B3/F3/F4/E5 lemmas
support the following transport grammar for homogeneous coefficient vectors.

T1. Fixing and projection When some grouped variables are fixed by dyadic slicing, congru-
ence slicing, or conditioning, they become constants. Homogeneous vectors are projected to the
remaining active coordinates.
   If

                                            𝑧 = (𝑧free , 𝑧fixed )
   and

                                 𝐿(𝑧) = ℓfree · 𝑧free + ℓfixed · 𝑧fixed + 𝑐,
   then the transported vector is

                                                 ℓ ↦→ ℓfree .

T2. Controlled CRT restriction            F3 controlled CRT absorption replaces a lattice coset by a
subcoset

                       Λ′ = {𝑧 ∈ Λ : 𝐿0 (𝑧) ≡ 𝑎        (mod 𝑞)},      𝑞 ≤ (log 𝑁 )𝐶 .
   Choosing coordinates

                                              𝑧 = 𝑧0 + 𝑇 𝑧 ′
   on the sublattice transports

                                                 ℓ ↦→ 𝑇 𝑡 ℓ.                                     (CRT)
    E5 proves that controlled content remains controlled. The particular matrix 𝑇 is part of the
skeleton provenance data.

T3. Fixed divisor quotient        If a fixed divisor condition

                                                 𝑑 | 𝐿(𝑧)
   is absorbed and the quotient form survives, then on the restricted lattice

                                            𝐿𝑑 (𝑧) = 𝐿(𝑧)/𝑑.
   On homogeneous vectors this gives
                                                   1 𝑡
                                                ℓ ↦→ 𝑇 ℓ,                                  (FDQ)
                                                   𝑑
   where the right side is integral on the restricted coordinate lattice. E5/F4 prove content does
not increase. The triple (𝑑, 𝑇, ℓ) is recorded as part of the quotient-origin data.

                                                       24
T4. Variable quotient residual        For an ordinary quotient equation

                                              𝐿(𝑧) = 𝑑𝑠,                                         (VQ)
   F4 either routes to Edge, LocalDiag, CKP, or leaves a central-long affine GoodAWACK quotient
form.
   If 𝑠 survives as an active quotient form, then in the extended active coordinate system its
homogeneous vector ℓ𝑠 satisfies

                                             𝑑ℓ𝑠 = 𝑇 𝑡 ℓ𝐿 .                                    (VQT)
     This relation is part of the origin record. If it forces local dependence, the atom is LocalDiag;
if it exposes balanced multiplicative structure, it is CKP; if it gives a strict C1 budget, it is Edge.
Otherwise it may feed GoodAWACK.

T5. Bounded affine regrouping          E5 permits bounded affine changes and regrouping:

                                            𝑧 = 𝑧0 + 𝐴𝑧 ′ ,
   where relevant coefficients and minors are bounded by powers of log 𝑁 . The vector transport is

                                               ℓ ↦→ 𝐴𝑡 ℓ.                                       (AFF)
   This preserves controlled content, but by itself it does not decide true complexity.

T6. Primitive slicing      Primitive slicing chooses a long one-dimensional fibre

                                             𝑧 = 𝑧0 + 𝑢𝑣.
   On the fibre a marked form becomes

                                 𝐿(𝑧0 + 𝑢𝑣) = 𝑔𝑢 + 𝑏,         𝑔 = ℓ(𝑣).
   For BAOC, the pre-slicing vector ℓ remains the object used in the TC1/HighTC tensor test.
The fibre coefficient 𝑔 is used analytically by E7/E9.

T7. Auxiliary bounded forms Auxiliary bounded or smooth coefficient forms inherit their
homogeneous vectors through the same transport rules T1–T6.
    No routing step is allowed to introduce an affine form without one of these provenance opera-
tions.
    —

BAOC.4. Statement and Proof: Transport-Level Catalogue

Theorem 5.10 (Theorem BAOC.1. Transport-level affine-origin catalogue). Every active affine
form 𝐿𝜌 in a terminal GoodAWACK skeleton produced by

                                        𝐵1 → 𝐵3 → 𝐹 3/𝐹 4
  has a homogeneous vector ℓ𝜌 generated from the B1/B3 grouped-coordinate source by finitely
many applications of T1–T7.


                                                  25
   Equivalently, for every terminal skeleton S there exists a finite provenance expression

                                               ℓ𝜌 ∈ 𝒞tr (ℬ, Γ, r)
   for each active form, where 𝒞tr is the transport closure generated by T1–T7.

Proof. Start with the B1 parent block. By Lemma B1, the only initial variables are finitely many
product variables 𝑎𝑖 , 𝑏𝑗 , with 𝑟, 𝑠 ≤ 2𝐽0 .
    Choose the B3 grouping history Γ. By Lemma B3, the grouping set is finite and each grouping
replaces products of parent variables by grouped variables 𝑢𝐼 , 𝑣𝐼 , 𝑢′𝐽 , 𝑣𝐽′ . At the affine bookkeeping
level these grouped variables supply the base coordinate vectors.
    F3 allows only controlled CRT absorption, F4 large-divisor decision, finite grouping selec-
tion/elimination, terminal LocalDiag detection, terminal Edge detection, and terminal labelling.
Controlled CRT absorption transports coefficient vectors by T2.
    F4 handles fixed divisor and variable quotient equations. F4.3–F4.4 give fixed divisor absorption
and quotient content control, which are T3. F4.5–F4.11 give the exhaustive variable quotient
decision, which is T4 together with the alternatives Edge, LocalDiag, CKP, and GoodAWACK. If
the quotient relation creates forced local dependence, balanced multiplicative structure, or strict
saving, the atom is no longer terminal GoodAWACK; it is LocalDiag, CKP, or Edge. Hence any
quotient form that reaches GoodAWACK is exactly a T4 quotient form.
    E5 records the permitted affine regrouping, primitive slicing, and content-stability operations.
These are T5 and T6. Auxiliary forms inherit the same transport data, giving T7.
    Since the F3 measure is well-founded and every routing history is finite, only finitely many
transport steps occur. Therefore every terminal GoodAWACK homogeneous vector lies in the
transport closure 𝒞tr (ℬ, Γ, r). This proves the transport catalogue.
    —


BAOC.5. Scope Boundary Relative to NoFAH                        BAOC is a provenance grammar, not the
final no-free-affine closure theorem.
    By itself it does not decide:

   1. whether a given affine regrouping is tagged or untagged in the E10M sense;

   2. whether a HighTC relation among the ℓ𝜌 ⊙ ℓ𝜌 is origin-degenerate;

   3. whether a formal free-affine pattern is impossible for actual B1 descendants.

   Consequently, BAOC alone cannot exclude the formal free-affine pattern

                 ℓ0 = (1, 0),   ℓ1 = (1, 1),     ℓ2 = (1, 2),       ℓ3 = (1, 3).          (4AP-vectors)
   These vectors have bounded coefficients and controlled content. Their tensors satisfy

                                      𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.
    The BAOC transport grammar alone does not contain a rule saying that a bounded affine family
of this shape cannot be produced by T1–T7.
    Thus BAOC proves provenance, while NoFAH is supplied by E10Y/E10X/E10K/E10L.
    —


                                                      26
BAOC.6. Structural Closure Needed for NoFAH                  The structural closure must add a tagged-
origin classification to the transport grammar.

Lemma 5.11 (Lemma BAOC.2. Tagged B1 affine-origin closure). For every parent block ℬ,
grouping Γ, and terminal routing history r, the transport closure T1–T7 can be refined to a finite-
parametric list

                                F(ℬ, Γ, r) = {ℱ𝜈 (p) : 𝜈 ∈ 𝒩 , p ∈ 𝒫𝜈 },
   where each ℱ𝜈 (p) gives:

  1. a concrete active coordinate lattice;

  2. concrete transport matrices 𝑇, 𝐴;

  3. concrete quotient-origin relations;

  4. the full active affine vector list {ℓ𝜌 };

  5. the marked set ℳ;

  6. the terminal rejection data for Edge, CKP, LocalDiag, and LongAP/Local.

   Moreover, for every listed family, every HighTC certificate is origin-degenerate, impossible, or
routed by the E10M/E10K/E10L no-untagged-AFF closure.
   Then NoFAH follows.

Proof that the tagged closure implies NoFAH. Let S be an actual terminal GoodAWACK skeleton
with a HighTC certificate. The tagged closure places its coefficient vectors in one of the listed
families ℱ𝜈 (p). The final clause says that the certificate is origin-degenerate, impossible, or excluded
by the no-untagged-AFF closure. Therefore S is not FreeAffineHighTC. This proves NoFAH.
   By HGO2R, NoFAH implies full HGO.2.
   —


BAOC.7. Scope Boundary: Alternative Route Through B3/H4                            There is a different
possible strong input:

                          Every B3 affine-dependence flag is H4-canonical.
   If this were proved, then many free-affine patterns, including the 4AP identity

                                       𝐿0 − 3𝐿1 + 3𝐿2 − 𝐿3 = 0,
   could be safely routed to LocalDiag.
   This alternative is not used here. Lemma H4 deliberately admits only canonical local projections
tagged by the parent B1 cell and routing history. A bare affine identity among oscillatory forms is
not enough.
   Thus the B3/H4 route would require a separate admission theorem. The proof instead uses
E10Y/E10X/E10K/E10L.
   —



                                                   27
BAOC.8. Output for Branch B          The Branch B chain is:

             GoodAWACK = TC1 ⊔ OriginDegenerateHighTC ⊔ FreeAffineHighTC.
   The TC1 part is closed by Lemma TNG, which packages TGT, MRT, TTD, ROC, BRS, TTH,
and X9L-GT in the near-global form. The second part is rerouted by HGO2R.
   The remaining part is

                                      𝑅FreeAffineHighTC (𝑁 ).
   BAOC records this class as a structural catalogue boundary. The class is not left to BAOC
alone: E10M proves that no untagged rank-dropping affine origin survives, E10K converts this into
AFF-origin completeness, and E10L assembles the resulting GoodAWACK cancellation.
   —
Remark 5.12 (BAOC.9. Output).

BAOC proves the transport catalogue; the no-free-affine closure is supplied by E10Y/E10X/E10K/E10L.

   Established output:

                                         ℓ𝜌 ∈ 𝒞tr (ℬ, Γ, r)
   for every terminal GoodAWACK active affine form.
   Structural closure:

                 The free-affine class is discharged by E10Y/E10X/E10K/E10L.
   Structural completion block:


      E10Y/E10X/E10K enumerate and classify the relevant rank-dropping affine origins.

   This is the structural task supplied by the E10X closure chain.

5.5   Part 5. E10G: Strong BAOC catalogue
Source file: Lemmas/e10g_strong_baoc_catalogue_ltx.md.

E10G. Strong BAOC Catalogue and Reduction

E10G.0. Statement and Role Lemma E10G supplies a finite catalogue schema and identifies
the FreeAffineHighTC obstruction that is discharged by the finite GoodAWACK grammar closure
Lemmas E10Y and E10X. It is not used as an independent proof of strong BAOC. Its role is to
reduce the formal catalogue class to the actual-origin closure theorem E10Y/E10X, after which
E10K gives AFF-origin completeness and E10L assembles the GoodAWACK estimate.
   E10G treats the strong form of BAOC isolated by Lemma BAOC.
   The desired structural statement is:


  every actual terminal GoodAWACK affine-vector family has no FreeAffineHighTC certificate.


                                                28
   Equivalently, for every terminal GoodAWACK skeleton

                            S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   produced by

                                          𝐵1 → 𝐵3 → 𝐹 3/𝐹 4,
   every HighTC relation

                                         𝑐𝜌 (ℓ𝜌 ⊙ ℓ𝜌 ) = 0,          𝑐𝑚 ̸= 0
                                   ∑︁

                                     𝜌

   with 𝑚 ∈ ℳS should be forced into one of:

                         CKP,        LocalDiag,              Edge,       Impossible.
   The outcome is a precise split.


A finite-parametric catalogue compiler is available, and the decisive actual-origin rigidity is supplied by E10Y/E

   More concretely:

  1. B1/B3/F3/F4/E5 give a finite-parametric transport catalogue schema for all terminal
     GoodAWACK coefficient vectors.

  2. For every fixed catalogue cell, the TC1/HighTC tensor test is a finite symbolic row-reduction
     problem.

  3. The broad affine-regrouping/CRT transport interface admits formal 4AP-like FreeAffine-
     HighTC vector patterns, so the proof routes those formal witnesses to the actual-origin closure
     theorem E10Y/E10X.

   Thus E10G supplies the finite catalogue schema and identifies the closure input supplied by
E10Y/E10X:


prove transport rigidity for the actual affine-regrouping matrices, or route every resulting free affine dependence

   —

E10G.1. Setup: Source Data Already Proved                        We use only the already established source
lemmas.

B1 source    Lemma B1 supplies a typed finite-convolution parent block
                                                     𝑟                          𝑠
            𝑃𝐴 (𝑎) + 𝑃𝐵 (𝑏) = 𝑁,         𝑃𝐴 (𝑎) =                 𝑃𝐵 (𝑏) =                  𝑟, 𝑠 ≤ 2𝐽0 .   (B1)
                                                    ∏︁                         ∏︁
                                                          𝑎𝑖 ,                       𝑏𝑗 ,
                                                    𝑖=1                        𝑗=1

   The parent block has finitely many dyadic scale and coefficient-type choices.



                                                      29
B3 source    Lemma B3 supplies a finite grouping set

                                       𝒢(ℬ),      |𝒢(ℬ)| ≪𝐽0 1,
   and preliminary labels:

              TypeI/Edge,     LongAP/Local,        CKP,     BranchB,    LocalDiag flag.
   For the BranchB/GoodAWACK path, all short, purely local, CKP-balanced, and forced-dependence
candidates must have failed or have been terminally routed away.

F3/F4 source     Lemma F3 defines terminal GoodAWACK by:

  1. central-long affine WACLE structure;

  2. bounded affine complexity;

  3. smooth weight of polylogarithmic complexity;

  4. no forced local diagonal relation;

  5. no unresolved ordinary large divisor condition;

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

  7. long active fibre directions.

   Lemma F4 proves the exhaustive ordinary-divisor decision:

              OrdinaryLargeDivisor =⇒ Edge ⊔ LocalDiag ⊔ CKP ⊔ GoodAWACK,
   or else the corrected F3 measure strictly decreases.
   The GoodAWACK quotient case is precisely the case where the divisor/quotient ambiguity has
been absorbed or resolved and the remaining object is central-long affine with controlled content.

E5 source    Lemma E5 proves controlled content stability under:


CRT,    fixed divisor absorption,    primitive slicing,   affine regrouping,   Cauchy/cube,   local diagonal extracti

   For the present catalogue, the important point is that E5 controls content but does not enu-
merate the affine transport matrices.
   —

E10G.2. Strong catalogue cells Fix a parent block ℬ, a B3 grouping Γ ∈ 𝒢(ℬ), and an F3/F4
routing history r that ends in terminal GoodAWACK.
   The BAOC grammar can be sharpened into the following finite-parametric catalogue schema.




                                                  30
Cell C0. Base grouped-coordinate cell             After choosing (ℬ, Γ), the active pre-routing coordi-
nate module is

                                    𝑉0 = Z𝑘0 ,       𝑘0 ≤ 𝐾0 (𝐽0 ).
   The base homogeneous vectors are coordinate vectors

                                                 𝑒𝛼 ∈ 𝑉0*
   attached to surviving grouped variables and residual product variables.
   This cell is finite for fixed 𝐽0 .

Cell C1. Projection/fixing cell       Fixing dyadic, congruence, or auxiliary variables replaces

                                         𝑉 ∼
                                           = 𝑉free ⊕ 𝑉fixed
   by 𝑉free . Homogeneous vectors are transported by the projection

                                                         *
                                         𝜋free : 𝑉 * → 𝑉free .
   This cell cannot create HighTC relations not already present after restriction; it only deletes
coordinates.

Cell C2. Controlled CRT cell        A controlled congruence restriction

                             𝐿0 (𝑧) ≡ 𝑎 (mod 𝑞),            𝑞 ≤ (log 𝑁 )𝐶 ,
   chooses coordinates

                                           𝑧 = 𝑧0 + 𝑇 𝑧 ′
   on the sublattice. Homogeneous vectors are transported by

                                              ℓ ↦→ 𝑇 𝑡 ℓ.                                    (CRT-T)
   The determinant and relevant minors of 𝑇 are polylogarithmically controlled by F3/E5. The
actual-origin classification of such matrices is supplied by E10Y/E10X/E10K.

Cell C3. Fixed-divisor quotient cell        For

                                                 𝑑 | 𝐿(𝑧)
   absorbed on a restricted lattice, the quotient form is

                                         𝐿𝑑 (𝑧) = 𝐿(𝑧)/𝑑.
   On coefficient vectors:
                                                 1 𝑡
                                             ℓ ↦→  𝑇 ℓ,                                      (FDQ-T)
                                                 𝑑
   where the right side is integral on the chosen restricted coordinate lattice.
   By F4.4/E5.2, content does not increase:


                                                    31
                                               contΛ (𝐿)
                             contΛ𝑑 (𝐿/𝑑) =                 ≤ contΛ (𝐿).
                                             (contΛ (𝐿), 𝑑)
   This cell is already controlled by F4 at the transport-catalogue level.

Cell C4. Variable quotient residual cell          For a quotient equation

                                              𝐿(𝑧) = 𝑑𝑠,                                       (VQ)
   F4 routes to Edge, LocalDiag, CKP, or GoodAWACK.
   If it reaches GoodAWACK, then neither short-volume Edge, nor forced local dependence, nor
balanced CKP applies. The surviving quotient vector satisfies an origin relation

                                              𝑑ℓ𝑠 = 𝑇 𝑡 ℓ𝐿 .                                 (VQ-T)
    The relation (VQ-T) must be retained as part of the strong catalogue cell.
    Any HighTC certificate using (VQ-T) in a way that determines one active form from another
is origin-degenerate and is already handled by HGO2R.

Cell C5. Bounded affine regrouping cell            E5 allows bounded affine changes and regrouping:

                                           𝑧 = 𝑧0 + 𝐴𝑧 ′ ,
   with coefficients and relevant minors bounded by powers of log 𝑁 . Homogeneous vectors trans-
form by

                                               ℓ ↦→ 𝐴𝑡 ℓ.                                  (AFF-T)
    This is the decisive cell. E5 proves controlled content under such transformations. The classifi-
cation of which matrices 𝐴 can arise from actual routing is supplied by E10Y/E10X/E10K rather
than by E5 itself.
    Therefore C5 requires the actual-origin classification supplied by E10Y/E10X/E10K before it
can be used inside clean terminal GoodAWACK.

Cell C6. Primitive slicing cell      Primitive slicing writes a marked form on a long fibre as

                                       𝐿(𝑧0 + 𝑢𝑣) = 𝑔𝑢 + 𝑏.
    For the true-complexity verification, the relevant vector is the pre-slicing vector ℓ, not merely
the one-dimensional coefficient 𝑔. This cell supplies the analytic E7/E9 interface but does not by
itself decide HighTC.
    —

E10G.3. Catalogue compiler theorem
Lemma 5.13 (Lemma E10G.1. Finite-parametric strong-catalogue schema). Every terminal GoodAWACK
skeleton produced by

                                        𝐵1 → 𝐵3 → 𝐹 3/𝐹 4
   belongs to a finite-parametric catalogue cell obtained by composing C0–C6.
   More explicitly, for each terminal skeleton there are:

                                                   32
  1. a finite B1/B3 source cell (ℬ, Γ);
  2. a finite F3/F4 routing word r;
  3. controlled integer matrices 𝑇𝑗 , 𝐴𝑗 ;
  4. quotient-origin equations 𝑑ℓ𝑠 = 𝑇 𝑡 ℓ𝐿 ;
  5. a finite active list {ℓ𝜌 };
  6. a nonempty marked subset ℳ;
  7. terminal rejection data recording why Edge, CKP, LocalDiag, and LongAP/Local did not
     apply.
   For every fixed choice of this symbolic data, TC1/HighTC is decided by a finite rational row-
reduction on

                                              𝑄𝜌 = ℓ𝜌 ⊙ ℓ𝜌 .
Proof. B1 and B3 give finitely many parent/grouping source cells. The number of parent variables
and groupings is bounded in terms of 𝐽0 .
    F3 has a well-founded routing measure M♯ , and its generic routing steps are limited to con-
trolled CRT absorption, F4 large-divisor decision, square-divisor routing, finite grouping selec-
tion/elimination, terminal LocalDiag detection, terminal Edge detection, and terminal class la-
belling. Hence every routing word r is finite, with length bounded by the initial obstruction data.
    F4 handles every ordinary divisor or quotient predicate. Its fixed-divisor and variable-quotient
branches are exactly C3 and C4 when the residual reaches GoodAWACK; otherwise the atom is
terminal Edge, LocalDiag, or CKP.
    E5 supplies the content-stability rules for CRT restriction, fixed divisor absorption, affine re-
grouping, primitive slicing, and Cauchy/cube operations. At the homogeneous-vector level these
are C1–C6.
    Thus every active terminal vector ℓ𝜌 is produced by a finite composition of C0–C6, with quotient-
origin relations retained. Since the number of active forms and ambient rank are bounded in terms
of 𝐽0 , the tensor list

                                         {ℓ𝜌 ⊙ ℓ𝜌 } ⊂ Sym2 (Q𝑘 )
   has bounded size. Therefore, after fixing a catalogue cell, TC1/HighTC is a finite rational
row-reduction problem. Lemma proved.
   —


E10G.4. Rigidity input for strong BAOC The compiler lemma implies NoFAH once it is
combined with the following rigidity statement, supplied by the master closure Lemma E10X and
the AFF-OC consequence E10K.
Lemma 5.14 (Lemma E10G.2. Transport-rigidity NoFAH). For every catalogue cell C0–C6 that
is actually produced by the B1/B3/F3/F4 routing history, every HighTC tensor relation

                                        𝑐𝜌 (ℓ𝜌 ⊙ ℓ𝜌 ) = 0,     𝑐𝑚 ̸= 0
                                   ∑︁

                                    𝜌
   with 𝑚 ∈ ℳ is origin-degenerate:

                                                    33
  1. it uses a repeated/proportional source vector;
  2. or it uses a fixed divisor/gcd/quotient-origin relation;
  3. or it exposes a B3 CKP-balanced multiplicative grouping;
  4. or it forces a strict C1 Edge predicate;
  5. or it is incompatible with the parent cell and routing history.

   If E10G.2 holds, then HGO2R gives:

                        HighTC =⇒ CKP ⊔ LocalDiag ⊔ Edge ⊔ Impossible,
   and hence

                                        𝑅FreeAffineHighTC (𝑁 ) = 0.
   Branch B closes using Lemma TNG for the global TC1 near-global testing chain plus the origin-
degenerate rerouting.
   —

E10G.5. Scope Boundary: Free-Affine Class Inside the Catalogue Interface E10G.2 is
a reduction target for the master closure Lemma E10X, not a consequence of the catalogue compiler
alone.
    The free-affine class is not F4’s fixed-divisor or variable-quotient analysis. Those parts carry
explicit origin equations and are exactly the cases handled by HGO2R.
    The obstruction is the combination of:

  1. terminal GoodAWACK accepting any bounded-complexity central-long affine system with
     controlled content and a marked Liouville form, after negative tests fail;
  2. E5 allowing bounded affine regrouping with controlled coefficients/minors;
  3. the catalogue schema alone does not classify the actual matrices 𝐴, 𝑇 ;
  4. the catalogue schema alone does not prove that every affine dependence generated by such
     matrices is H4-canonical LocalDiag.

   Because of C5, the catalogue schema still admits the following vector family:

             ℓ0 = (1, 0),    ℓ1 = (1, 1),       ℓ2 = (1, 2),      ℓ3 = (1, 3).        (4AP-vectors)
   Indeed, these arise from the two-coordinate source (𝑥, 𝑟) by the bounded affine forms

                                   𝑥,     𝑥 + 𝑟,   𝑥 + 2𝑟,     𝑥 + 3𝑟.
   All coefficients are 𝑂(1), all contents are 1, and the affine complexity is bounded.
   Their quadratic tensors satisfy:

                                    𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.                               (4AP-Q)
   If any 𝐿𝑖 is marked, the marked tensor lies in the span of the others. Thus the pattern is
HighTC.
   At the level of the GoodAWACK interface alone, (4AP-vectors) need not be:

                                                    34
  1. Edge by short volume or content;

  2. CKP by balanced multiplicative origin;

  3. LocalDiag in the H4-canonical sense;

  4. impossible from the parent B1 equation.

    Therefore the catalogue compiler passes this formal class to the E10X finite-grammar and
origin-completeness closure.
    This is the same structural interface example as in the NoFAH B1-origin verification, but now
localized to a precise catalogue cell: bounded affine regrouping before the E10X rigidity theorem
is applied.
    —

E10G.6. Closure Route The proof uses Route R1 below, as formalized in E10Y/E10X/E10K/E10L.
Routes R2 and R3 are recorded only as alternative sufficient inputs.

Route R1. Affine-regrouping rigidity Strengthen C5 from arbitrary bounded affine regroup-
ing to an explicit rigid list of matrices generated by the actual B1/B3/F3/F4 operations.
    One sufficient target would be:

                               𝐴 ∈ 𝒜rigid (ℬ, Γ, r),    |𝒜rigid | ≪𝐽0 1,
   where every listed matrix is built from coordinate projection, signed permutation, controlled
diagonal quotient, CRT basis choice with recorded congruence origin, and incidence maps coming
from quotient equations.
   Then one must row-reduce each resulting family and prove that every HighTC relation is origin-
degenerate or impossible.

Route R2. B3/H4 canonical-local admission Prove that every B3 affine-dependence flag
surviving into a terminal GoodAWACK-looking affine system is actually H4-admissible canonical
LocalDiag.
   This would route patterns such as

                                      𝐿0 − 3𝐿1 + 3𝐿2 − 𝐿3 = 0
    to LocalDiag, but only if the resulting local term is genuinely admitted by H4’s tagged canonical
local-projection interface.
    This route must not use the broad word "affine dependence" alone; it needs an H4 admission
proof.

Route R3. Higher-order analytic input An actual 4AP-like free-affine catalogue cell outside
the E10Y/E10X/E10K actual-origin closure would require a separate analytic estimate at that cell.
     Such an estimate would have to control the surviving HighTC family, for example through a
𝑈 3 -level or nilsequence orthogonality input with complexity strong enough for the exact catalogue
cell.
     This route reintroduces a higher-order analytic block, but now with a sharply specified target
rather than the whole GoodAWACK class.
     —

                                                   35
Remark 5.15 (E10G.7. Output).

      E10G proves the finite catalogue schema used by the E10Y/E10X/E10K/E10L closure.

   What is proved here:


Every terminal GoodAWACK atom belongs to a finite-parametric catalogue schema C0–C6, and each fixed cell h

   Structural closure:

               The C5/free-affine class is discharged by E10Y/E10X/E10K/E10L.
   Completion block:

          E10Y/E10X/E10K provide the required affine-regrouping origin completeness.

5.6   Part 6. E10H: Rigidity interface
Source file: Lemmas/e10h_e10g_rigidity_ltx.md.

E10H. Matrix Rigidity Reduction for Strong BAOC

E10H.0. Statement and Role Lemma E10H is a reduction: it localizes the structural issue
left by E10G to CRT/AFF matrix-origin rigidity. The resulting reduction is closed by the finite
GoodAWACK grammar Lemma E10X, whose proof uses E10I, E10J, E10Y, E10M, and E10K. The
E10S records are non-logical reproducibility support, not part of this closure.
    E10H treats the next block after Lemma E10G.
    The target isolated there was:


E10G-Rigidity: enumerate the actual affine-regrouping/CRT matrices allowed by B1/B3/F3/F4.

   The purpose of E10H is to isolate the precise rigidity statement needed from the source lemmas.
   The outcome is a sharper reduction:


All non-matrix transport operations are origin-safe; the remaining target is CRT/AFF matrix-origin rigidity.

   More precisely, the source lemmas prove enough to control:

  1. fixing/projection;

  2. fixed divisor quotient;

  3. variable quotient residuals, provided quotient-origin equations are retained;

  4. primitive slicing as an analytic fibre operation;

  5. Cauchy/cube shifts as linear-part preserving operations.

   The part isolated for the matrix-origin step is the enumeration of:

                                                 36
  1. the basis matrices used in controlled CRT sublattices;

  2. the bounded affine regrouping matrices admitted by E5;

  3. the full active vector list after these matrices are composed.

   Thus E10H reduces E10G-Rigidity to a concrete matrix-origin lemma stated in Section E10H.7,
which is discharged by E10X.
   —

E10H.1. Rigidity statement           Let S be a terminal GoodAWACK skeleton from

                                              𝐵1 → 𝐵3 → 𝐹 3/𝐹 4.
   Write the active affine forms as

                               𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 ,            𝑄𝜌 = ℓ𝜌 ⊙ ℓ𝜌 .
   The E10G-Rigidity statement isolated by this reduction is:
Lemma 5.16 (Lemma E10H.Rig). For every actual terminal GoodAWACK skeleton S, the coef-
ficient vectors ℓ𝜌 lie in an explicitly enumerated finite-parametric matrix family

                                                   ℛ(ℬ, Γ, r),
   where every matrix in the family carries one of the following origin tags:

  1. coordinate projection/fixing;

  2. CRT sublattice basis tied to a controlled congruence;

  3. fixed divisor quotient;

  4. variable quotient residual;

  5. B3 grouping incidence;

  6. primitive slicing/fibre selection;

  7. Cauchy/cube shift.

   Moreover, every HighTC tensor relation

                                               𝑐𝜌 𝑄𝜌 = 0,        𝑐𝑚 ̸= 0
                                       ∑︁

                                          𝜌

   for a marked 𝑚 ∈ ℳ is origin-degenerate or impossible.
   If this lemma holds, then E10G and HGO2R imply:

                                       𝑅FreeAffineHighTC (𝑁 ) = 0.
   —

E10H.2. Safe transport operations                We first separate the transport operations that are al-
ready safe.

                                                       37
S1. Fixing and projection         Projection deletes fixed coordinates:

                                       ℓ = (ℓfree , ℓfixed ) ↦→ ℓfree .
    This operation cannot introduce a new untagged origin. If it creates equality, proportionality,
or forced collision between surviving forms, F3 routes the atom to LocalDiag. Otherwise it merely
lowers ambient rank.
    Projection may turn a previously TC1 system into HighTC by collapsing coordinates. But then
the collapse itself is recorded as a fixing/projection origin. If the resulting relation is caused by the
collapse, it is not FreeAffine; if it is not caused by the collapse, it must already be present in the
pre-projection system.
    Thus projection is origin-safe.

S2. Fixed divisor quotient        For a fixed divisor condition

                                                 𝑑 | 𝐿(𝑧),
   F4/E5 replace the lattice by

                                  Λ𝑑 = {𝑧 ∈ Λ : 𝐿(𝑧) ≡ 0         (mod 𝑑)}
   and the quotient form by

                                                𝐿𝑑 = 𝐿/𝑑.
   At the vector level:
                                                       1 𝑡
                                                ℓ ↦→     𝑇 ℓ,
                                                       𝑑
   and F4.4/E5.2 prove

                                                 contΛ (𝐿)
                              contΛ𝑑 (𝐿/𝑑) =                  ≤ contΛ (𝐿).
                                               (contΛ (𝐿), 𝑑)
    Any HighTC relation whose support uses the fixed quotient in a way that determines one active
form from another is origin-degenerate by HGO2R, cases D1/D2. If it does not use the quotient
origin, the fixed quotient is merely a controlled vector transport.
    Thus fixed divisor quotient is safe except for the CRT matrix 𝑇 , which is separated below.

S3. Variable quotient residual         For

                                               𝐿(𝑧) = 𝑑𝑠,
   F4 gives the exhaustive alternative:

                             Edge ⊔ LocalDiag ⊔ CKP ⊔ GoodAWACK.
   If the quotient reaches GoodAWACK, the quotient vector satisfies an explicit origin equation

                                               𝑑ℓ𝑠 = 𝑇 𝑡 ℓ𝐿 .                               (VQ-origin)
   If a HighTC certificate uses this equation to force dependence, then it is origin-degenerate:


                                                       38
  1. short quotient/divisor gives Edge;

  2. forced determination gives LocalDiag;

  3. balanced multiplicative quotient gives CKP;

  4. incompatibility gives Impossible.

    Therefore variable quotient residuals are safe, again modulo the same CRT/basis matrix-origin
target 𝑇 .

S4. Primitive slicing     Primitive slicing writes a marked form on a one-dimensional fibre as

                                         𝐿(𝑧0 + 𝑢𝑣) = 𝑔𝑢 + 𝑏.
   For TC1/HighTC classification, the relevant object remains the pre-slicing vector ℓ. The fibre
coefficient 𝑔 is used by E7/E9 analytically. Primitive slicing therefore does not create a new HighTC
tensor relation among the pre-slicing vectors.
   Thus primitive slicing is not the rigidity obstruction.

S5. Cauchy/cube shifts       Cauchy/cube operations introduce shifts:

                                       𝐿(𝑧 + 𝜔ℎ) = 𝐿(𝑧) + ℓ(𝜔ℎ).
    The linear part in 𝑧 remains ℓ. If cube operations create equality, proportionality, or forced
local dependence, E5/F3 route to LocalDiag. Otherwise at least one marked controlled-content
form survives.
    Hence Cauchy/cube operations are linear-part safe.
    —

E10H.3. The remaining matrix operations                 The only remaining operations capable of cre-
ating new free affine tensor patterns are:

M1. Controlled CRT basis choice            F3 controlled CRT absorption imposes

                              𝐿(𝑧) ≡ 𝑎     (mod 𝑞),          𝑞 ≤ (log 𝑁 )𝐶 ,
   and replaces the lattice coset by

                                Λ′ = {𝑧 ∈ Λ : 𝐿(𝑧) ≡ 𝑎          (mod 𝑞)}.
   To express Λ′ in free coordinates, one chooses a basis

                                             𝑧 = 𝑧0 + 𝑇 𝑧 ′ .
   Vectors transform by

                                               ℓ ↦→ 𝑇 𝑡 ℓ.
    The F3/E5 statements control the index and content growth. They do not by themselves
classify the possible matrices 𝑇 , nor do they constrain the resulting rows beyond polylogarithmic
content/minor bounds.

                                                   39
M2. Bounded affine regrouping          E5 permits an integer affine map
                                                    ′
                                             𝑇 : Z𝑟 → Z𝑟
   with coefficients and relevant minors bounded by powers of log 𝑁 , and records only:

                                  cont(𝐿 ∘ 𝑇 ) ≤ (log 𝑁 )𝐶 cont(𝐿).
   If 𝑇 is unimodular, content is preserved exactly.
   This proves content stability, but not rigidity. It does not say that 𝑇 must be a coordinate
projection, signed permutation, diagonal quotient, incidence matrix, or any other finite rigid matrix
family.
   Thus M1/M2 are exactly where E10G-Rigidity requires the E10X actual-origin classification.
   —

E10H.4. Interface Example: Formal 4AP-like Witness Before imposing the actual-descendant
constraint supplied by E10X, the broad M1/M2 interface permits, at the coefficient-vector level,
the following formal situation.
    Take four source coordinate forms 𝑌0 , 𝑌1 , 𝑌2 , 𝑌3 on Z4 , and restrict/regroup to a two-dimensional
affine sublattice

                                     𝑌𝑖 = 𝑥 + 𝑖𝑟,        0 ≤ 𝑖 ≤ 3.
   Equivalently, use the matrix

                                                  1      0
                                                    ⎛     ⎞
                                                ⎜1       1⎟
                                             𝑇 =⎜          ⎟,
                                                ⎜          ⎟
                                                ⎝1       2⎠
                                                  1      3
   so that

                                             𝑇 𝑡 𝑒𝑖 = (1, 𝑖).
   The transported vectors are

                                     ℓ𝑖 = (1, 𝑖),        0 ≤ 𝑖 ≤ 3.
   They have bounded coefficients and content 1. Their quadratic tensors satisfy

                                    𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.                                (4AP-Q)
   No equality or proportionality among the 𝐿𝑖 = 𝑥+ 𝑖𝑟 is forced. The domain can be central-long:

                        𝑥 ≍ 𝑋,      𝑟 ≍ 𝑅,       𝑥 + 3𝑟 ≍ 𝑋,          𝑋, 𝑅 ≥ 𝑁 𝜃 .
   This is a FreeAffineHighTC pattern unless the routing history records an origin that makes it:

  1. CKP;

  2. H4-canonical LocalDiag;

  3. strict C1 Edge;

                                                    40
  4. impossible.

    The broad M1/M2 matrix hypotheses alone do not decide whether a matrix of this kind is an
actual terminal descendant. Therefore this formal pattern is not used as a terminal GoodAWACK
cell. Its role is to show why the matrix-origin reduction in E10H must be paired with the finite-
grammar theorem E10X.
    E10X supplies that actual-origin information. If such a 4AP-like rank-dropping transport is
produced by actual B1/B3/F3/F4 routing, then its rank drop is tagged and the cell leaves clean
terminal GoodAWACK by the CKP, LocalDiag, Edge, Impossible, or post-terminal analytic route.
If it is untagged, then it is not an admissible actual descendant under the F3-complete routing
interface.
    —

E10H.5. Why H4 admission is not automatic                One might try to use the linear identity

                                      𝐿0 − 3𝐿1 + 3𝐿2 − 𝐿3 = 0
   to label the 4AP pattern LocalDiag.
   This is not justified by Lemma H4.
   H4 admits a local/main term only if it equals the tagged canonical local projection

                                            Loc𝑄 𝑅ℬ,𝜏 (𝑁 )
    up to 𝑜(𝑁 ).
    A bare affine identity among oscillatory forms does not prove such an equality. In particular, a
Liouville-weighted four-term affine pattern is a nonlocal oscillatory configuration, not automatically
a local density projection modulo 𝑄.
    Therefore the H4 route would require the additional theorem:


        every B3/F3 affine-dependence flag surviving from actual routing is H4-canonical.

    The proof does not use this automatic-H4 implication. Instead, it uses E10Y/E10X/E10K to
exclude the untagged actual terminal occurrence before E10L assembles the clean GoodAWACK
estimate.
    —

E10H.6. Rigidity reduction theorem

Lemma 5.17 (Lemma E10H.1. Reduction to matrix-origin rigidity). For terminal GoodAWACK
skeletons in the proof tree, every HighTC certificate is origin-degenerate or impossible unless it is
supported entirely after applying M1/M2 matrix transports in a way that does not use fixed-divisor,
variable-quotient, repeated/proportional, CKP-balanced, C1 Edge, or parent-incompatibility origins.
    Equivalently:

             FreeAffineHighTC ⊆ HighTC produced by CRT/AFF matrix transport.

Proof. By E10G, every terminal GoodAWACK vector is produced by the catalogue cells C0–C6.
    Cells corresponding to fixing/projection, fixed divisor quotient, variable quotient residual, primi-
tive slicing, and Cauchy/cube shifts are S1–S5 above. In each case, either the operation preserves the

                                                  41
relevant linear parts, deletes coordinates with recorded origin, or carries an explicit quotient/local
origin.
    If a HighTC relation uses any of these origins in an essential way, then HGO2R routes it to
CKP, H4-admissible LocalDiag, strict C1 Edge, or Impossible. If it does not use those origins, then
those operations are irrelevant to its free-affine character.
    The only operations left capable of producing a new untagged affine tensor relation are M1 con-
trolled CRT basis choice and M2 bounded affine regrouping. Therefore every remaining FreeAffine-
HighTC certificate must come from the matrix-origin part. Lemma proved.
    —


E10H.7. Matrix-origin closure lemma             The structural conclusion is stated directly at the
matrix level.
Lemma 5.18 (Lemma E10H.2. CRT/AFF matrix-origin rigidity). Let 𝑇tot be the total coeffi-
cient transport matrix obtained by composing all controlled CRT basis choices and bounded affine
regroupings in an actual terminal GoodAWACK routing history.
    Then one of the following holds:

  1. 𝑇tot belongs to an explicitly enumerated rigid family whose tensor row-reduction has no FreeAffine-
     HighTC relation;

  2. any HighTC relation created by 𝑇tot is tagged by a quotient/gcd/divisor/local origin and is
     origin-degenerate;

  3. the corresponding tagged atom is H4-canonical LocalDiag;

  4. the routing cell is empty or violates B1/B3/F3/F4 admissibility.

   E10X supplies this conclusion for actual terminal GoodAWACK descendants. With that input,
E10H.2 gives:

                                      𝑅FreeAffineHighTC (𝑁 ) = 0.
    The formal 4AP-like cell of E10H.4 is not an obstruction to E10H.2: it is not a constructed
actual B1 descendant. E10X proves that an actual untagged occurrence of that type is impossible
in the routing tree.
    —
Remark 5.19 (E10H.8. Output).

              E10H reduces FreeAffineHighTC to CRT/AFF matrix-origin rigidity.

   What is proved here:

          FreeAffineHighTC is reduced to the CRT/AFF matrix-origin rigidity problem.
   Structural closure:

                 The remaining rank-dropping AFF issue is discharged by E10X.
   Completion block:

                                                  42
         MOR: Matrix-Origin Rigidity for controlled CRT and bounded affine regrouping.

   This block is supplied by E10X, using E10I, E10J, E10Y, E10M, and E10K.

5.7    Part 7. E10I: Matrix-origin rigidity
Source file: Lemmas/e10i_mor_matrix_origin_rigidity_ltx.md.

E10I. Matrix-Origin Rigidity Verification

E10I.0. Statement and Role Lemma E10I supplies the MOR reduction to untagged rank-
dropping AFF. That final class is discharged by the finite GoodAWACK grammar Lemma E10X.
   Therefore the class isolated by E10I is not a hidden gap; it is the input passed to the E10J–
E10Y–E10M–E10K closure packaged by E10X.
   E10I continues the MOR block isolated in Lemma E10H.
   The target was:


       MOR: prove matrix-origin rigidity for controlled CRT and bounded affine regrouping.

   The outcome is a further reduction.


controlled CRT and full-rank affine coordinate changes are tensor-safe; E10I reduces the matrix target to untagg

   At the stage of E10I alone, the proof has reduced rather than proved

                                    𝑅FreeAffineHighTC (𝑁 ) = 0,
   because the remaining matrix target is the following narrower statement, which is discharged
by E10X:


      FreeAffineHighTC ⊆ HighTC created by rank-dropping AFF transport without origin.

   —

E10I.1. Linear algebra fact: tensor tests are invariant under rational isomorphism
Let 𝑉, 𝑊 be finite-dimensional rational vector spaces and let

                                            𝑆 : 𝑉 * → 𝑊*
   be an injective linear map. It induces

                    Sym2 (𝑆) : Sym2 (𝑉 * ) → Sym2 (𝑊 * ),     ℓ ⊙ ℓ ↦→ 𝑆ℓ ⊙ 𝑆ℓ.
   If 𝑆 is injective, then Sym2 (𝑆) is injective.
   Consequently, for any finite family {ℓ𝜌 } ⊂ 𝑉 * and any marked index 𝑚,


                                                 43
                                 ℓ𝑚 ⊙ ℓ𝑚 ∈ spanQ {ℓ𝜌 ⊙ ℓ𝜌 : 𝜌 ̸= 𝑚}
   if and only if

                              𝑆ℓ𝑚 ⊙ 𝑆ℓ𝑚 ∈ spanQ {𝑆ℓ𝜌 ⊙ 𝑆ℓ𝜌 : 𝜌 ̸= 𝑚}.

Proof. Choose bases. An injective linear map 𝑆 has a left inverse over Q on its image. Hence the
induced map on symmetric tensors also has a left inverse on its image, so Sym2 (𝑆) is injective.
    Applying Sym2 (𝑆) to a rational linear relation among the tensors preserves the relation. Con-
versely, if a relation holds after applying Sym2 (𝑆), injectivity implies the same relation held before
applying it.
    This proves the equivalence.
    —


E10I.2. Controlled CRT is tensor-safe           In F3, a controlled CRT restriction replaces a lattice
coset by

                       Λ′ = {𝑧 ∈ Λ : 𝐿(𝑧) ≡ 𝑎     (mod 𝑞)},      𝑞 ≤ (log 𝑁 )𝐶 .
    If nonempty, Λ′ is a finite-index subcoset of Λ. Its difference lattice has the same rank as the
original difference lattice.
    Choosing coordinates on Λ′ gives

                                            𝑧 = 𝑧0 + 𝑇 𝑧 ′ ,
    where 𝑇 is a full-rank square matrix over Q after choosing bases of the original and restricted
difference lattices. Homogeneous vectors transform by

                                               ℓ ↦→ 𝑇 𝑡 ℓ.
   Since 𝑇 𝑡 is injective over Q, Section E10I.1 shows that the TC1/HighTC tensor test is invariant
under this coordinate choice.

Lemma 5.20 (Lemma E10I.1. CRT basis choice does not create FreeAffineHighTC). Controlled
CRT basis choice cannot turn a TC1 family into a FreeAffineHighTC family, nor can it create a
new untagged tensor relation. Any HighTC relation after CRT was already present before CRT,
transported by an injective symmetric-square map.

Proof. Immediate from E10I.1 and the full-rank finite-index nature of controlled CRT restrictions.
   Thus the matrix-origin residual is not ordinary CRT basis choice.
   —




                                                   44
E10I.3. Full-rank affine regrouping is tensor-safe                   E5 permits bounded affine regrouping:

                                            𝑧 = 𝑧0 + 𝐴𝑧 ′ .
   If this regrouping is a full-rank coordinate change between equal-rank active parameter lattices,
then 𝐴 is invertible over Q. Homogeneous vectors transform by

                                               ℓ ↦→ 𝐴𝑡 ℓ.
   Again 𝐴𝑡 is injective, so the tensor test is invariant.
Lemma 5.21 (Lemma E10I.2. Full-rank AFF maps are not the obstruction). Any bounded affine
regrouping whose linear part is full-rank on the active affine span preserves the TC1/HighTC clas-
sification.
     In particular, unimodular changes, finite-index basis changes, signed permutations, and diagonal
controlled quotient coordinate changes cannot create a new FreeAffineHighTC certificate.
Proof. Apply E10I.1 to 𝑆 = 𝐴𝑡 .
   —


E10I.4. Rank-dropping AFF maps are the only remaining matrix danger                             The tensor
test is not invariant under rank-dropping maps.
    If
                                                     ′
                                            𝐴 : Q𝑘 → Q𝑘
   has rank 𝑘 ′ < 𝑘, then
                                                                 ′
                                         𝐴𝑡 : (Q𝑘 )* → (Q𝑘 )*
   need not be injective. Distinct quadratic tensors in Sym2 ((Q𝑘 )* ) may collapse to dependent
tensors after restriction to the lower-dimensional slice.
   This is exactly how a 4AP-like pattern appears.
   Take source coordinate forms

                                             𝑌0 , 𝑌1 , 𝑌2 , 𝑌3
   on Q4 , and restrict to the two-dimensional slice

                                     𝑌𝑖 = 𝑥 + 𝑖𝑟,         0 ≤ 𝑖 ≤ 3.
   The resulting vectors are

                                      ℓ𝑖 = (1, 𝑖),        0 ≤ 𝑖 ≤ 3,
   and

                                     𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.
   This tensor relation is not produced by an invertible coordinate change. It is produced by a
rank-dropping affine slice.
   Thus any structural MOR proof must control rank-dropping AFF maps.
   —

                                                     45
E10I.5. What B1/B3/F3/F4/E5 contribute to rank-dropping maps The source lemmas
do not introduce a free list of rank-dropping affine maps. They provide product data, routing
operations, and stability transports whose actual rank-dropping occurrences are classified by the
E10Y/E10M grammar and then packaged by E10X. The E10S records supply reproducibility checks
for this classification, but they are not the proof of the classification.

B1    Lemma B1 gives product variables and dyadic cells, not affine matrix parametrizations.

B3    Lemma B3 gives a finite set of product groupings:

                                      𝑢𝐼 =                     𝑣𝐼 =
                                             ∏︁                       ∏︁
                                                   𝑥𝑖 ,                     𝑥𝑖 ,
                                             𝑖∈𝐼                      𝑖∈𝐼
                                                                       /

     and preliminary labels. It does not give a matrix list for later affine parameterizations.

F3 Lemma F3 permits controlled CRT absorption and terminal routing. CRT is full-rank and
tensor-safe by E10I.1. F3 does not list affine slices of the form

                                               𝑌𝑖 = 𝑥 + 𝑖𝑟.

F4 Lemma F4 handles fixed-divisor and variable-quotient origins. These are origin-tagged and al-
ready routed by HGO2R when they cause HighTC. F4 does not enumerate untagged rank-dropping
AFF maps.

E5    Lemma E5 is the stability source that explicitly permits a broad affine map:
                                                          ′
                                               𝑇 : Z𝑟 → Z𝑟
     with coefficients and relevant minors bounded by powers of log 𝑁 .
     E5 proves content stability:

                                   cont(𝐿 ∘ 𝑇 ) ≤ (log 𝑁 )𝐶 cont(𝐿).
    It does not say that 𝑇 is full-rank on the active affine span, nor that every rank-dropping 𝑇
carries a quotient/local/CKP/Edge origin.
    Therefore the E5 content-stability statement is not the MOR closure mechanism. The proof
uses E10X to classify the actual rank-dropping occurrences created by the B1/B3/F3/F4 routing
tree and reads E5 only as a stability lemma for those authorized transports.
    —

E10I.6. MOR reduction theorem

Lemma 5.22 (Lemma E10I.3. Reduction to rank-dropping AFF origin). For actual terminal
GoodAWACK skeletons supported by the proof tree,

                                          FreeAffineHighTC
   can only arise from a rank-dropping bounded affine regrouping/slicing map whose rank drop is
not already recorded as:


                                                          46
  1. fixing/projection;
  2. controlled CRT finite-index restriction;
  3. fixed-divisor quotient;
  4. variable quotient residual;
  5. forced LocalDiag;
  6. CKP-balanced grouping;
  7. strict C1 Edge;
  8. parent incompatibility.

Proof. By E10H, all non-matrix operations are origin-safe.
    By E10I.2, controlled CRT basis choices are full-rank finite-index coordinate changes and cannot
create new tensor dependence.
    By E10I.3, full-rank affine regroupings are tensor-safe.
    Thus any remaining FreeAffineHighTC certificate must be created by the only matrix operation
not covered by these safe cases: a rank-dropping AFF map. If the rank drop is tagged by one of
the origins 1–8, then HGO2R reroutes it. Therefore the surviving case is precisely an untagged
rank-dropping AFF origin. Lemma proved.
    —


E10I.7.   Rank-drop closure lemma             The remaining structural input is a rank-drop origin
lemma.
Lemma 5.23 (Lemma E10I.4. No untagged rank-dropping AFF in terminal GoodAWACK). Let
S be an actual terminal GoodAWACK skeleton. Every rank-dropping affine map used to produce
its active affine system is one of:

  1. a recorded fixing/projection already covered by the skeleton origin map;
  2. a quotient/divisor/gcd-origin map covered by F4;
  3. a local/collision map routed to H4-canonical LocalDiag;
  4. a CKP-balanced grouping;
  5. a strict C1 Edge configuration;
  6. an impossible/empty cell.

   Equivalently, no untagged rank-dropping AFF map may survive into terminal GoodAWACK.
   If E10I.4 is proved, then

                                       𝑅FreeAffineHighTC (𝑁 ) = 0.
    E10X supplies this lemma for actual terminal GoodAWACK skeletons through the E10Y/E10M
finite-grammar classification. The E10S records document a non-logical reproducibility check for
the maintained source files; they are not used as proof of the classification.
    —

                                                   47
Remark 5.24 (E10I.8. Output).

                MOR is partially proved: CRT and full-rank AFF are tensor-safe.
   Completion theorem:

                No untagged rank-dropping AFF map in terminal GoodAWACK.
   Structural closure:

                                 This task is discharged by E10X.

5.8    Part 8. E10J: Rank-dropping AFF origin verification
Source file: Lemmas/e10j_rda_rank_dropping_aff_origin_verification_ltx.md.

E10J. Rank-Dropping AFF Origin Verification

E10J.0. Statement and Role Lemma E10J proves that tagged rank drops are origin-degenerate
or already routed, and reduces the remaining case to the affine-origin completeness theorem pack-
aged by E10X and proved through the E10Y/E10M/E10K finite-grammar chain for actual terminal
GoodAWACK skeletons. The E10S records remain reproducibility support for the finite source list.
    E10J treats the next block isolated in Lemma E10I.
    The target was:


        RDA: no untagged rank-dropping AFF map survives into terminal GoodAWACK.
   The reduction proved in this file is:

                 RDA reduces to an affine-regrouping origin-completeness lemma.
   What is proved:

                  every tagged rank drop is already routed or origin-degenerate.
   Completion theorem:


      exclude or classify rank drops allowed only by the broad E5 affine-regrouping interface.
   —

E10J.1. RDA statement         Let

                             S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   be an actual terminal GoodAWACK skeleton.
   A rank-dropping AFF map is a bounded affine transport

                                 𝑧 = 𝑧0 + 𝐴𝑧 ′ ,        rank 𝐴 < dim 𝑧,
   used to produce or represent the active affine system.
   It is tagged if its rank drop is recorded as one of:

                                                   48
  1. fixing/projection of inactive coordinates;

  2. fixed divisor quotient;

  3. variable quotient residual;

  4. controlled local/gcd dependence;

  5. CKP-balanced grouping;

  6. strict C1 Edge;

  7. impossible/empty support;

  8. primitive slicing used only analytically, while the pre-slicing vectors remain the tensor-verification
     objects.

   It is untagged if none of these origins is recorded.
   RDA asks to prove:

         no untagged rank-dropping AFF map occurs in terminal GoodAWACK.                        (RDA)
   By E10I, RDA would imply:

                                      𝑅FreeAffineHighTC (𝑁 ) = 0.
   —

E10J.2. Tagged rank drops are safe

Lemma 5.25 (Lemma E10J.1. Tagged rank-dropping AFF is origin-degenerate or irrelevant). If a
rank-dropping AFF map in a terminal GoodAWACK skeleton is tagged by one of the origins listed
in E10J.1, then it cannot support a FreeAffineHighTC certificate.

Proof. We inspect the tagged cases.
    If the rank drop is fixing/projection, then the collapse is recorded in the origin map. Any
HighTC relation caused by the collapse is not free-affine; if it is not caused by the collapse, it was
already present before projection.
    If the rank drop comes from fixed divisor quotient or variable quotient residual, then F4 supplies
the quotient/divisor origin. By HGO2R, any HighTC certificate using that origin is LocalDiag,
CKP, Edge, or Impossible.
    If the rank drop is controlled local/gcd dependence, then it is precisely a LocalDiag-origin case,
admitted only when H4-canonical.
    If it is CKP-balanced, the atom is CKP and handled by G8a.
    If it is strict C1 Edge or empty support, it contributes 𝑜(𝑁 ) or zero.
    If it is primitive slicing, then by E10H and E10I the pre-slicing vectors remain the objects used
in the TC1/HighTC tensor verification; the one-dimensional fibre is an analytic E7/E9 object, not
a new terminal HighTC coefficient family.
    Thus no tagged rank drop produces FreeAffineHighTC. Lemma proved.
    —




                                                  49
E10J.3. Source classification for untagged rank drops We classify what the source lemmas
prove about untagged rank-dropping AFF before the finite-grammar theorem E10X is applied.

B1 Lemma B1 gives typed Heath–Brown product variables and dyadic cells. It does not introduce
affine matrix maps or rank-dropping affine slices.
    Thus B1 does not create an untagged rank-dropping AFF occurrence.

B3   Lemma B3 gives a finite product grouping set:

                                     𝑢𝐼 =                     𝑣𝐼 =
                                            ∏︁                       ∏︁
                                                  𝑥𝑖 ,                     𝑥𝑖 ,
                                            𝑖∈𝐼                      𝑖∈𝐼
                                                                      /

    and preliminary labels. It also says that forced equality, proportionality, repeated factor, fixed
gcd-local dependence, or affine dependence may produce a LocalDiag flag.
    But the corrected H4 interface does not accept a bare affine dependence as LocalDiag unless it is
a tagged canonical local projection. Therefore B3 is not by itself the closure theorem for untagged
rank-dropping AFF. Its role is to provide finite grouping data and tags used by E10X.

F3 Lemma F3 performs controlled CRT absorption, F4 large-divisor decision, square-divisor rout-
ing, finite grouping selection/elimination, LocalDiag detection, Edge detection, and terminal class
labelling.
    Controlled CRT is full-rank and tensor-safe by E10I.
    F3 does not enumerate rank-dropping affine regrouping maps. Its terminal GoodAWACK pred-
icate is negative:

  1. central-long affine WACLE;

  2. bounded affine complexity;

  3. no forced LocalDiag;

  4. no unresolved ordinary large divisor;

  5. marked Liouville-type affine form;

  6. long active directions.

    This negative predicate must be read together with the complete F3.6 operation list. F3 la-
bels terminal GoodAWACK descendants; it does not license a new untagged rank-dropping affine
parametrization.

F4 Lemma F4 handles ordinary divisor and quotient origins. These are tagged rank drops and
are safe by E10J.2.
    F4 handles the tagged divisor, quotient, gcd, balanced CKP, and strict C1 origins. Any rank
drop not tied to one of these origins is passed to the E10X finite-grammar closure rather than
treated as an admissible terminal generator.




                                                         50
BGS      Lemma BGS records

                                                   rgrp
     as affine regrouping or affine changes of variables, and includes an origin map

                                                 origS .
    This is enough to state RDA. The proof that every actual rank drop in rgrp is one of the tagged
origins in E10J.1 is supplied by E10X through the E10Y grammar theorem and E10M. The E10S
records are non-logical reproducibility support for the maintained source files.

E5    Lemma E5 permits an affine map
                                                     ′
                                             𝑇 : Z𝑟 → Z𝑟
     with coefficients and relevant minors bounded by powers of log 𝑁 , and proves only:

                                   cont(𝐿 ∘ 𝑇 ) ≤ (log 𝑁 )𝐶 cont(𝐿).
     It does not state:

  1. 𝑇 must be full-rank on the active affine span;

  2. every rank drop of 𝑇 must be fixing/projection;

  3. every rank drop of 𝑇 must have quotient/divisor/gcd/CKP/Edge/LocalDiag origin;

  4. every affine dependence created by 𝑇 is H4-canonical LocalDiag.

   Therefore E5 is a stability lemma, not the closure theorem for RDA. The proof reads E5 in the
E10X-clean sense: it may transport already authorized full-rank or tagged data, but it is not an
additional terminal generator of untagged rank-dropping AFF.
   —

E10J.4. Formal rank-dropping AFF witness At the broad E5/BGS interface, before apply-
ing E10X’s actual-descendant restriction, one can write the following formal rank-dropping AFF
cell.
    Start with four independent source coordinate forms

                                             𝑌0 , 𝑌1 , 𝑌2 , 𝑌3 .
     Apply the rank-dropping affine parametrization

                                     𝑌𝑖 = 𝑥 + 𝑖𝑟,          0 ≤ 𝑖 ≤ 3.
     Equivalently, the transport matrix is

                                                 1        0
                                                   ⎛        ⎞
                                               ⎜1         1⎟
                                             𝐴=⎜            ⎟.
                                               ⎜            ⎟
                                               ⎝1         2⎠
                                                 1        3


                                                    51
   The resulting homogeneous vectors are

                                             ℓ𝑖 = (1, 𝑖).
   They satisfy the HighTC tensor relation

                                     𝑄0 − 3𝑄1 + 3𝑄2 − 𝑄3 = 0.
   All contents are 1, all coefficients are 𝑂(1), and the affine complexity is bounded. A central-long
domain can be chosen:

                        𝑥 ≍ 𝑋,      𝑟 ≍ 𝑅,      𝑥 + 3𝑟 ≍ 𝑋,      𝑋, 𝑅 ≥ 𝑁 𝜃 .
    At the level of the broad terminal GoodAWACK wording alone, this formal cell is not automat-
ically:

  1. Edge;

  2. CKP;

  3. H4-canonical LocalDiag;

  4. impossible.

    Thus broad interface language alone does not classify this formal rank-dropping AFF cell.
    This is not claimed to be an actual B1 descendant. It is an interface example showing why
RDA is proved through E10Y/E10X/E10K rather than through the broad E5/BGS wording alone.
If this pattern is generated by actual B1/B3/F3/F4 routing, then E10X classifies its rank drop and
routes it away from clean terminal GoodAWACK; if it remains untagged, it is not an admissible
actual terminal skeleton.
    —

E10J.5. RDA reduction theorem

Lemma 5.26 (Lemma E10J.2. RDA reduces to affine-regrouping origin completeness). Assume
the following origin-completeness statement:


    Every rank-dropping affine regrouping recorded in rgrp is tagged by one of E10J.1(1)–(8).
                                                                                       (AFF-OC)
   Then RDA holds.

Proof. Let S be a terminal GoodAWACK skeleton. By E10I, any FreeAffineHighTC certificate
must arise from a rank-dropping AFF map.
   By AFF-OC, every such rank drop is tagged by one of the origins in E10J.1.
   By Lemma E10J.1, tagged rank drops are origin-degenerate or irrelevant for FreeAffineHighTC.
   Therefore no FreeAffineHighTC certificate remains. This proves RDA.
   —




                                                 52
E10J.6. AFF-origin completeness closure lemma              The closure block is an origin-completeness
upgrade for affine regrouping.

Lemma 5.27 (Lemma E10J.3. AFF-origin completeness). In every actual B1/B3/F3/F4 terminal
GoodAWACK routing history, every affine regrouping or affine change of variables recorded in

                                                  rgrp
   has linear part 𝐴 satisfying exactly one of:

  1. 𝐴 is full-rank on the active affine span;

  2. the rank drop is a recorded fixing/projection;

  3. the rank drop is induced by fixed divisor or quotient-origin data;

  4. the rank drop is induced by a forced local/gcd/collision relation and is H4-canonical LocalDiag;

  5. the rank drop exposes CKP-balanced grouping;

  6. the rank drop gives strict C1 Edge;

  7. the cell is impossible.

   If E10J.3 is proved, then:

                                     𝑅FreeAffineHighTC (𝑁 ) = 0.
   E10Y/E10X/E10K supply E10J.3 for the actual terminal GoodAWACK cells.
   —

Remark 5.28 (E10J.7. Output).

      RDA is reduced to AFF-origin completeness, which is supplied by E10Y/E10X/E10K.

   What is proved:

         RDA follows from AFF-origin completeness, and all tagged rank drops are safe.
   Structural closure:

         AFF-origin completeness is discharged by E10X and assembled in E10K/E10L.
   Completion block:

                         AFF-OC: Affine-regrouping origin completeness.
   This block is supplied by E10X and assembled in E10K/E10L.

5.9   Part 9. E10Y: GoodAWACK routing grammar completeness
Source file: Lemmas/e10y_goodawack_routing_grammar_completeness_ltx.md.

E10Y. Completeness of the GoodAWACK Routing Grammar

                                                  53
E10Y.0. Statement and Role Lemma E10Y is a structural completeness theorem for the
GoodAWACK routing grammar. It proves that every operation which can generate or modify an
actual terminal GoodAWACK affine skeleton is already represented in the finite B1/B3/F3/F4
routing grammar, with E5 used only for controlled content transport.
    The lemma concerns only actual B1/B3/F3/F4/E5-generated descendants. It does not
classify arbitrary bounded affine systems and it does not assert that every formal affine parametriza-
tion is reachable. Its assertion is:


 every skeleton-generating pre-terminal operation in an actual B1-origin GoodAWACK descendant is one of the o
                                                                                            (E10Y)
    Consequently, an unlisted rank-dropping affine regrouping cannot enter a terminal GoodAWACK
skeleton as a hidden operation. Post-terminal analytic operations may estimate a fixed terminal
object, but they do not generate a new terminal GoodAWACK skeleton.
    Logical dependencies are B1, B3, F3, F3A, F3T, F4, and the content-stability calculations of E5.
E10Y is used by E10M, E10X, E10K, and E10L. E10S and E10S-MECH are maintained separately
as non-logical reproducibility records for the same finite operation list.
    —

E10Y.1. Setup

Actual routing record       An actual routing record is a tuple

                                      r = (𝑉, 𝒞, ℒ, 𝒬, 𝜏, orig, 𝑊 )
   where:

  1. 𝑉 is the finite list of active variables inherited from B1;

  2. 𝒞 records dyadic, congruence, content, gcd and divisor restrictions;

  3. ℒ is the finite list of affine forms visible on the current cell;

  4. 𝒬 records fixed-divisor, quotient and local tags;

  5. 𝜏 is the current routing tag;

  6. orig records the origin of every rank-changing operation;

  7. 𝑊 is the bounded or polylogarithmic weight data transported with the cell.

   An actual terminal GoodAWACK skeleton is the terminal value of such a routing record along
a descendant of

                                       𝐵1 −→ 𝐵3 −→ 𝐹 3/𝐹 4.




                                                   54
Pre-terminal operation A pre-terminal operation is a transformation of an actual routing
record before terminal class labelling. It is actual-generated if it is invoked by the B1, B3, F3
or F4 routing construction, or by the E5 content-stability calculation applied to a record already
produced by those routing layers. This definition is external to the E10Y grammar: it refers to
the construction of descendants in B1/B3/F3/F4/E5, not to the list of E10Y transition classes.
Thus "actual-generated" means "lying in the image of the independently defined B1/B3/F3/F4/E5
construction"; it does not mean "allowed because E10Y allows it."

Lemma 5.29 (Lemma E10Y.0. Source-to-record extraction). Every Branch B descendant that is
actually produced by B1/B3/F3/F4/E5 and then fed to the GoodAWACK terminal class carries a
finite routing record
                                 r = (𝑉, 𝒞, ℒ, 𝒬, 𝜏, orig, 𝑊 )
of the kind defined above. Each rank-relevant operation occurrence in that descendant is represented
either by a transformation of this record before terminal labelling or by a post-terminal analytic
operation after terminal labelling.

Proof. B1 fixes a finite-depth Heath–Brown product block, its variables, its dyadic cell and its
coefficient data. B3 replaces this by one of finitely many grouped product records. F3 and F4 act
only through their recorded routing decisions: congruence restrictions, divisor or quotient choices,
local/gcd relations, Edge or CKP routing, continuation tags, and terminal class labels. E5 is
applied only to a record already carrying those variables, constraints and origin tags. Hence every
actual Branch B descendant has a finite record of the displayed form. Any later TC1/HighTC,
coarea, Fourier, BRS/X16, Davenport/AP, Cauchy–Schwarz or local-projection step is performed
only after the terminal routing record has already been fixed, and is therefore recorded as post-
terminal analytic use rather than as a new pre-terminal operation.
    This proves the extraction claim.


Skeleton-generating operation           A pre-terminal operation is skeleton-generating if it changes
at least one of

                                  𝑉,       𝒞,     ℒ,      𝒬,      orig,
   in a way that can affect the terminal GoodAWACK affine skeleton.

Post-terminal analytic non-generator A post-terminal analytic non-generator is an operation
performed after a terminal routing object has been fixed. Such an operation may form test functions,
apply Cauchy–Schwarz, take Fourier transforms, slice a fixed testing family, or estimate an auxiliary
sum. It does not create a new B1/B3/F3/F4 descendant and it does not add a new terminal
GoodAWACK skeleton.

Terminal tensor-test vectors           For a terminal GoodAWACK skeleton S, the terminal affine
forms are
                                       ℒS = {𝐿𝜌 (𝑧) = ℓ𝜌 · 𝑧 + 𝑐𝜌 }.
The TC1/HighTC test is applied to the corresponding terminal vectors ℓ𝜌 and tensors 𝑄𝜌 = ℓ𝜌 ⊗ ℓ𝜌 .
Post-terminal operations may restrict domains, average over fibres, or introduce auxiliary testing
variables, but they may not replace the terminal list {ℓ𝜌 } by a new list and then treat the new list as


                                                    55
a fresh GoodAWACK routing descendant. Any operation that would change the terminal tensor-
test vectors for routing purposes must already occur as a pre-terminal operation in the routing
record.

Rank drop and tag An affine transformation is full-rank on the active affine span if its linear
part is injective on the difference space generated by the current active forms, up to the finite-index
restrictions already recorded in 𝒞. For terminal GoodAWACK records, E5-clean full-rank transport
also has trivial kernel on the span of the terminal tensor-test vectors. It is rank-dropping if this
injectivity fails on the active span or on the terminal tensor-test span.
    Throughout this lemma, a bounded affine map means an affine map whose coefficients, denomi-
nators and induced lattice index are controlled by the fixed routing complexity and the polylogarith-
mic parameter hierarchy. Thus "bounded" is not a new qualitative assumption; it is the quantitative
bounded-complexity condition already present in the B1/B3/F3/F4/E5 routing record.
    A rank drop is tagged if orig records one of:


Fix/Proj,   CRT,     FixedDiv,    VarQuot,    LocalDiag,     CKP,    Edge,    PostTerminalNonGenerator.

   It is untagged if it is present only as a free affine regrouping or formal affine parametrization.
   —

E10Y.2. Phase Separation
Lemma 5.30 (Lemma E10Y.1. Pre-terminal and post-terminal phases are disjoint). Every actual
B1-origin descendant has a finite pre-terminal routing phase followed by a terminal analytic phase.
Operations from the terminal analytic phase do not generate new terminal GoodAWACK skeletons.
Proof. B1 supplies typed Heath–Brown product variables, dyadic cells and exact convolution weights.
B3 supplies finitely many product-grouping candidates and preliminary structural labels. F3 and
F4 then perform the finite routing decisions that determine whether the descendant is Edge, CKP,
GoodAWACK, LongAP/Local or LocalDiag.
    Once a GoodAWACK terminal object has been labelled, the later TC1/HighTC, Cauchy–
Schwarz, Fourier, coarea, Shiu/BRS, Davenport/AP and local projection arguments operate on
that fixed terminal object or on a testing family derived from it. None of those arguments returns
to B3, F3 or F4 to create an additional descendant, and none introduces a new terminal routing
class.
    Thus the routing construction has two separated phases:

             B1/B3/F3/F4 pre-terminal routing       then   terminal analytic estimation.
   The second phase estimates, reroutes or discards already fixed terminal data; it is not a skeleton-
generation mechanism.
   —


E10Y.3. Initial B1/B3 Sources
Lemma 5.31 (Lemma E10Y.2. B1 and B3 introduce no free rank-dropping affine regrouping). B1
and B3 supply finitely many initial sources for the routing grammar, but neither layer introduces
an arbitrary rank-dropping affine regrouping into a terminal GoodAWACK skeleton.

                                                  56
Proof. In B1 the variables are the product variables of the fixed-depth Heath–Brown decomposition,
together with dyadic restrictions and exact convolution weights. This layer introduces product
coordinates and cells; it does not apply a bounded affine map to the active affine span.
    In B3 the construction enumerates finitely many product-grouping candidates. The operation
is a finite selection among grouped product-coordinate descriptions. If the grouping exposes a
short-volume, quotient, local, CKP-balanced or Edge structure, that information is recorded as
a routing feature and passed to F3/F4. If it does not, the descendant remains a candidate for
terminal routing.
    Therefore B1/B3 create the finite set of start states for the later grammar, but they do not add
a hidden rank-dropping AFF operation.
    —


E10Y.4. Exhaustive Pre-Terminal Routing
Lemma 5.32 (Lemma E10Y.3. F3/F4 exhaust the skeleton-generating pre-terminal operations).
Let r be an actual routing record after B3. Every skeleton-generating pre-terminal operation applied
before terminal class labelling is one of the F3/F4 operations recorded in the following list:

  1. controlled CRT absorption;
  2. F4 large-divisor or quotient decision;
  3. square-divisor routing;
  4. finite grouping selection or elimination;
  5. terminal LocalDiag detection;
  6. terminal Edge detection by a C1 predicate;
  7. terminal class labelling into Edge, CKP, GoodAWACK, LongAP/Local or LocalDiag.

Proof. Lemma F3A proves that Section F3.6 is complete for generic F3 routing-level operations.
Lemma F3T expands this list into the complete finite routing table by B1 type, B3 grouping, dyadic
regime, divisor/conductor state, coefficient type, terminal class and exclusion reason. Lemma F4
supplies the ordinary divisor and quotient decision used inside the second item.
    The F3T table has no sixth terminal class and no row whose operation is "arbitrary affine
regrouping." Each non-terminal row either continues the finite routing procedure with a recorded
tag or is eliminated as incompatible, empty, Edge, local, CKP or already terminal. Hence any
actual-generated operation that can change the terminal skeleton before labelling is represented by
the seven operations above.
    —


E10Y.5. Full-Rank Transport and Tagged Rank Drop
Lemma 5.33 (Lemma E10Y.4. E5 does not add an independent skeleton generator). E5 content
stability may transport content, coefficients and auxiliary variables along an already generated rout-
ing record. It does not create an additional terminal GoodAWACK skeleton from an external affine
system.
    More precisely, every E5-compatible affine transport is one of:

                                                 57
  1. full-rank on the active affine span and on the terminal tensor-test span, with controlled
     bounded-minor/content loss;

  2. rank-dropping with an origin tag already supplied by B1/B3/F3/F4;

  3. post-terminal analytic slicing after the terminal object has already been fixed.

Proof. The content-stability calculation of E5 is applied only after the current routing record has
already supplied the variables, congruence restrictions, divisor data and origin information being
transported. A full-rank transport preserves the active affine rank, is injective on the terminal
tensor-test span, and changes content only by the controlled bounded-minor factors recorded in
E5.
    If the transport is not full-rank on the active affine span, or if it has a kernel on the terminal
tensor-test span, then it is not E5-clean full-rank transport. The lost rank must then come from
a restriction already present in the routing record: fixing/projection, CRT compatibility, fixed
divisor quotient, variable quotient residual, local/diagonal dependence, CKP-balanced structure,
Edge predicate or post-terminal post-terminal analytic slicing. These are exactly the tags recorded
in the origin component of the routing record.
    Thus E5 is a stability principle for transports whose source is already known. It is not a sepa-
rate mechanism for adjoining an untagged rank-dropping affine map to a GoodAWACK terminal
skeleton.
    —


E10Y.6. No Feedback from Analytic Tests

Lemma 5.34 (Lemma E10Y.5. Terminal analytic operations do not feed back into the routing
grammar). Let S be a terminal GoodAWACK skeleton. The TC1/HighTC split, global testing
construction, regular/singular testing dichotomy, BRS/X16 short-image analysis, Davenport/AP
estimate, Cauchy–Schwarz, cube expansion, Fourier expansion and local projection arguments do
not create an additional terminal GoodAWACK skeleton.

Proof. Each listed operation is invoked after the terminal skeleton has been selected. Its input is
a fixed terminal skeleton, a fixed terminal testing family, or a sum derived from those fixed data.
The output is one of the following:

  1. an 𝑜(𝑁 ) analytic estimate;

  2. a routing-away conclusion to Edge, CKP, LongAP/Local or LocalDiag already present in the
     F3/F4 terminal alternatives;

  3. a proof that the GoodAWACK contribution belongs to the HighTC finite grammar closure;

  4. a local-main projection used only in the final assembly.

    None of these outputs is a new B1/B3/F3/F4 descendant. Therefore post-terminal analytic
tests cannot supply a missing pre-terminal operation and cannot produce an untagged terminal
GoodAWACK rank drop.




                                                 58
Lemma 5.35 (Lemma E10Y.5b. Terminal tensor-vector immutability). Once a terminal GoodAWACK
skeleton S is fixed, the affine vectors ℓ𝜌 and tensors 𝑄𝜌 = ℓ𝜌 ⊗ ℓ𝜌 used in the TC1/HighTC test
are immutable under post-terminal analytic operations. Post-terminal slicing, averaging, Cauchy–
Schwarz, cube expansion, TC1 testing, BRS/X16 estimates and Davenport/AP estimates may re-
strict or test the fixed terminal object, but they may not replace the terminal affine skeleton by a
new one.

Proof. By definition, the TC1/HighTC split is applied to the terminal list ℒS produced by B1/B3/F3/F4/E5
before post-terminal estimation begins. A later analytic operation has one of two effects. It either
restricts the summation domain or introduces auxiliary variables used to test, average, or estimate
the already fixed terminal data. Neither effect changes the routing record r, the origin map, or the
terminal class label.
    If a proposed post-terminal step replaced the list {ℓ𝜌 } by a new rank-relevant list and then
used that new list as a terminal GoodAWACK skeleton, the step would be a skeleton-generating
operation rather than a post-terminal analytic operation. By Lemma E10Y.0 and Lemma E10Y.3,
such a step would have to appear in the pre-terminal routing record and be classified by F3/F4/E5.
Therefore it cannot occur as a hidden post-terminal feedback operation.
    —


E10Y.7. Apparent Operations Table The following table records the status of all operation
types that can appear syntactically in the GoodAWACK branch.


      Apparent operation                                      Mathematical status
      Dyadic refinement                                       B1/B3 cell restriction; no affine rank drop
      Product grouping                                        B3 finite candidate source; not a free affine map
      Controlled CRT restriction                              F3 operation; full-rank on the active difference lattice
                                                              or incompatible
      Fixed divisor quotient                                  F4/E5-compatible tagged quotient
      Variable quotient residual                              F4 tagged quotient or rerouting case
      Square-divisor routing                                  F3/F4 Edge or zero/short-fibre routing, recorded by
                                                              tag
      Gcd/local/proportional relation                         F4/HGO2R local or LocalDiag origin
      CKP-balanced relation                                   Terminal CKP tag; not GoodAWACK HighTC
                                                              residue
      Strict saving or boundary relation                      C1 Edge tag
      Full-rank affine coordinate change                      E5 content-stable transport; injective on the active
                                                              affine span and terminal tensor-test span
      Primitive or coarea slicing                             Post-terminal analytic non-generator
      Cauchy–Schwarz or cube expansion                        Post-terminal analytic non-generator
      Fourier expansion or TC1 testing                        Post-terminal analytic non-generator
      Local projection                                        H4/D1 local-main assembly; post-terminal non-
                                                              generator
      Arbitrary rank-dropping affine reparametrization        Not actual-generated unless one of the recorded tags
                                                              is present




   This table is not an extra assumption. It is the union of Lemmas E10Y.0–E10Y.5b.
   —

E10Y.7A. Formal Transition Table                  This section records the routing grammar as transforma-
tions of the actual routing record


                                                         59
                                               r = (𝑉, 𝒞, ℒ, 𝒬, 𝜏, orig, 𝑊 ).
   The table is part of the proof of E10Y. It is not an additional assumption: each row is the
formal state-level version of a B1/B3/F3/F4/E5 operation already isolated above.

 Operation             Input state             Output state             Rank effect            Required tag           If not satisfied
 B1 start-state cre-   no previous Branch      𝑉, 𝒞, 𝑊         from     no affine rank drop    start-state origin     not a Branch B de-
 ation                 B state                 a        fixed-depth                                                   scendant
                                               Heath–Brown
                                               product block
 B3 finite grouping    B1   state    with      one grouped candi-       finite     selection   B3 grouping origin     candidate removed
                       product variables       date Γ, with up-         only; no free affine                          or routed by F3
                                               dated ℒ and pre-         map
                                               liminary 𝜏
 controlled CRT ab-    state with congru-      restricted        lat-   full-rank      finite- CRT                    incompatible fibre,
 sorption              ence 𝐿0 (𝑧) ≡ 𝑎         tice/coset       and     index     restriction                         hence zero/empty
                       (mod 𝑞)                 updated 𝒞                on the active dif-
                                                                        ference lattice, or
                                                                        empty
 F4            quo-    state containing 𝑑 |    updated 𝒬, 𝜏 , and       possible         rank  FixedDiv,              routed away or M♯
 tient/divisor         𝐿(𝑧) or 𝐿(𝑧) = 𝑑𝑠       origin record            drop only through      VarQuot,               decreases
 decision                                                               recorded         quo-  LocalDiag, CKP,
                                                                        tient/local/CKP/Edgeor Edge
                                                                        data
 square-divisor        state with square-      Edge state, con-         no untagged affine     Edge or CRT            zero/short-volume
 routing               divisor predicate       trolled divisibility     rank drop                                     or strict C1 saving
                                               state, or empty
                                               state
 grouping selection    finite B3/F3 candi-     selected candidate,      finite selection; no   B3/F3       grouping   candidate    elimi-
 or elimination        date list               removed      candi-      new affine transfor-   origin                 nated
                                               date, or decreased       mation
                                               routing measure
 LocalDiag    detec-   state with equal-       terminal     Local-      rank       col-        LocalDiag              continue    F3/F4
 tion                  ity, proportional-      Diag state               lapse   leaves                                routing
                       ity, repeated form,                              GoodAWACK
                       or forced local rela-
                       tion
 Edge detection        state satisfying a      terminal        Edge     any collapse is        Edge                   continue    F3/F4
                       C1/C1A        strict-   state                    absorbed into a                               routing
                       saving predicate                                 strict-saving route
 CKP detection         state      exposing     terminal        CKP      rank relation is a     CKP                    continue    F3/F4
                       balanced bilinear       state                    CKP origin, not                               routing
                       Kloosterman-                                     a     GoodAWACK
                       fraction structure                               residual
 GoodAWACK ter-        state with no Edge,     terminal                 labelling only; no     terminal label         not a terminal
 minal labelling       CKP, LocalDiag,         GoodAWACK                coordinate opera-                             GoodAWACK
                       LongAP/Local,           skeleton                 tion                                          skeleton
                       or       unresolved
                       ordinary     divisor
                       predicate
 E5 clean transport    already generated       transported con-         full-rank on active    inherited    origin not E5-clean; must
                       B1/B3/F3/F4             tent/auxiliary data      and      tensor-test   tag, or no tag      be routed/tagged
                       routing record          on the same record       spans, or inherited    needed in full-rank before terminality
                                                                        tagged rank drop       case
 post-terminal ana-    fixed      terminal     test,          slice,    may restrict ana-                          if it changes ter-
                                                                                               PostTerminalNonGenerator
 lytic non-generator   skeleton                Fourier/coarea           lytic sums but can-                        minal vectors, it is
                                               family, or estimate      not replace termi-                         not post-terminal
                                               of the fixed object      nal tensor-test vec-                       and must appear
                                                                        tors                                       above




   Consequently a rank-changing operation in an actual GoodAWACK descendant has only two
possibilities. Either it is one of the pre-terminal rows and carries the displayed origin information,

                                                                60
or it is a post-terminal analytic non-generator and cannot create a new terminal GoodAWACK
skeleton.
    —

E10Y.8. Bidirectional Source–Grammar Tables The following two tables make explicit that
E10Y is not taking completeness as an unnamed premise. The first table maps each independently
defined B1/B3/F3/F4/E5 operation to the E10Y transition class that covers it.


   Source operation                        E10Y transition class                   Rank effect
   B1 typed Heath–Brown block and          B1/B3 start-state generation            no affine rank drop
   dyadic cell
   B3 finite product grouping candidate    B1/B3 start-state generation            no free affine map; grouping is
                                                                                   recorded
   F3 controlled CRT absorption            F3/F4 pre-terminal routing              finite-index restriction or incompati-
                                                                                   ble fibre
   F4 divisor or quotient decision         F3/F4 pre-terminal routing              tagged quotient, local, CKP, Edge,
                                                                                   GoodAWACK, or decreasing contin-
                                                                                   uation
   F3 square-divisor routing               F3/F4 pre-terminal routing              Edge or controlled divisibility/CRT
                                                                                   tag
   F3 grouping selection/elimination       F3/F4 pre-terminal routing              finite candidate selection; no new
                                                                                   affine operation
   F3 LocalDiag detection                  F3/F4 pre-terminal routing              terminal      LocalDiag;        leaves
                                                                                   GoodAWACK
   F3 Edge detection                       F3/F4 pre-terminal routing              terminal Edge; leaves GoodAWACK
   F3 terminal labelling                   F3/F4 pre-terminal routing              label only
   E5 full-rank content transport          E5 full-rank content-stability trans-   rank preserved on active and tensor-
                                           port                                    test spans
   E5 rank-dropping transport              E5 tagged content-stability transport   allowed only with an already
                                                                                   recorded origin tag
   TC1/HighTC, BRS/X16, Daven-             post-terminal analytic non-generator    no new routing descendant and no
   port/AP, Fourier, cube, coarea, local                                           replacement of terminal tensor-test
   projection                                                                      vectors




   Conversely, every E10Y transition class has only the following possible sources in the proof tree.


   E10Y transition class                   Possible sources                        Excluded sources
   B1/B3 start-state generation            B1 and B3                               E5, F4, analytic estimates
   F3/F4 pre-terminal routing              F3.6–F3.14 and F4                       arbitrary affine reparametrization;
                                                                                   Cauchy/cube/Fourier steps
   E5 full-rank content-stability trans-   E5 applied to an already generated      external affine systems not produced
   port                                    routing record                          by B1/B3/F3/F4
   E5 tagged rank-dropping transport       E5 with a Fix/Proj, CRT, FixedDiv,      untagged rank-dropping AFF
                                           VarQuot, LocalDiag, CKP or Edge
                                           origin already present
   post-terminal analytic non-generator    terminal analytic estimates applied     any operation that changes the ter-
                                           after the terminal skeleton is fixed    minal tensor-test vectors for routing
                                                                                   purposes




   Thus a syntactically visible operation has two tests. It must appear in the left table as a source
operation, and its E10Y class must have an allowed source in the right table. If either test fails,
the operation is not an actual-generated GoodAWACK skeleton generator.
   —


                                                            61
E10Y.9. Grammar Completeness Theorem

Theorem 5.36 (Theorem E10Y.6. Completeness of the GoodAWACK routing grammar). Every
actual-generated operation that can generate or modify an actual terminal GoodAWACK affine
skeleton is one of the operations in Lemmas E10Y.2–E10Y.5b. Equivalently, the GoodAWACK
routing grammar has no hidden skeleton-generating operation outside:

                                    B1/B3 start-state generation,
                                     F3/F4 pre-terminal routing,
                          E5 full-rank or tagged content-stability transport,
                                post-terminal analytic non-generators.
    Consequently, any rank-dropping affine operation visible in an actual terminal GoodAWACK
skeleton must have one of the recorded origin tags


Fix/Proj,     CRT,    FixedDiv,   VarQuot,     LocalDiag,    CKP,    Edge,      PostTerminalNonGenerator,

    or else the skeleton is not an actual B1-origin terminal GoodAWACK descendant.

Proof. Let S be an actual terminal GoodAWACK skeleton. By Lemma E10Y.0, S has a finite
routing history
                                  𝑟0 → 𝑟1 → · · · → 𝑟𝑇 = S,
where 𝑟0 is a B1/B3 start record and each transition is an actual-generated pre-terminal operation
or a terminal class labelling step. We prove by induction on 𝑡 the invariant

ℐ(𝑟𝑡 ) :   every rank-changing operation up to 𝑟𝑡 is E10Y-classified and carries an allowed origin tag.

    At 𝑡 = 0, Lemma E10Y.2 shows that B1 and B3 supply only product-coordinate and grouping
start states. No untagged rank-changing affine operation has occurred.
    Assume ℐ(𝑟𝑡 ) and consider 𝑟𝑡 → 𝑟𝑡+1 . If the transition is an F3/F4 routing operation, Lemma
E10Y.3 classifies it as controlled CRT, F4 divisor/quotient decision, square-divisor routing, finite
grouping selection or elimination, LocalDiag detection, Edge detection, or terminal class labelling.
Each rank-changing case either records one of the allowed tags or routes the cell away from terminal
GoodAWACK. If the transition is an E5 transport, Lemma E10Y.4 says that it is either full-rank
on the active and terminal tensor-test spans, or else rank-dropping with an already recorded origin
tag. Thus ℐ(𝑟𝑡+1 ) holds.
    After terminal labelling, Lemmas E10Y.5 and E10Y.5b apply. Post-terminal analytic operations
may restrict or test the fixed terminal object, but they do not produce a new routing descendant
and do not replace the terminal tensor-test vectors. Hence they cannot violate the invariant by
adding a hidden skeleton-generating operation.
    These cases exhaust the route from B1 to the terminal GoodAWACK object. Therefore no
additional skeleton-generating operation can occur. In particular, an untagged rank-dropping affine
regrouping is not a permissible operation in the actual GoodAWACK routing grammar.
    —


Parameter check 5.37 (E10Y.10. Parameter Check and Output Form). The theorem introduces
no new analytic parameter and no new error term. Its only finiteness input is the fixed-depth


                                                  62
B1 decomposition, the finite B3 grouping list, the finite F3T routing table and the finite F4 divi-
sor/quotient decision tree. All content losses are those already controlled in E5.
    The output supplied to E10X is:


    the finite grammar used in E10X is complete for actual terminal GoodAWACK skeletons.

   The output supplied to E10M/E10K/E10L is:


a rank-dropping affine regrouping in terminal GoodAWACK is admissible only with an allowed origin tag.

5.10    Part 10. E10M: No untagged rank-dropping AFF
Source file: Lemmas/e10m_no_untagged_rank_dropping_aff_ltx.md.

E10M. No Untagged Rank-Dropping AFF in Terminal GoodAWACK

E10M.0. Statement and Role Lemma E10M is the no-untagged-rank-drop theorem behind
the E10K interface cleanup. Lemma E10Y proves that the GoodAWACK routing grammar is
complete for actual B1-origin terminal skeletons. The master closure is Lemma E10X, which
packages E10Y, E10M, and E10K into the finite GoodAWACK grammar interface.
    The finality of the generator list used below is proved in E10Y. The E10S occurrence record is
a reproducibility check for the source files; it is not a logical prerequisite for the theorem below.
    The issue isolated by E10I–E10K is the following residual:


 could a terminal GoodAWACK skeleton contain an untagged rank-dropping affine regrouping?

    The answer is no, provided the terminal object is required to be an actual descendant of the
active routing tree

                                        𝐵1 → 𝐵3 → 𝐹 3/𝐹 4
    and not merely a formal affine pattern allowed by broad wording in E5, BGS, BAOC or E10G.
    Thus the result below is not a new analytic estimate. It is the structural version of the F3-
complete routing interpretation: every terminal GoodAWACK skeleton must be generated by the
finite operation list already proved in F3.6 and by the F4 large-divisor decision procedure.
    Logical dependencies are B1, B3, F3, F4, E5, BGS, E10Y, E10I, E10J, and HGO2R. E10M is
used by E10X, E10K, and E10L.

Role inside the E10X master closure E10M is the central structural input for the rank-
dropping AFF obstruction isolated in E10H–E10J. Packaged by E10X, it discharges the active
descendants of:

  1. E10H.2, by proving that a formal 4AP-like matrix witness cannot be an untagged actual
     terminal GoodAWACK cell;

  2. E10I.4, by proving that the only rank-dropping AFF residual left after the CRT/full-rank
     safety reductions has no untagged actual occurrence;

                                                 63
  3. E10J.3, by proving AFF-origin completeness for actual B1/B3/F3/F4 terminal GoodAWACK
     routing histories.

   The formal 4AP-like matrix family

                                       𝑌𝑖 = 𝑥 + 𝑖𝑟,        0 ≤ 𝑖 ≤ 3,
    is therefore not deleted from the proof. It is treated in E10X as an interface witness at the
broad E5/BGS/BAOC level. E10M proves the decisive structural claim: if such a rank-dropping
configuration is produced by actual routing, then its rank drop is tagged by one of the permitted
origins; if it is untagged, it violates the E10Y-certified F3-complete routing interface and is not an
admissible terminal GoodAWACK skeleton.
    —

E10M.1. Setup: Definitions

Actual terminal GoodAWACK skeleton                    An actual terminal GoodAWACK skeleton is a
skeleton

                               S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   which occurs as the terminal record of a descendant produced by the E10Y-certified routing
grammar, namely:

  1. the typed Heath–Brown product variables and dyadic cells of Lemma B1;

  2. the finite product-grouping candidates of Lemma B3;

  3. the routing operations of Lemma F3, Section F3.6;

  4. the large-divisor decision procedure of Lemma F4;

  5. the content-stability transports of Lemma E5, read in the clean sense of E10Y/E10L/E10M.

Rank-dropping AFF occurrence A rank-dropping AFF occurrence is a bounded affine map
used in the skeleton record whose linear part drops rank on the active affine span.
   Such an occurrence is tagged if its rank drop is explicitly caused by one of:

  1. fixing or projection;

  2. congruence compatibility or an inconsistent fibre;

  3. fixed divisor quotient;

  4. variable quotient residual;

  5. local/diagonal or gcd origin;

  6. CKP-balanced origin;

  7. strict C1 Edge origin;

  8. post-terminal analytic slicing which is not used to generate the terminal tensor-test vectors.

                                                      64
   It is untagged if it is recorded only as a free affine regrouping or affine parametrization, with
no origin in the routing record.
   —

E10M.2. Statement and Proof

Theorem 5.38 (Theorem E10M.1. No untagged rank-dropping AFF). Let S be an actual terminal
GoodAWACK skeleton. Then every rank-dropping AFF occurrence in its terminal record is tagged.
   Equivalently:


    no untagged rank-dropping affine regrouping survives into terminal GoodAWACK.            (E10M)

Proof. We trace all places where a rank drop could enter an actual terminal GoodAWACK skeleton.
By Lemma E10Y, this trace exhausts all actual-generated skeleton-generating operations.
    B1. By Lemma B1, the starting objects are product variables, dyadic cells and exact Heath–
Brown convolution factors. B1 introduces no affine matrix map and no rank-dropping affine slice.
    B3. By Lemma B3, the next operation is finite product-grouping selection. B3 may record
grouping alternatives and preliminary labels, but it does not introduce a free affine parametriza-
tion. If a grouping exposes short factors, CKP-balanced structure, canonical local structure, forced
dependence or an Edge predicate, the descendant is routed to the corresponding terminal class
rather than being left as untagged GoodAWACK data.
    F3. By Lemma F3, Section F3.6, the generic 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, LocalDiag.

   Cauchy/cube operations and Fourier expansion are explicitly post-terminal proof subroutines,
not generic routing operations. Hence F3 contains no operation whose effect is "add an arbitrary
rank-dropping affine regrouping to the terminal skeleton."
   Controlled CRT absorption is finite-index and full-rank on the difference lattice. It may change
content by bounded or polylogarithmic factors controlled by E5, but it does not create a new
rank-dropping affine relation. If the CRT conditions are incompatible, the fibre is impossible.
   Square-divisor routing is either terminal C1 Edge when the square divisor is large, or a controlled
CRT/divisibility restriction when the square divisor is small. In the second case it is subsumed by
controlled absorption; in the first case it leaves GoodAWACK. Thus it does not create a free affine
rank drop.
   Finite grouping selection/elimination chooses among B3’s already finite product-grouping can-
didates. It either keeps a candidate with its recorded origin data or removes it with a strict
routing-measure decrease. It is not a new affine slice.

                                                 65
    Terminal LocalDiag and terminal Edge detections are tagged by their defining local or C1
predicates. They leave the GoodAWACK class once detected.
    Terminal GoodAWACK labelling is only a label. It records that after the F3/F4 decisions no
Edge, CKP, LongAP/Local, LocalDiag or unresolved large-divisor predicate remains. It is not itself
a coordinate operation.
    F4. By Lemma F4, every ordinary large-divisor or quotient predicate is decided exhaustively.
A rank drop coming from a fixed divisor quotient, variable quotient residual, gcd/local dependence,
proportional or repeated forms, or quotient-determined forms is therefore tagged by the F4 origin
record. The resulting descendant is routed to Edge, CKP, LocalDiag, LongAP/Local, GoodAWACK
with the ambiguity resolved, or to a measure-decreasing continuation.
    Thus F4 may create tagged rank-drop data, but it does not admit a free rank-dropping AFF
occurrence with no origin.
    E5. Lemma E5 supplies content stability for the allowed transports. The phrase "affine re-
grouping" in E5 cannot be read as an additional terminal-routing operation, because F3.6 is the
exhaustive list of such operations. Therefore E5 may be used only for:

  1. full-rank coordinate changes;

  2. tagged fixing/projection or quotient/local transports;

  3. tagged CKP, Edge or impossible-origin reductions;

  4. post-terminal analytic slicing after the terminal tensor-test vectors have already been fixed.

    This is precisely the E5-clean interpretation recorded in E10L.
    Finally, post-terminal primitive slicing, Cauchy/cube and Fourier operations are analytic sub-
routines inside estimates. They are not allowed to generate a new terminal GoodAWACK skeleton
after the TC1/HighTC tensor test has been declared.
    All actual rank-dropping AFF occurrences are therefore tagged by one of the origins listed in
E10M.1. An untagged rank-dropping AFF occurrence would have to come from an operation not
present in B1, B3, F3.6 or F4, or from reading E5 as an extra terminal generator. Both alternatives
contradict the E10Y-certified F3-complete routing interface. The theorem follows.
    —


E10M.3. Finite Classification Table: AFF Occurrence Origins The proof above is sum-
marized by the following finite classification table. The table records every mathematical source in
the B1/B3/F3/F4/E5-clean routing grammar where a reader might suspect that a rank-dropping
affine regrouping is introduced.
     The table is exhaustive by E10Y and the structural source analysis in the proof above. The
separate E10S/E10S-MECH records are non-logical reproducibility checks for the maintained source
files; they are not used to prove the table.


 Source/interface   Phrase or opera-     Can drop rank?    If yes, tag source   Terminal genera-        Why no untagged
                    tion                                                        tor?                    AFF survives
 B1                 Heath–Brown          No                None needed          Yes, as initial prod-   B1 creates product
                    product variables;                                          uct data                coordinates    and
                    dyadic cells                                                                        weights, not affine
                                                                                                        regrouping maps.




                                                      66
B3              finite      product    No as a new affine     Existing B1 group-     Yes, only as candi-   B3 selects among
                grouping; prelimi-     map                    ing record             date selection        finite       product
                nary labels                                                                                groupings;         ex-
                                                                                                           posed         depen-
                                                                                                           dence routes to
                                                                                                           CKP/LocalDiag/Edge/GoodAWA
                                                                                                           labels with origin
                                                                                                           data.
F3, F3.6        controlled CRT ab-     No on the differ-      CRT compatibility      Yes                   CRT restriction is
                sorption               ence lattice           / impossible fibre                           finite-index/full-
                                                                                                           rank on the active
                                                                                                           span;       inconsis-
                                                                                                           tency is tagged
                                                                                                           impossible.
F3, F3.6/F3.9   square-divisor         No untagged affine     C1 square-divisor      Yes                   Large square divi-
                routing                rank drop              Edge or controlled                           sors are terminal
                                                              divisibility tag                             Edge; small square
                                                                                                           divisors     become
                                                                                                           controlled absorp-
                                                                                                           tion and inherit the
                                                                                                           CRT/divisibility
                                                                                                           tag.
F3, F3.6        finite grouping se-    No as a new slice      B3 grouping origin     Yes                   Selection records
                lection/elimination                                                                        or removes a can-
                                                                                                           didate; it is not an
                                                                                                           additional      affine
                                                                                                           operation.
F3, F3.6        LocalDiag     detec-   Yes only by forced     LocalDiag tag          Yes, but leaves       Once       detected,
                tion                   equality/local de-                            GoodAWACK             the atom is ter-
                                       pendence                                                            minal LocalDiag,
                                                                                                           not         terminal
                                                                                                           GoodAWACK.
F3, F3.6        Edge detection         Yes only through       C1 Edge tag            Yes, but leaves       Once detected, the
                                       strict saving predi-                          GoodAWACK             atom is terminal
                                       cate                                                                Edge and is han-
                                                                                                           dled by C1.
F3, F3.6        CKP detection          Yes only through       CKP tag                Yes, but leaves       Once           CKP-
                                       gcd/balanced                                  GoodAWACK             balanced structure
                                       grouping                                                            appears, the atom
                                                                                                           is terminal CKP
                                                                                                           and is handled by
                                                                                                           G8a.
F3, F3.6        GoodAWACK        la-   No                     None needed            Yes                   The label records
                belling                                                                                    the absence of
                                                                                                           other       terminal
                                                                                                           predicates;          it
                                                                                                           performs no coor-
                                                                                                           dinate operation.
F4              fixed divisor quo-     Yes                    F4     fixed-divisor   Yes                   The quotient ori-
                tient                                         origin                                       gin is recorded; un-
                                                                                                           tagged use is for-
                                                                                                           bidden by the F4
                                                                                                           decision procedure.
F4              variable    quotient   Yes                    F4        quotient-    Yes                   The          residual
                residual                                      residual origin                              is     routed       to
                                                                                                           Edge/CKP/LocalDiag/LongAP/
                                                                                                           with ambiguity re-
                                                                                                           solved, or to a
                                                                                                           decreasing contin-
                                                                                                           uation.
F4              repeated/proportional Yes                     local/diagonal or      Yes                   Forced        depen-
                forms                                         C1/CKP origin                                dence is terminally
                                                                                                           routed away or
                                                                                                           recorded as tagged
                                                                                                           origin data.




                                                       67
 E5                   affine    regroup-    Only if read too       E10M-clean full-       No   E5 is a stabil-
                      ing/content stabil-   broadly                rank or tagged              ity    lemma       for
                      ity                                          transport                   transports         al-
                                                                                               ready created by
                                                                                               B1/B3/F3/F4; it
                                                                                               is not an extra ter-
                                                                                               minal generator.
 BGS                  skeleton record /     Records possible       inherited origin tag   No   BGS records termi-
                      𝑟grp                  rank behavior                                      nal data produced
                                                                                               upstream; it does
                                                                                               not create a new
                                                                                               operation.
 BAOC                 weak      transport   Interface only         inherited              No   BAOC is cata-
                      catalogue, C5/T5                             B1/B3/F3/F4                 logue/grammar
                      interface examples                           origin                      support in the
                                                                                               proof tree; broad
                                                                                               catalogue classes
                                                                                               are discharged by
                                                                                               E10Y/E10X/E10K.
 E10G                 bounded     AFF       Reduction only         E10H–E10K chain        No   E10G isolates the
                      cell / FreeAffine-                                                       free-affine class; it
                      HighTC interface                                                         does not autho-
                      example                                                                  rize a new terminal
                                                                                               AFF map.
 E10H                 matrix-origin         Reduces          to    matrix-origin    re-   No   E10H        localizes
                      rigidity reduction    CRT/AFF          is-   duction tag                 the issue to E10I–
                                            sue                                                E10K; it does not
                                                                                               generate a termi-
                                                                                               nal skeleton.
 E10I                 CRT and full-rank     Full-rank only, ex-    MOR/RDA reduc-         No   E10I          proves
                      AFF safety            cept reduced resid-    tion tag                    safe    cases     and
                                            ual                                                passes only rank-
                                                                                               dropping AFF to
                                                                                               E10J/E10M.
 E10J                 tagged rank drops     Yes                    origin-degenerate      No   E10J proves tagged
                                                                   or routed tag               rank drops are safe
                                                                                               and reduces only
                                                                                               the untagged possi-
                                                                                               bility to E10M.
 post-terminal       analytic slicing af-   May restrict ana-                         No
                                                                   PostTerminalNonGenerator    These steps es-
 Cauchy/cube/Fourier ter terminal record    lytic sums             tag                         timate     a    fixed
 steps                                                                                         terminal       atom
                                                                                               and cannot create
                                                                                               a new terminal
                                                                                               GoodAWACK
                                                                                               skeleton.




    Therefore the only conceivable source of an untagged rank-dropping AFF would be to read one
of the record/stability documents as adding a new terminal operation outside F3.6 and F4. The
E10Y-certified F3-complete interface forbids that reading: terminal GoodAWACK skeletons are
actual descendants of B1/B3/F3/F4/E5-clean, not arbitrary formal affine systems.
    —

E10M.4. Output Consequences

Corollary 5.39 (Corollary E10M.2. AFF-OC is discharged). The AFF-origin completeness hy-
pothesis used in Lemma E10K is a theorem for actual terminal GoodAWACK skeletons:

                                                      AFF-OC.


                                                             68
    Thus E10K is no longer merely a conditional cleanup statement. Its F3-COMPLETE assump-
tion is discharged by E10Y and E10M.
Corollary 5.40 (Corollary E10M.3. FreeAffineHighTC is empty in the proof tree). Combining
E10M with the reductions in E10I and E10J gives:

                                      𝑅FreeAffineHighTC (𝑁 ) = 0.
  Together with HGO2R, this leaves only the origin-degenerate HighTC cases, which route to
CKP, LocalDiag, Edge or Impossible.
  —
Remark 5.41 (E10M.5. Output).

    E10M rules out untagged rank-dropping AFF in actual terminal GoodAWACK skeletons.

    It is cited by E10X, E10K and E10L. Its role is to make explicit, after E10Y, that broad "affine re-
grouping" language in E5/BGS/BAOC/E10G is not an additional source of terminal GoodAWACK
affine systems.

E10M.6. Logical Dependencies Internal dependencies: B1, B3, F3, F4, E5, BGS, E10Y,
E10I, E10J, HGO2R.
   Children served: E10X, E10K and E10L.

5.11    Part 11. E10X: Master finite-grammar closure
Source file: Lemmas/e10_master_source_exhaustion_closure_ltx.md.

E10X. Finite GoodAWACK Grammar Closure

E10X.0. Statement and Role Lemma E10X is the finite combinatorial closure theorem for
the GoodAWACK HighTC branch. It packages the reduction chain

                BAOC → E10G → E10H → E10I → E10J → E10Y/E10M → E10K
     into a single theorem-level interface.
     The theorem is not a search assertion. Lemma E10Y proves that the finite grammar below is
complete for actual terminal GoodAWACK skeletons. Lemma E10X uses that grammar and proves
its invariant: every rank-dropping affine operation created along a derivation has an allowed origin
tag. Formal affine counterexamples at the broad BAOC/E10G/E5 interface are therefore irrelevant
unless they are derivable from

                                         𝐵1 → 𝐵3 → 𝐹 3/𝐹 4
   with E5 used only as clean content stability.
   The theorem proved below is:


every actual terminal GoodAWACK skeleton has no untagged rank-dropping AFF source, hence no FreeAffineHi
                                                                                  (E10X)
   This is a structural theorem, not a new analytic estimate.

                                                   69
   Logical dependencies are B1, B3, F3, F4, E5, BGS, BAOC, HGO2R, E10G, E10H, E10I, E10J,
E10Y, E10M, and E10K. E10X is used by E10L and the GoodAWACK HighTC closure.
   —

E10X.1. Setup: Terminal GoodAWACK Skeletons and Grammar States                                            An actual
terminal GoodAWACK skeleton is a record

                                 S = (ℬ, Γ, r, ΛS , ΩS , ℒS , ℳS , origS , 𝒲S )
   generated by the E10Y-certified finite grammar described below.

   1. Lemma B1 supplies typed Heath–Brown product variables, dyadic cells and exact convolution
      weights.

   2. Lemma B3 supplies a finite list of product-grouping candidates and preliminary tags.

   3. Lemma F3, Section F3.6, supplies the complete F3 routing operations: controlled CRT ab-
      sorption, the F4 large-divisor decision, square-divisor routing, finite grouping selection or
      elimination, terminal LocalDiag detection, terminal Edge detection, and terminal class la-
      belling.

   4. Lemma F4 supplies the exhaustive ordinary divisor and quotient decision, with recorded
      quotient, divisor, gcd, local, CKP, Edge, impossible, or continuation origins.

   5. Lemma E5 supplies content stability for transports already generated by the previous routing
      layers. It is not an additional terminal generator of affine systems.

   Thus terminal GoodAWACK skeletons are not arbitrary bounded affine systems. They are
actual descendants of the finite routing grammar above, and Lemma E10Y proves that this grammar
contains every actual-generated skeleton-generating operation.
   —

E10X.2. Finite GoodAWACK grammar theorem                             Define the finite GoodAWACK grammar
𝒢GA as follows.
   A state is a tuple

                                            s = (𝑉, ℒ, 𝒞, 𝒬, 𝒯 , 𝒪),
    where 𝑉 is the finite list of active variables inherited from B1, ℒ is the finite list of affine forms
visible on the current cell, 𝒞 is the list of controlled CRT/content restrictions, 𝒬 is the list of divisor
or quotient tags, 𝒯 is the routing tag, and 𝒪 is the origin record for every rank-changing operation
already applied. The start states are exactly the B1/B3 grouped cells.
    The transition set is finite and consists only of the following operations.


    Transition type                     Allowed effect on affine rank          Required origin tag or outcome
    fixing/projection                   may lower dimension by fixing vari-    Fix/Proj
                                        ables already in 𝑉
    controlled CRT restriction          full-rank on the active span, or in-   CRT or empty
                                        compatible
    fixed-divisor quotient              quotient by a recorded fixed divisor   FixedDiv




                                                        70
   variable quotient residual            quotient/divisor residual selected by    VarQuot or rerouting tag
                                         F4
   local/diagonal/gcd dependence         forced equality, proportionality, re-    LocalDiag
                                         peated form, or gcd-local relation
   CKP-balanced relation                 balanced     bilinear   Kloosterman-     CKP
                                         fraction structure
   strict saving or boundary relation    C1 Edge, square-divisor, short-          Edge
                                         volume,     high-frequency,     small-
                                         conductor, or boundary case
   bounded affine regrouping             full-rank change on the active affine    inherited tag
                                         span, or rank-drop with recorded up-
                                         stream origin
   primitive/post-terminal slicing       occurs only after terminal tensor-test   PostTerminalNonGenerator
                                         vectors are fixed
   E5 auxiliary inheritance              transports content or auxiliary vari-    inherited tag; no terminal generator
                                         ables already generated upstream
   terminal labelling                    labels a terminal cell                   Edge, CKP, GoodAWACK, Local-
                                                                                  Diag, or LongAP/Local




   Every transition is one of the operations authorized in F3.6/F3T or one of the F4 quotient
outcomes. E5 transitions are allowed only when their input state already has an origin record; they
cannot create a terminal GoodAWACK state from an arbitrary external affine system. By E10Y,
no additional actual-generated skeleton-generating transition exists.

Theorem 5.42 (Theorem E10X.2A. Finite grammar invariant). For every state s reachable in
𝒢GA , every rank-dropping affine operation visible in s carries one of the following origin tags:


Fix/Proj,     CRT,      FixedDiv,       VarQuot,      LocalDiag,        CKP,       Edge,      PostTerminalNonGenerator.

   Consequently, a reachable terminal GoodAWACK state has no untagged rank-dropping AFF
operation.

Proof. We argue by induction on the length of the grammar derivation.
   At length zero, the state is a B1/B3 grouped cell. Its affine forms are the original product-
coordinate forms and their grouped descendants, and no rank-dropping affine operation has yet
been applied. The assertion is therefore vacuous.
   Assume the assertion for a reachable state s, and apply one transition.

  • A fixing or projection transition records the tag Fix/Proj.

  • A controlled CRT restriction is either incompatible, hence not terminal, or records the tag
    CRT with controlled content.

  • A fixed divisor quotient records FixedDiv.

  • A variable quotient residual records the F4 quotient tag VarQuot.

  • A local, diagonal, gcd, repeated-form, or proportionality transition records LocalDiag.

  • A balanced bilinear multiplicative transition records CKP.

  • A strict saving, boundary, square-divisor, short-volume, high-frequency, or small-conductor
    transition records Edge.

                                                          71
  • A post-terminal analytic slicing transition is allowed only after the terminal tensor-test vectors
    are fixed; it records PostTerminalNonGenerator and cannot create a new terminal affine
    skeleton.

  • An E5 transition only transports controlled content, CRT data, or auxiliary variables already
    present in the input state. By definition of the E5-clean interface in E10X.1, it inherits the
    existing origin record and does not introduce a new untagged rank-dropping map.

   Thus the invariant is preserved by every transition. Since the transition set is finite and every
terminal GoodAWACK skeleton is, by Lemma E10Y, a reachable terminal state of 𝒢GA , no terminal
GoodAWACK skeleton contains an untagged rank-dropping AFF operation. The theorem is proved.


Corollary 5.43 (Corollary E10X.2B. No free affine HighTC generator). Any formal affine con-
figuration that cannot be derived from 𝒢GA is not an actual terminal GoodAWACK skeleton. In
particular, a FreeAffineHighTC pattern can remain only as a formal interface witness unless it
is produced by a grammar derivation; if it is produced by such a derivation, Theorem E10X.2A
supplies an allowed origin tag and HGO2R/E10K route it to an already handled class.
    —

Verification record 5.44 (E10X.3. Non-Logical Verification Records). The mathematical proof
of E10X is E10Y plus the grammar invariant in Theorem E10X.2A. The records E10S and E10S-
MECH are retained only as non-logical verification records for the maintained source files. They
are useful for checking that later edits have not introduced language outside the finite grammar,
but they are not premises of E10X.
    The maintenance classes used in those records are:

  1. G0, B1 initial product data;

  2. G1, B3 finite product-grouping candidates;

  3. G2, complete F3 routing operations;

  4. G3, F4 quotient and divisor decisions;

  5. G4, E5 content stability;

  6. G5, BGS terminal skeleton recording;

  7. G6, BAOC/E10G/E10H/E10I/E10J catalogue and reduction layers;

  8. G7, E10Y/E10M/E10X/E10K/E10L completion and assembly layers, with E10S/E10S-MECH
     retained only as verification records;

  9. G8, post-terminal analytic subroutines after the terminal skeleton has been fixed.

    These classes mirror the mathematical transition table in E10X.2 and the classification table in
E10M.3. They do not enlarge the proof graph and do not replace the mathematical completeness
assertion E10Y or the invariant proof E10X.2A.
    —




                                                 72
Parameter check 5.45 (E10X.4. Parameter Check: Stability Under Grammar Changes). The
E10X finite-grammar theorem is valid for the grammar specified in E10X.1–E10X.2. Any later
change to the Branch B / GoodAWACK source files must be checked against the grammar before
the package is redistributed.
   The verification must be refreshed if any of the following occurs:

  1. a Branch B / GoodAWACK source file is edited;

  2. a new Branch B / GoodAWACK source file is added;

  3. F3.6 gains, loses, or renames a routing operation;

  4. new rank-changing, slicing, quotient, projection, regrouping, affine, coordinate, matrix, CRT,
     diagonal, or transport language is introduced;

  5. E5 is read as a terminal generator rather than as E10-clean stability;

  6. post-terminal analytic slicing is allowed to replace the terminal vectors used in the TC1/HighTC
     tensor test.

   After such a change, the transition list and E10M table must be refreshed if the mathematical
grammar has changed. The E10S/E10S-MECH records should then be refreshed as reproducibility
support.
   —

E10X.5. Output: No Untagged Rank-Dropping AFF By Lemma E10X.2A, the grammar
invariant already proves that reachable terminal GoodAWACK states have no untagged rank-
dropping AFF. By Lemma E10Y, this grammar is complete for actual terminal GoodAWACK
skeletons. By Lemma E10M, every rank-dropping AFF occurrence found in an actual terminal
GoodAWACK skeleton is one of the tagged grammar cases.
    The allowed tags are:

  1. fixing or projection;

  2. congruence compatibility or impossible fibre;

  3. fixed divisor quotient;

  4. variable quotient residual;

  5. local, diagonal, or gcd origin;

  6. CKP-balanced origin;

  7. strict C1 Edge origin;

  8. post-terminal analytic slicing that does not generate the terminal tensor-test vectors.

  Therefore an untagged rank-dropping affine regrouping cannot occur in an actual terminal
GoodAWACK skeleton:

                                       No-Untagged-AFF.
   —

                                                73
E10X.6. Interface Example: Formal 4𝐴𝑃 -Like Family                    The files E10G, E10H, E10I and
E10J use the formal family

                                     𝑌𝑖 = 𝑥 + 𝑖𝑟,        0 ≤ 𝑖 ≤ 3,
   whose coefficient vectors ℓ𝑖 = (1, 𝑖) satisfy

                             ℓ0 ⊙ ℓ0 − 3ℓ1 ⊙ ℓ1 + 3ℓ2 ⊙ ℓ2 − ℓ3 ⊙ ℓ3 = 0.                     (4AP)
    This example is admissible as a formal interface test: it shows that a broad phrase such as
"bounded affine regrouping" is too large if it is read without the actual B1/B3/F3/F4 routing
origin.
    It is not a terminal GoodAWACK obstruction. Indeed, if such a family arises from a full-rank
affine change on the active affine span, E10I shows that the TC1/HighTC tensor test is invariant
and no new FreeAffineHighTC certificate is created.
    If it arises from a rank-dropping map with fixing, projection, quotient, local, CKP, Edge,
impossible, or post-terminal analytic origin, then HGO2R reroutes the resulting HighTC certificate
to an already handled class.
    If it arises only from an untagged rank-dropping affine parametrization, then it violates the
E10Y-certified routing grammar and is not an actual terminal GoodAWACK skeleton by E10Y/E10M.
    Thus the 4𝐴𝑃 -like example remains in the proof as a sharp interface test, while E10X proves
that it has no untagged actual terminal occurrence.
    —

E10X.7. Proof: AFF-Origin Completeness and FreeAffineHighTC                      Lemma E10K derives
AFF-origin completeness from E10M:


 every rank-dropping affine map in an actual terminal GoodAWACK skeleton has an allowed origin tag.
                                                                                   (AFF-OC)
    By E10J, AFF-OC implies RDA, the rank-dropping AFF origin statement. By E10I, RDA
eliminates the remaining matrix-origin class after CRT and full-rank AFF safety. By E10H and
E10G, this eliminates the broad catalogue FreeAffineHighTC class:

                                      𝑅FreeAffineHighTC (𝑁 ) = 0.
   Together with HGO2R, every HighTC GoodAWACK certificate is therefore either origin-degenerate
and routed to CKP, LocalDiag, Edge, or Impossible, or it is an empty FreeAffineHighTC class.
   —

E10X.8. Output for E10L          The structural input inserted into Theorem E10L.4 is:

                           E10X =⇒ E10K =⇒ 𝑅FreeAffineHighTC (𝑁 ) = 0.
   The TC1 contribution is handled independently by TNG, namely the chain

               𝐵1-origin coarea → MRT/TTD → ROC/BRS → TTH → X9L-GT.
   Thus E10L closes GoodAWACK without X8:



                                                    74
                                   𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).
   —

E10X.9. Logical dependencies Internal dependencies: B1, B3, F3, F3A, F3T, F4, E5, BGS,
HGO2R, BAOC, E10G, E10H, E10I, E10J, E10Y, E10M, and E10K. E10S and E10S-MECH are
verification records, not logical prerequisites.
    Children served: E10L, E10G, E10H, E10I, E10J, the GoodAWACK manuscript section, and
the E10 finite-grammar appendix.

5.12   Part 12. E10K: AFF-origin completeness
Source file: Lemmas/e10k_aff_oc_affine_regrouping_origin_completeness_ltx.md.

E10K. AFF-Origin Completeness

E10K.0. Statement and Role Lemma E10K proves AFF-origin completeness using E10Y
and E10M.
   Lemma E10Y proves that the GoodAWACK routing grammar is complete for actual B1-origin
terminal skeletons. Lemma E10M proves that actual terminal GoodAWACK skeletons contain no
untagged rank-dropping AFF occurrence. Therefore E10K is the AFF-OC consequence of E10Y
plus E10M. Lemma E10X packages this implication as the finite GoodAWACK grammar theorem
used by E10L. The E10S maintenance record is retained only as reproducibility support.
   The target was:


        AFF-OC: every rank-dropping affine regrouping in rgrp has an allowed origin tag.

   The outcome is closure by E10Y grammar completeness and the E10M no-untagged-AFF
lemma:

                            AFF-OC follows from E10Y plus E10M.
   Lemma F3 contains the key fact:

            generic F3 routing operations do not include arbitrary affine regrouping.
    Therefore an untagged rank-dropping affine map cannot be a terminal-routing operation. E10Y
records completeness of the actual B1/B3/F3/F4/E5 operation list, and E10M proves the no-
untagged-rank-drop theorem on that list.
    However, E5, BGS, BAOC, and E10G use broader language around "affine regrouping." That
language is read through the following normalized interface:


affine regrouping may be used only as full-rank coordinate change, tagged projection/fixing, tagged quotient/loc
    With this normalization, made explicit in E10Y and E10M, AFF-OC holds and hence the
structural FreeAffineHighTC obstruction disappears.
    Logical dependencies are B1, B3, F3, F4, E5, BGS, E10G, E10H, E10I, E10J, E10Y, E10M,
and HGO2R. E10K is used by E10X and E10L.
    —

                                               75
E10K.1. Setup: Complete Terminal-Routing Operations                 Lemma F3, Section F3.6, states
that F3 has only the following 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.

   It also explicitly says that Cauchy/cube and Fourier expansion are not generic F3 routing
operations, but post-terminal proof subroutines.
   We use the corresponding reading:

         arbitrary rank-dropping affine regrouping is not a generic F3 routing operation.
                                                                                (F3-COMPLETE)
   This is not an extra mathematical estimate. It is a bookkeeping consequence of the finite
operation list in F3.6.
   —

E10K.2. Setup: Allowed Meanings of Affine Regrouping Under F3-COMPLETE, every
occurrence of "affine regrouping" in the Branch B infrastructure must be interpreted as one of the
following.

A1. Full-rank coordinate change          The linear part is full-rank on the active affine span. By
E10I, this is tensor-safe:

                                           TC1/HighTC
   is invariant under the induced rationally injective map on symmetric tensors.

A2. Tagged fixing/projection Some coordinates are fixed by dyadic slicing, conditioning,
congruence compatibility, or an already recorded routing restriction.
    This is rank-dropping, but the rank drop is tagged. If it creates a HighTC relation, the relation
is caused by recorded projection data and is not FreeAffine.

A3. Tagged F4 quotient/divisor/local origin           The rank drop is produced by:

  1. fixed divisor quotient;

  2. variable quotient residual;

  3. fixed gcd/local dependence;


                                                 76
  4. repeated/proportional forms;

  5. quotient-determined active forms.

   These are exactly F4/BGS origin-degenerate cases and are routed by HGO2R.

A4. Tagged CKP or Edge origin            The rank drop exposes:

  1. B3 CKP-balanced finite-convolution structure;

  2. strict C1 Edge saving;

  3. empty/impossible support.

   These are terminally handled outside GoodAWACK.

A5. Post-terminal analytic slicing Primitive slicing or Cauchy/cube operations may reduce
dimension inside E10’s proof.
    They are not terminal-routing operations generating the GoodAWACK skeleton. For the
TC1/HighTC test, the pre-slicing affine vectors remain the objects being tested; this is the E10H/E10I
interface.
    —

E10K.3. Statement and Proof: AFF-OC after E10Y and E10M

Theorem 5.46 (Theorem E10K.1. AFF-origin completeness). By Lemma E10Y, the terminal
GoodAWACK skeleton is generated by the complete GoodAWACK routing grammar. By Lemma
E10M, actual terminal GoodAWACK skeletons contain no untagged rank-dropping AFF occurrence.
   Then every rank-dropping affine map recorded in

                                                rgrp
   for an actual terminal GoodAWACK skeleton has one of the allowed origin tags A2–A5.
   Equivalently:

             there is no untagged rank-dropping AFF map in terminal GoodAWACK.

Proof. Let S be an actual terminal GoodAWACK skeleton produced by

                                       𝐵1 → 𝐵3 → 𝐹 3/𝐹 4.
    This is now a direct consequence of E10Y and E10M. For completeness, we recall the mechanism.
    By Lemma B1, the starting data are product variables and dyadic cells. No affine rank-dropping
map is introduced at B1.
    By Lemma B3, the grouping choices are finite product groupings. They are recorded as grouping
alternatives. If they reveal short factors, CKP-balanced structure, local AP structure, or forced
dependence, the atom is routed to Edge, CKP, LongAP/Local, or LocalDiag. If not, the residual
may feed BranchB/GoodAWACK, but B3 has not introduced an arbitrary rank-dropping affine
map; it has only selected product groupings and tags.



                                                77
    By F3.6, terminal-routing operations are exactly controlled CRT absorption, F4 large-divisor
decision, square-divisor routing, finite grouping selection/elimination, terminal LocalDiag detec-
tion, terminal Edge detection, and terminal class labelling.
    Controlled CRT absorption is finite-index/full-rank on the difference lattice and is tensor-safe
by E10I.
    F4 large-divisor decision produces either:

  1. Edge;

  2. LocalDiag;

  3. CKP;

  4. GoodAWACK after fixed quotient/divisor ambiguity is resolved.

    Any rank drop caused by fixed divisor, variable quotient, gcd-local dependence, or quotient-
determined forms is therefore tagged by F4 origin data.
    Finite grouping selection/elimination does not create an untagged affine slice. It only chooses
among the finitely many B3 product groupings and either terminally routes the atom or eliminates
the grouping.
    Terminal LocalDiag and Edge detections are tagged by their definitions.
    Terminal GoodAWACK labelling is not a new operation. It only declares that after the above
decisions no unresolved Edge, CKP, LongAP/Local, LocalDiag, ordinary divisor, or grouping al-
ternative remains.
    Therefore any rank-dropping affine map that remains in the terminal GoodAWACK skeleton
must have been one of:

  1. a recorded fixing/projection;

  2. an F4 quotient/divisor/local origin;

  3. a CKP/Edge/impossible origin;

  4. post-terminal analytic slicing not used as the terminal tensor object.

   These are exactly A2–A5.
   Thus no untagged rank-dropping AFF map survives terminal GoodAWACK. E10Y proves that
the preceding list is complete for actual B1-origin terminal skeletons, and E10M proves that each
rank-dropping occurrence in that complete list is tagged. AFF-OC follows. The theorem is proved.
   —


E10K.4. Output for RDA and FreeAffineHighTC                 By E10J, RDA follows from AFF-OC.
  Therefore, using E10Y and E10M:

                                               RDA
   holds.
   By E10I, RDA eliminates the remaining MOR obstruction.
   By E10H, this eliminates the remaining matrix-origin obstruction.
   By E10G and HGO2R, this eliminates the residual FreeAffineHighTC branch:

                                                78
                                     𝑅FreeAffineHighTC (𝑁 ) = 0.
   Combining with the TC1 global-testing route and origin-degenerate HighTC rerouting gives:

                                     𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 )
   without using X8.
   —

Parameter check 5.47 (E10K.5. Parameter Check: Interface Normalization Supplied by E10Y/E10M/E10K
and Consumed by E10L). The proof above depends on reading F3.6 as complete for actual F3
routing and on excluding post-terminal analytic operations from the list of skeleton generators.
E10Y makes this grammar-completeness statement explicit, E10M proves the no-untagged-rank-
drop theorem on that grammar, and E10K packages the resulting AFF-origin-completeness inter-
face. E10L consumes the already normalized E10Y/E10M/E10K interface when estimating the
terminal GoodAWACK contribution.
    The broader language in the auxiliary Branch B documents is read as follows to avoid reintro-
ducing an untagged AFF operation:

E5 cleanup    Lemma E5 uses the phrase:

                                         affine regrouping
    among "allowed F3 operations."
    E5 is a conditional content-stability lemma for transports whose origin tags have already been
recorded by B1/B3/F3/F4. It does not obtain its meaning from E10L, and it does not introduce a
new terminal GoodAWACK generator.
    Equivalently, in the structural grammar language:

  1. full-rank affine coordinate changes preserve content;

  2. rank-dropping affine maps are allowed only when tagged by fixing/projection, quotient/divisor/local
     origin, CKP, Edge, impossible, or post-terminal analytic slicing;

  3. Cauchy/cube and primitive slicing are post-terminal E10 proof operations, not terminal-
     routing operations creating new GoodAWACK skeletons.

BGS cleanup      Lemma BGS records

                                                rgrp
   as affine regrouping or affine changes of variables.
   In the clean skeleton record rgrp records only:

  1. B3 product grouping choices;

  2. full-rank coordinate changes;

  3. tagged rank drops of the types A2–A5.



                                                 79
BAOC/E10G cleanup The weak BAOC grammar and E10G catalogue do not serve as inde-
pendent terminal generators of arbitrary rank-dropping bounded affine maps. Their broad C5/T5
cell is normalized by the E10Y/E10M/E10K interface before E10L uses it:

  1. full-rank AFF, tensor-safe;

  2. tagged rank-dropping AFF, origin-degenerate or post-terminal analytic;

  3. forbidden untagged rank-dropping AFF.

   —
Remark 5.48 (E10K.6. Output).

       AFF-OC is proved for actual terminal GoodAWACK skeletons by E10Y and E10M.

   Mathematical consequence:

                                     𝑅FreeAffineHighTC (𝑁 ) = 0

   inside the active B1/B3/F3/F4/E5 routing tree.
   This is the structural input used by E10L to close the HighTC class without X8.

E10K.7. Logical Dependencies Internal dependencies: B1, B3, F3, F4, E5, BGS, E10G,
E10H, E10I, E10J, E10Y, E10M, and HGO2R.
   Children served: E10L.

5.13   Part 13. E10L: Clean Branch B closure
Source file: Lemmas/e10l_e10_clean_branch_b_ltx.md.

E10L. Branch B GoodAWACK Theorem without X8

E10L.0. Statement and Role Lemma E10L is the Branch B / GoodAWACK theorem. It
is backed by E10Y and E10X. Lemma E10Y proves completeness of the GoodAWACK routing
grammar for actual B1-origin terminal skeletons. Lemma E10X packages E10Y/E10M/E10K and
proves by a grammar invariant that an actual terminal GoodAWACK skeleton cannot contain an
untagged rank-dropping AFF occurrence. E10S is a verification record for the maintained source
files, not a logical input to the grammar invariant. The TC1 analytic side uses X16C through
BRS/TTH, and Lemma TNG records the complete B1-origin near-global chain showing that TGT
uses X9L-GT only after the MRT/PACK branch and the TTH length lower bound are in force.
     It is the normalized Branch B interface for:

                   E5,   BGS,      BAOC,   E10G,     HGO2R/E10H/E10I/E10J.
   The route is:


       TGD + TNG + BGS/HGO2R + E10Y + E10X + E10K =⇒ 𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 )

   and uses no X8.

                                                80
   Logical dependencies are E5, BGS, HGO2R, TGD, TGT, TNG, MRT, TTD, ROC, BRS, TTH,
X16BRS, X16C, E10Y, E10I, E10J, E10M, E10X, E10K, C1, G8a, H4, and X9L-GT. E10L is used
by I1 and the final assembly.
   —

E10L.1. Setup: Normalized Terminal-Routing Interface                 The interface is the F3-complete
routing interface:

          terminal-routing operations are exactly those listed in F3.6.            (F3-COMPLETE)
   Thus a terminal GoodAWACK skeleton may be generated only by:

  1. the initial B1 typed product variables and B3 product grouping choices;

  2. controlled CRT absorption;

  3. F4 large-divisor decisions;

  4. square-divisor routing;

  5. finite grouping selection/elimination;

  6. terminal LocalDiag detection;

  7. terminal Edge detection by C1 predicates;

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

   In particular:


      arbitrary rank-dropping affine regrouping is not a generic terminal-routing operation.
                                                                                  (No-Untagged-AFF)
    This is not an extra estimate. It is a structural consequence of the proof interface, made explicit
in Lemma E10Y and used in Lemma E10X.
    —

E10L.2. Setup and Proof: E5-Clean Content Stability The phrase "affine regrouping" in
Lemma E5 is read in the following normalized sense, whose completeness for actual GoodAWACK
descendants is supplied by Lemma E10Y.

E5-clean A. Full-rank affine coordinate changes If the affine change has full rank on the
active affine span, then it is allowed. It preserves the TC1/HighTC tensor classification by E10I,
and it preserves controlled content by the usual bounded-minor content calculation already used in
E5.




                                                  81
E5-clean B. Tagged rank-dropping maps A rank-dropping affine map is allowed only if its
rank drop is explicitly tagged by one of the existing origins:

  1. fixing or projection;

  2. fixed divisor quotient;

  3. variable quotient residual;

  4. local/diagonal origin;

  5. CKP origin;

  6. strict C1 Edge origin;

  7. impossible/inconsistent fibre;

  8. post-terminal analytic slicing which does not create a new terminal GoodAWACK skeleton.

    If such a tagged rank drop creates a HighTC relation, then the relation is origin-degenerate and
is rerouted by HGO2R.

E5-clean C. Post-terminal proof operations Cauchy/cube operations, primitive slicing, and
Fourier expansion are post-terminal analytic subroutines inside E10-type estimates. They do not
enlarge the list of terminal-routing operations and do not create new terminal GoodAWACK skele-
tons. For the TC1/HighTC test, the pre-slicing terminal affine vectors are the objects being tested.

Lemma 5.49 (Lemma E10L.1. E5-clean content stability). Under E5-clean A–C, content stability
remains exactly the content stability proved in Lemma E5, but no untagged rank-dropping affine
map is available as a terminal-vector generator.

Proof. Full-rank affine changes are covered by the bounded-minor content argument. Tagged rank
drops are already part of fixing, projection, quotient, local, CKP, Edge, or impossible routing data.
Post-terminal proof operations happen after the terminal skeleton has been fixed and therefore
cannot introduce a new terminal GoodAWACK affine system. These cases exhaust the normalized
meanings of "affine regrouping" by Lemma E10Y. Hence E5 content stability is preserved and
No-Untagged-AFF is enforced.
   —


E10L.3. Setup and Proof: BGS-Clean Skeleton Record                    In the skeleton normal form,
replace the broad phrase

                    rgrp records affine regrouping or affine changes of variables
   by:


  grp records only B3 product groupings, full-rank coordinate changes, and tagged rank drops.
 rclean
                                                                                        (BGS-clean)
   The tagged rank drops are precisely the cases listed in E5-clean B.


                                                 82
Lemma 5.50 (Lemma E10L.2. BGS-clean is equivalent to F3-complete routing). Every actual
terminal GoodAWACK descendant admitted by Lemma BGS has a clean skeleton record.

Proof. By Lemma E10Y, it is enough to check the complete B1/B3/F3/F4/E5 routing grammar.
By B1, the starting variables are product variables and dyadic cells. By B3, only finitely many
product groupings are selected. By F3.6, the subsequent routing-level operations are controlled CRT
absorption, F4 decisions, square-divisor routing, finite grouping selection/elimination, LocalDiag
detection, Edge detection, and terminal class labelling. None of these is an arbitrary untagged
rank-dropping affine map.
    Therefore every rank drop that appears in the terminal record must come from fixing/projection,
quotient/divisor/local data, CKP, Edge, impossible fibres, or post-terminal analytic slicing. These
are exactly the tagged rank drops in BGS-clean. The lemma follows.
    —


E10L.4. Setup and Proof: BAOC/E10G-Clean Affine Cell                 The broad BAOC/E10G affine
cell

                                C5/T5 = bounded affine regrouping
   is replaced by the disjoint trichotomy:

                              C5a/T5a = full-rank AFF, tensor-safe;



       C5b/T5b = tagged rank-dropping AFF, origin-degenerate or post-terminal analytic;


         C5c/T5c = untagged rank-dropping AFF, forbidden by E10Y/F3-COMPLETE.

Lemma 5.51 (Lemma E10L.3. The 4AP-like witness is not an admissible clean terminal cell).
The formal affine family

                                   𝑥,   𝑥 + 𝑟,   𝑥 + 2𝑟,   𝑥 + 3𝑟
   which appears as an interface example in E10G is not, by itself, an admissible C5-clean terminal
GoodAWACK cell.

Proof. If the family is produced by a full-rank change of variables on the active affine span, then
it is tensor-safe by E10I and cannot create a new FreeAffineHighTC certificate.
     If it is produced by a rank-dropping map with a fixing, quotient, local, CKP, Edge, impossible,
or post-terminal analytic tag, then it is origin-degenerate and is handled by HGO2R.
     If it is produced only by an untagged rank-dropping affine parametrization, then it violates the
E10Y-certified F3-complete grammar and is not a terminal-routing operation. Hence the inter-
face family marks exactly the broadness of the C5/T5 wording, not an admissible clean terminal
GoodAWACK cell.
     —




                                                 83
E10L.5. Output Theorem: Branch B GoodAWACK Cancellation

Theorem 5.52 (Theorem E10L.4. GoodAWACK cancellation). For every tagged terminal GoodAWACK
atom produced by the B1/B3/F3/F4/E5 interface, its total contribution is 𝑜(𝑁 ), using the TC1 in-
terfaces MRT/PACK and the X16-Core carrier-slice input. Consequently

                                    𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).                          (E10-clean)
   The proof uses no X8.

Proof. By Lemma TGD, every terminal GoodAWACK atom belongs to exactly one of:

                        TC1-GoodAWACK,            HighTC-GoodAWACK.
   The TC1 part is handled by Theorem TNG-A, the TC1 near-global-or-routed theorem. For
every unrouted B1-origin coarea test produced by TGT, TNG-A gives exactly one of two outcomes:

  1. the test is MRT-admissible, satisfies PACK and 𝐻 ≥ 𝑋(log 𝑋)−𝐵𝜅 , and is therefore an
     admissible input to the near-global Davenport/AP theorem X9L-GT;

  2. before X9L-GT is invoked, TTD/ROC/BRS together with X16BRS/X16C routes the test to
     Edge, LongAP/Local, CKP, LocalDiag, or empty support.

    Thus the TC1 branch is controlled by one theorem-interface, not by a free choice among short
fibres. Combining TNG-A with X9L-GT gives

                                  𝑅TC1-GoodAWACK (𝑁 ) = 𝑜(𝑁 ).
    This uses no X8 and no pointwise shifted short-interval X9L-SI input.
    Now consider the HighTC part. By HGO2R, every origin-degenerate HighTC certificate reroutes
to one of:

                        CKP,       LocalDiag,        Edge,        Impossible.
   These are already handled by G8a, H4, C1, or contribute zero.
   The only formal HighTC class not covered by HGO2R is

                                       FreeAffineHighTC.
   By Lemma E10Y, the finite GoodAWACK grammar is complete for actual terminal skeletons.
By Lemma E10X, actual terminal GoodAWACK skeletons contain no untagged rank-dropping AFF
occurrence, and Lemma E10K gives AFF-origin completeness. Hence:

                                    𝑅FreeAffineHighTC (𝑁 ) = 0.
    Therefore the whole HighTC contribution is either rerouted to already handled classes or empty
as a GoodAWACK class. Combining this with the TC1 estimate gives 𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 ).
The theorem is proved.
    —




                                                84
E10L.6. Dependency Profile         The E10 theorem depends on:


TGD+TGT+TNG+TTD+MRT+ROC+BRS+X16BRS/X16-Core+TTH+X9L-GT+BGS/HGO2R+E10I+E10J+

    together with the standard already-used inputs:

                                X5,   E5-clean,    C1,   G8a,   H4.
    The E10 theorem does not depend on:

                                                  X8.
    The full nilsequence form of X9, the pointwise-fibre TC1 route, and the pointwise shifted X9L-SI
input are not used. The external input is only the near-global Davenport/AP X9L-GT form used
after TTH.
    —
Remark 5.53 (E10L.7. Output).

Branch B / GoodAWACK cancellation is proved using E10Y/E10X/E10K and the near-global Davenport/AP X

    E10L supplies

                                      𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 )
    for the final assembly.

E10L.8. Logical Dependencies External dependency: X9L-GT in the near-global Daven-
port/AP range.
   Internal dependencies: E5, BGS, HGO2R, TGD, TGT, TNG, MRT, TTD, ROC, BRS, TTH,
X16BRS, X16C, E10Y, E10I, E10J, E10M, E10X, E10K, C1, G8a, and H4.
   Children served: I1 and the final proof assembly.


6      Package Dependency Ledger and Synchronization Notes
6.1     Compact Package Dependency Graph
GoodAWACK-Finite-Grammar +– E5: content stability and affine transport +– BGS/HGO2R/BAOC/E10G/E10H
reductions to actual-origin closure +– E10Y: grammar completeness +– E10M: no untagged rank-
dropping AFF +– E10X: finite grammar invariant and closure +– E10K: AFF-origin completeness
+– E10L: Branch B GoodAWACK output

6.2     Local Ledger

      ID                           Uses                            Exports
      E5                           lattice/content algebra         controlled affine transport
      E10Y                         B1/B3/F3/F4/E5 grammar          completeness of skeleton-generating
                                                                   operations
      E10M                         E10Y                            no untagged rank-dropping AFF
      E10X                         E10Y, E10M, E10K                finite grammar closure




                                                  85
    E10K                            E10J/E10I/HGO2R reductions      AFF-origin completeness
    E10L                            TNG/TC1 plus HighTC closure     𝑅GoodAWACK (𝑁 ) = 𝑜(𝑁 )




7     Bibliography
This package has no active external analytic bibliography. It is a structural finite grammar package
using internal routing lemmas and standard finite lattice/content algebra. The relevant mathemat-
ical bibliography is therefore internal: E5 for affine transport and content stability, E10Y for gram-
mar completeness, E10M for no untagged rank-dropping AFF, E10X for finite grammar closure,
E10K for AFF-origin completeness, and E10L for clean Branch B assembly.


8     References
Active logical references for this package:

    1. E5, BGS, HGO2R, BAOC, E10G, E10H, E10I, and E10J, which reduce the HighTC GoodAWACK
       obstruction to actual-origin closure.

    2. E10Y, which proves grammar completeness for actual GoodAWACK skeletons.

    3. E10M and E10X, which exclude untagged rank-dropping AFF and package the finite grammar
       induction.

    4. E10K and E10L, which assemble AFF-origin completeness and the Branch B GoodAWACK
       output.

   Non-logical reproducibility records E10S and E10S-MECH may be read as maintenance aids,
but they are not active logical references for this package.
   No direct external analytic theorem is invoked in this package.




                                                  86
