Resolvent Components of Completely Normal Elements and the Morgan-Mullen Conjecture

We study completely normal elements of Fqⁿ over Fq, that is, elements that are normal over every intermediate field, through partial Lagrange resolvents. In these coordinates, complete normality splits into independent components, in a way closely related to Hachenberger's decomposition theory. Our main tool is a structure theorem for the components; together with a finite computation, it shows that every component has weight (the sum of the probabilities that its conditions fail) at most $3/4$, uniformly in n. Combined with the classical character-sum method, this gives an explicit sufficient criterion for the existence of a primitive completely normal element. We verify the criterion for all $n>q$ except $70$ pairs $(q,n)$, which we settle with explicit elements found by computer. Since the case n≤ q is due to Garefalakis and Kapetanakis, this confirms the conjecture of Morgan and Mullen (1996) that every Fqⁿ contains a primitive element that is completely normal over Fq. The same estimates give two further results. First, Hachenberger's conjectured lower bound (q-1)n'q(pᵃ-1)n' for the number of completely normal elements, where p is the characteristic and n=pᵃn' with p n', holds for all pairs $(q,n)$; it was known for regular pairs. Second, primitivity and complete normality are asymptotically independent: as qⁿ→∞, the number of primitive completely normal elements is (1+o(1))\,φ(qⁿ-1)/(qⁿ-1) times the number of completely normal elements (for fixed n this was known). Our arguments for $n>q$ and for both further results, including every computer-assisted step, are formalised in Lean 4 with Mathlib; the formalisation takes the case n≤ q and an explicit bound of Rosser and Schoenfeld as axioms and relies on Lean's compiler and interpreter for the large computations.