            GoodAWACK Finite Grammar Theorem Package
                                          Denis Saltykov

                                             May 2026


                                              Abstract
         This note isolates the finite combinatorial part of the GoodAWACK closure. It proves that
     actual terminal GoodAWACK skeletons are generated by a finite B1/B3/F3/F4/E5-clean rout-
     ing grammar, that this grammar preserves a no-untagged-rank-drop invariant, and therefore
     that no terminal GoodAWACK skeleton contains an untagged rank-dropping affine regroup-
     ing. As a consequence the FreeAffineHighTC residual is empty, and the HighTC-GoodAWACK
     branch is routed to already handled terminal classes or contributes zero.


Contents
1 Scope                                                                                              1

2 Routing Records and Terminal Skeletons                                                             2

3 Allowed Grammar                                                                                    2

4 Grammar Completeness                                                                               3

5 Finite Grammar Invariant                                                                           4

6 No Untagged AFF in Actual GoodAWACK                                                                4

7 Formal Free-Affine Witnesses                                                                       5

8 HighTC-GoodAWACK Closure                                                                           5

9 Role of the E10S Reproducibility Record                                                            5

10 Output for E10L                                                                                   6

11 Logical Dependencies                                                                              6


1   Scope
The theorem concerns actual terminal GoodAWACK skeletons. An actual skeleton is a descendant
of the proof-tree construction
                                   B1 −→ B3 −→ F 3/F 4,
with E5 used only as clean content stability for records already generated by that construction.
The theorem does not classify arbitrary bounded affine systems written down after the fact.

                                                  1
     The goal is the structural implication

    actual terminal GoodAWACK skeleton =⇒ no untagged rank-dropping AFF occurrence.              (1.1)

The analytic TC1 route is not part of this package. This package handles the finite grammar and
HighTC structural closure.


2     Routing Records and Terminal Skeletons
An actual routing record is a tuple

                                        r = (V, C, L, Q, τ, orig, W ),

where:

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

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

    3. L is the finite list of visible affine forms;

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

    5. τ is the current routing tag;

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

    7. W is the bounded or polylogarithmic weight data.

     A terminal GoodAWACK skeleton is the terminal record

                                S = (B, Γ, r, ΛS , ΩS , LS , MS , origS , WS )

produced by this routing record when the terminal label is GoodAWACK.
   For terminal affine forms Lρ (z) = ℓρ · z + cρ , the TC1/HighTC test uses the tensors

                                                Qρ = ℓρ ⊗ ℓρ .

After terminality these vectors and tensors are fixed routing data. Later analytic operations may
test or restrict the fixed terminal object, but may not replace its terminal vector list and treat the
replacement as a new terminal GoodAWACK skeleton.


3     Allowed Grammar
Define the finite GoodAWACK grammar GGA as follows. A state is a tuple

                                           s = (V, L, C, Q, T , O),

where O is the origin record for rank-changing operations.
    The start states are exactly the B1/B3 grouped product cells. The transition set consists of the
following operations.


                                                       2
    Transition                      Allowed effect                              Required tag or outcome
    B1 start-state creation         creates product variables, dyadic cells     start-state origin
                                    and weights
    B3 finite grouping              selects one finite grouped candidate        B3 grouping origin
    controlled CRT restriction      finite-index full-rank restriction or in-   CRT or empty
                                    compatible fibre
    fixed-divisor quotient          quotient by a recorded fixed divisor        FixedDiv
    variable quotient residual      quotient/divisor residual selected by       VarQuot or routed tag
                                    F4
    square-divisor routing          Edge, controlled divisibility, or empty     Edge or CRT
                                    state
    grouping               selec-   finite candidate selection or removal       B3/F3 grouping origin
    tion/elimination
    local/diagonal/gcd detection    equality, proportionality, repeated         LocalDiag
                                    form, or forced local relation
    CKP-balanced detection          balanced     bilinear     Kloosterman-      CKP
                                    fraction structure
    strict saving or boundary de-   C1 Edge, short-volume, boundary,            Edge
    tection                         high-frequency or small-conductor
                                    case
    full-rank affine transport      injective on active and terminal            no rank-drop tag needed
                                    tensor-test spans
    tagged rank-dropping trans-     rank drop inherited from an earlier         inherited allowed tag
    port                            routing origin
    terminal labelling              labels Edge, CKP, GoodAWACK, Lo-            terminal label
                                    calDiag or LongAP/Local
    post-terminal analytic opera-   estimates or tests a fixed terminal ob-     PostTerminalNonGenerator
    tion                            ject



    There is no transition whose output is an untagged rank-dropping affine regrouping.


4     Grammar Completeness
Theorem 1 (Completeness of the GoodAWACK routing grammar). Every actual-generated op-
eration that can generate or modify an actual terminal GoodAWACK affine skeleton is one of the
transitions of GGA .
Proof. B1 supplies only fixed-depth Heath–Brown product variables, dyadic cells and exact con-
volution weights. B3 supplies only a finite list of product-grouping start states. Neither layer
introduces a free affine rank drop.
    F3 and F4 perform the complete pre-terminal routing. The generic F3 operations are controlled
CRT absorption, the F4 large-divisor decision, square-divisor routing, finite grouping selection or
elimination, terminal LocalDiag detection, terminal Edge detection, and terminal class labelling.
F4 exhausts ordinary divisor and quotient decisions. Any quotient, local-dependence, CKP, Edge,
impossible, or continuation outcome receives a recorded tag before terminality.
    E5 is applied only to records already produced by B1/B3/F3/F4. In the clean interface it is
either full-rank on the active affine span and on the terminal tensor-test span, or else it inherits
an already recorded rank-drop origin. Thus E5 is content stability, not an independent terminal
generator.

                                                       3
    After terminal labelling, Cauchy–Schwarz, cube expansions, Fourier expansions, coarea tests,
TC1 testing, BRS/X16 estimates, Davenport/AP estimates and local projection arguments act only
on the fixed terminal object. They cannot produce a new B1/B3/F3/F4 descendant and cannot
replace the terminal tensor-test vectors.
    These cases exhaust the actual B1-origin construction. Hence every operation that generates a
terminal skeleton belongs to GGA .


5    Finite Grammar Invariant
The allowed rank-drop tags are

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

Theorem 2 (No-untagged-rank-drop invariant). For every state reachable in GGA , every rank-
dropping affine operation visible in that state carries one of the tags in (5.1). Consequently, a
reachable terminal GoodAWACK skeleton contains no untagged rank-dropping AFF occurrence.

Proof. We argue by induction on the length of the grammar derivation.
    At length zero, the state is a B1/B3 grouped product cell. It contains product variables,
dyadic restrictions and grouped candidates, but no rank-dropping affine operation. The invariant
is therefore true.
    Assume the invariant for a reachable state and apply one transition. If the transition is fixing
or projection, the origin tag is Fix/Proj. If it is controlled CRT restriction, then either the fibre is
incompatible and disappears, or the operation has the tag CRT. A fixed-divisor quotient has the
tag FixedDiv. A variable quotient residual has the F4 tag VarQuot, unless it routes to LocalDiag,
CKP, Edge, LongAP/Local or empty support.
    If the transition detects a local, diagonal, gcd, repeated-form or proportional relation, the state
leaves GoodAWACK with tag LocalDiag. If it detects balanced multiplicative structure, the state
leaves GoodAWACK with tag CKP. If it detects strict saving, short volume, square-divisor saving,
high frequency, small conductor or a boundary case, the state leaves GoodAWACK with tag Edge.
    A full-rank affine transport has no rank drop. A rank-dropping E5 transport is allowed only
when the rank drop is inherited from an already recorded routing origin, so the induction hypothesis
supplies the tag. Terminal labelling is a label and performs no coordinate operation.
    Finally, a post-terminal analytic operation is allowed only after the terminal tensor-test vectors
are fixed. It can restrict a sum or introduce testing variables, but it cannot change the terminal
routing record. Hence any rank drop that occurs in a post-terminal analytic calculation is tagged
PostTerminalNonGenerator and cannot generate a new terminal GoodAWACK skeleton.
    Thus every transition preserves the invariant. The theorem follows.


6    No Untagged AFF in Actual GoodAWACK
Corollary 1 (No untagged rank-dropping AFF). Let S be an actual terminal GoodAWACK skele-
ton. Then every rank-dropping affine occurrence in S is tagged by one of (5.1).

Proof. By the grammar-completeness theorem, S is reachable in GGA . By the invariant theorem,
every rank-dropping affine operation in any reachable state is tagged. Hence an untagged rank-
dropping AFF occurrence cannot occur in S.


                                                    4
7    Formal Free-Affine Witnesses
The formal 4AP-like family
                                      Yi = x + ir,       0 ≤ i ≤ 3,
with coefficient vectors ℓi = (1, i), satisfies a quadratic tensor relation

                              ℓ0 ⊙ ℓ0 − 3ℓ1 ⊙ ℓ1 + 3ℓ2 ⊙ ℓ2 − ℓ3 ⊙ ℓ3 = 0.                    (7.1)

This family is useful as an interface witness: it shows that a broad phrase such as “bounded affine
regrouping” would be too large if it were read without the actual routing origin.
    It is not, by itself, an actual terminal GoodAWACK obstruction. If it arises from a full-rank
transport, the TC1/HighTC classification is invariant under that transport. If it arises from a
tagged rank drop, the resulting HighTC certificate is origin-degenerate. If it arises only from an
untagged rank-dropping affine parametrization, it is not generated by GGA and is not an actual
terminal GoodAWACK skeleton.


8    HighTC-GoodAWACK Closure
HGO2R routes every origin-degenerate HighTC certificate to one of

                          CKP,        LocalDiag,         Edge,       Impossible.              (8.1)

Those outputs are handled outside GoodAWACK by the CKP, local, Edge and zero branches.
   The only remaining HighTC residual is FreeAffineHighTC: a high-true-complexity certificate
generated by a rank-dropping affine operation with no allowed origin tag.

Theorem 3 (FreeAffineHighTC is empty). For actual terminal GoodAWACK skeletons,

                                       RFreeAffineHighTC (N ) = 0.

Proof. Suppose a FreeAffineHighTC skeleton existed. By definition its HighTC tensor relation
would have to be produced by an untagged rank-dropping affine operation; otherwise HGO2R
would classify it as origin-degenerate and route it to one of (8.1).
   But by the preceding corollary, no actual terminal GoodAWACK skeleton contains an untagged
rank-dropping AFF occurrence. Therefore the assumed FreeAffineHighTC skeleton is not an actual
B1-origin terminal GoodAWACK descendant. Hence the FreeAffineHighTC contribution is empty.


Corollary 2 (HighTC-GoodAWACK closure). Every HighTC-GoodAWACK terminal contribu-
tion is either routed by HGO2R to CKP, LocalDiag, Edge or Impossible, or belongs to the empty
FreeAffineHighTC class. Thus the HighTC-GoodAWACK contribution contributes no unresolved
GoodAWACK mass.


9    Role of the E10S Reproducibility Record
The conceptual proof is the grammar-completeness theorem plus the induction invariant above.
E10S-MECH is a reproducibility record for the source layer: it lists the proof files checked, their
hashes, the search terms, and the occurrence-to-class map for all rank-affecting language in the
Branch B / GoodAWACK proof-source files.

                                                     5
    The E10S record is not a proof by search. Its function is narrower: it makes the finite source-
layer verification reproducible and records when the check must be refreshed. If a Branch B /
GoodAWACK source file changes, a new rank-changing term is introduced, or the F3/F4 routing
grammar changes, the hash record and occurrence classification must be updated before the E10S
record is cited again.


10    Output for E10L
The package supplies the structural input

                  E10Y + E10X + E10M + E10K =⇒ RFreeAffineHighTC (N ) = 0.

Together with HGO2R, this closes the HighTC-GoodAWACK branch. E10L combines this HighTC
closure with the separate TC1 near-global-or-routed theorem TNG and the near-global X9L-GT
input to prove
                                   RGoodAWACK (N ) = o(N ).


11    Logical Dependencies
Internal dependencies: B1, B3, F3, F3A, F3T, F4 and E5; BGS and HGO2R; BAOC and E10G–
E10J as the reduction chain isolating FreeAffineHighTC; E10Y, E10S-MECH, E10M, E10X and
E10K; C1, G8a and H4 as destinations for routed outputs.
    External dependencies: none. This package is combinatorial and structural.
    Children served: E10L and the GoodAWACK theorem.




                                                6
