Norm-fiber densities and relative traces in characteristic two

This preprint studies exact multiplicative-order populations in the norm-one subgroup of a binary quartic extension. It develops effective norm-fiber densities and uniform relative-trace estimates over the intermediate field, and gives a complete classification of empty nonzero trace slices with the exceptional groups C9 at t=8 and C11 at t=32. Further results concern cyclic-convolution distributions, norm transfer and affine companion groups. Classical counting objects and general methods are explicitly credited. The deposit contains the 41-page main paper, the 36-page supplement, editable LaTeX sources, raw mathematical data and exact certificates, deterministic verification programs, and selective Lean sources and actual check records. The data include 1,384,765 element-level records with explicit field parameters, norms, fiber labels and relative traces. Their declared finite coverage is documented; infinite-parameter statements rely on mathematical proofs. Version v17 (28 October 2026) adds checked rational a/gamma bijections, exact-order component equivalence, and transfer of the original M_c count using Algebra.norm and Algebra.trace in a genuine finite-field tower. Nine Lean modules check 129 theorem/lemma declarations and 33 definitions. Concrete field certificates, fixed-generator conversion, the complete exceptional-case assembly, geometric estimates, the sieve and infinite tail remain outside the formal build. Neither Theorem 5.1 nor Theorem 5.4 is claimed wholly formalized. This exact version was published on GitHub on 28 October 2026: https://github.com/63331849121/yijing-mathematical-structures/releases/tag/paperA-v2026.10.28-v17 . An earlier expanded preprint version was posted there on 26 October 2026. This is a separate work from the earlier Singer-layer note (10.5281/zenodo.22731492); that DOI is not reassigned. The work is a research preprint and has not been externally peer reviewed. Manuscripts are CC BY 4.0; verification code and Lean sources retain MIT terms, and bundled fonts retain their separate licenses.