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

Preprint · Florian Hellwig

- Archive id: arxiv:2610.36534
- Published: 2026-10-27
- arXiv: https://arxiv.org/abs/2610.36534
- Citations: 0
- Source URL: https://arxiv.org/abs/2610.36534
- PDF: https://arxiv.org/pdf/2610.36534
- Provenance: arxiv

## Abstract

We study completely normal elements of $\\mathbb{F}\_{q^n}$ over $\\mathbb{F}\_q$, 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\\le q$ is due to Garefalakis and Kapetanakis, this confirms the conjecture of Morgan and Mullen (1996) that every $\\mathbb{F}\_{q^n}$ contains a primitive element that is completely normal over $\\mathbb{F}\_q$. The same estimates give two further results. First, Hachenberger's conjectured lower bound $(q-1)^{n'}q^{(p^a-1)n'}$ for the number of completely normal elements, where $p$ is the characteristic and $n=p^an'$ with $p\\nmid n'$, holds for all pairs $(q,n)$; it was known for regular pairs. Second, primitivity and complete normality are asymptotically independent: as $q^n\\to\\infty$, the number of primitive completely normal elements is $(1+o(1))\\,\\varphi(q^n-1)/(q^n-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\\le q$ and an explicit bound of Rosser and Schoenfeld as axioms and relies on Lean's compiler and interpreter for the large computations.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.