Internal proof and artifact review

September 9, 2026. Conducted within the same AI-assisted task; no independent human or subagent review is claimed.

Proof audit

1. Functional degree and support. A nonconstant nonzero function admits a nonzero first difference. Commutativity of translations lowers the annihilating-difference bound by one. Its support lies in the union of two translates of the original support. Constants and trivial domain groups are covered explicitly. The codomain may be any finite abelian group.
2. Literal word formula. The negative letter contributes minus rho(prefix minus its top coordinate), by the actual inverse formula. This verifies the character expansion for arbitrary signs, repeated variables, zero exponent sums, and the empty word. No free-group automorphism normal form is assumed.
3. Constrained top tuples. The exponent-sum map is a homomorphism because T is abelian. Each nonempty fibre is the actual coset t0+ker(alpha), with probability 1/D. No parametrization by field coordinates is used.
4. Leading coefficient. The minimum is taken over all coefficients and all tuples in that one top fibre. One coefficient attaining it defines a nonzero function into R/(pi^(s+1)). Every difference of each character introduces a principal-ideal factor. The support lemma applies to this quotient-ring-valued function itself, not to a chosen digit function.
5. Common image and uniformity. All conditional base images are contained in pi^s M. On at least 2^(-s) of the top tuples one coefficient is pi^s times a unit, so that entire subgroup is attained. Uniformity is only invoked for a fixed additive homomorphism M^k to its image. It is not assumed across arbitrary quotient fibres.
6. Module length. Reduction by Ann(M) is valid for nonzero M and preserves the residue field. Faithfulness makes every layer before the nilpotency index nonzero; otherwise iteration kills pi^(ell-1)M. The index is at least Q^s, compensating for 2^s. The zero module and field cases are explicit.
7. Split cover. If c=b^q has order p^h, b has order q p^h. The scalar u obeys u^q=1 after faithful reduction and uc=c. The cover map (m,j) to m b^j is surjective and has the central cyclic kernel generated by (-c,q), of exactly p^h elements. The case c=0 gives a trivial kernel.
8. Attained lift count. Multiplication of inputs by central kernel elements changes the word by their exponent-sum powers. Therefore at least |K^a| lifts of every attained quotient value are attained. This does not assert that all lifts are attained. Uniform pushforward of input tuples gives the probability sum over the whole fibre.
9. Essential compensation. The split estimate uses D, not the whole complement order. The difference max(e+h-t,0)-max(h-t,0) is at most e, including t=infinity. This is the precise step that avoids an invalid general quotient-inheritance argument.
10. Corollaries. A p-power-order unit of Z/p^a reduces to one modulo p; characteristic two is included. An elementary abelian kernel with cyclic quotient yields (A-I)^(p^e)=0, hence a truncated-polynomial-ring module. Sylow subgroups of a nilpotent metacyclic group are metacyclic, and word probabilities multiply. Wreath products have an elementary abelian base and cyclic complement. No classification theorem is needed.
11. Outside-prior-class example. For C16 semidirect_3 C4 the lower central terms are 2^(j-1)M, of orders 8,4,2,1. The geometric sums for every top residue show exponent 16. There is no cyclic maximal subgroup of order 32. This witness is justified in the proof and also checked separately by enumeration.

No universal step is delegated to finite testing. No gap was identified in this internal review. External correctness and historical-priority review remain outstanding.

Exact finite checks

The supplied scripts are unchanged copies of the versions that produced the recorded results. They use Python and NumPy and write JSON beside themselves. The second script imports the first by its exact filename. Run from any directory:

python3 q43-chain-ring-check.py
python3 q43-cyclic-extension-check.py

The split checker covers 12 models, 405 full distributions, 80,843,650 literal word evaluations, and 10,980 attained fibres. Its SHA-256 is db6593cb912a7d30678f98ab9a2c971588e00792a8c919c3a126753d2eb75915.

The nonsplit checker covers 10 models, 340 full distributions, 29,608,165 literal evaluations, and 9,322 attained fibres. Its SHA-256 is c7b3715cffd6dbe936aeb7cfe7e3dec4e43bb41326bf6e422058ff5b34c097f6. It checks exact distribution pushforward, centrality, homomorphism pairs, and attained-lift counts. The largest quotient has order 729 and its cover order 2187; that cover's 4,782,969 multiplication pairs satisfy the homomorphism identity.

Together: 22 models, 745 distributions, 110,451,815 literal word evaluations, and 20,302 attained fibres. The records include seeds and whether each associativity check is exhaustive or sampled. Tested words do not exhaust all words. Polynomial and integer chain rings, module lengths, complement ranks, characteristic two, quaternion extensions, and zero/deep coefficients are represented. Residue fields of nonprime order are handled by the proof, not by these particular test families.

Artifact review

The manuscript compiles to eight pages with no reported overfull boxes or undefined references. All eight full-page PNGs were inspected. The title, byline, theorem statements, displays, page transitions, and bibliography are legible, with no clipping or overlap. The final page contains the bibliography and intentional white space.

The full Markdown edition includes Henry Zweiman's byline. The converter verifies the source math sequence (312 expressions), theorem/proof markers, references, and semantic roundtrip. The Markdown math renderer accepts 318 expressions, including proof-ending squares, with zero errors. Hashes and machine checks are in the adjacent JSON records. PDF and source copies must match these records before publication.

The first conversion attempt was launched before the PDF existed and failed without producing a completed conversion. The successful run occurred after compilation. No failed attempt is counted as a successful validation.