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

1.2 Results

• Every F_q^n contains a primitive element completely normal over F_q, completing the conjecture beyond the previously proved case n ≤ q.The n ≤ q case is due to Garefalakis and Kapetanakis; this paper proves n > q.Source: §1 · pp. 1–2, §1.2 · p. 3

1.5 Idea of the proof

• Independent resolvent components yield a lower bound on complete-normality density from their individual weights, enabling the character-sum method uniformly in n.Essential conditions whose fibres meet no common Frobenius orbit are independent; the method bounds each component’s weight rather than the potentially unbounded total weight.Source: §1.2 · p. 3, §1.5 · p. 6

1.2 Results

• The number CN_q(n) satisfies Hachenberger’s conjectured lower bound for every q and n, with equality exactly when n′ divides q − 1.The bound was previously known for regular pairs.Source: §1.2 · p. 4
• PCN_q(n)/(θ CN_q(n)) tends to 1 as q^n grows, uniformly over pairs (q, n), where θ = φ(q^n − 1)/(q^n − 1).For fixed n, convergence was already known; the result adds uniformity in n.Source: §1.2 · p. 4

1.3 Computer-assisted steps and formal verification

• The proof for n > q and the computer-assisted steps for the further results are formalised in Lean 4 with Mathlib.The formalisation assumes the n ≤ q case and a Rosser–Schoenfeld bound as axioms; large computations also rely on Lean’s compiler and interpreter.Source: §1.3 · p. 4

1.5 Idea of the proof

• For q ≥ 8, the criterion holds beyond explicit thresholds of at most 171, and for q ≥ 32 the threshold is at most 14.Sharper local bounds give M(q,n) ≤ 0.41n, 0.62n, and 0.75n for q = 2, 3, and 4, respectively, for all but finitely many n.Source: §1.5 · p. 7
• For n>q, criterion (∗) holds with at least one bit to spare except for 70 pairs, settled by explicit primitive completely normal elements.All exceptions have q ≤ 19 and n ≤ 378; the case n ≤ q follows from Garefalakis and Kapetanakis [38, Theorem 1.3].Source: §1.5 · p. 8
• The asymptotic-independence corollary bounds the relative error by 2^-∆, where ∆ is the margin in criterion (∗).The large-n estimates make ∆ grow at least linearly in n, uniformly in q; for bounded n and large q, a cruder estimate suffices.Source: §1.5 · p. 8
• Corollary 8.8 proves Hachenberger’s lower bound for the number of completely normal elements by comparing local contributions of S with the bound’s normalized form.The sum S splits into local contributions indexed by roots of unity, paralleling the decomposition of M.Source: §1.5 · p. 8

2 Coordinates by partial resolvents

• Partial resolvents split the Frobenius sums by residues modulo p^a, supplying coordinates for all intermediate-field levels when p divides n.When p does not divide n, they reduce to ordinary Lagrange resolvents.Source: §2 · pp. 8–9
• For uniformly random w, coordinates belonging to distinct pair orbits are independent and uniform in their respective coordinate spaces.The partial resolvents remain injective coordinates even when p divides n, when the full resolvents alone no longer determine w.Source: §2 · pp. 8–9
• Normality over F_qd is equivalent to every level-d fibre sum being nonzero; each condition's kernel has codimension lcm(d, o(d, k)).For essential conditions, the codimension is o(d, k).Source: §2 · p. 10
• Each condition kernel is the zero set of one fibre sum involving only coordinates in its support, enabling independence arguments across disjoint supports.The resolvent formulation expresses the classical invariant-subspace criterion in these coordinates.Source: §2 · p. 11
• Complete normality requires avoiding only the kernels of essential conditions, rather than those of every condition.Each nonessential condition's kernel is contained in the kernel of an essential condition.Source: §2 · p. 11
• For n > 1, levels carrying essential conditions match Hachenberger and Hackenberg's (q, n)-essential set; the reduction also identifies needed targets individually.At level d, only targets whose order e satisfies d | ord_e(q) are needed.Source: §2 · p. 12

3 Components and the product formula

• Components are equivalence classes of essential conditions linked by shared pair-orbit support; their supports are disjoint across components.The conditions in a component can also be characterized by fibres meeting common Frobenius orbits.Source: §3 · pp. 12–13
• The component pass-events are independent, so the completely normal density is their product and is at least the product of one minus each component's weight when all weights are below 1.The product formula is exact; the lower bound uses a union bound within each component.Source: §3 · pp. 12–13
• Every component without a codimension-one condition has weight at most W(q) < 1, uniformly in n.This bound supplies the component-weight control used to lower-bound the density of completely normal elements.Source: §3 · p. 13
• A codimension-one essential condition forms a singleton component; every other component has no codimension-one condition.The weights of components other than these singletons sum to the weight of all essential conditions of codimension at least two.Source: §3 · pp. 13–14

4 The counting criterion

• The character-sum argument takes the number of completely normal elements as its main term and bounds the nontrivial-character contribution using L.The coefficient-function norm is at most L, and the nonzero-frequency contribution is bounded by θβ(L−δ_n).Source: §4 · pp. 14–15
• The criterion uses L ≤ 2^M(1−1/q)^M1, where M counts essential conditions and M1 counts those of codimension 1.L is the product over essential conditions of (1−q^−o(C)).Source: §4 · p. 15
• If (q^n−1)δ* ≥ 2^ω q^(n/2)L, then (q, n) has the Morgan–Mullen property.Here ω = ω(q^n−1), and δ* is a lower bound for the density δ_n.Source: §4 · pp. 14–15
• The sufficient criterion replaces δ_n by its lower bound δ*; the product formula and component-weight bound supply that lower bound.The remaining inputs include ω(q^n−1) and M, which are treated in Sections 5 and 6.Source: §4 · pp. 14–15

5 Prime factors of qn −1 and essential types

• The section expresses the number M of essential conditions and their codimension-at-least-2 total weight S as finite sums over essential types.It also bounds the number of conditions at each codimension.Source: §5 · pp. 15–16
• The number of distinct prime factors ω(q^n−1) is bounded using the counts t_k of prime divisors with ord_ℓ(q)=k.t_k is the largest number of smallest primes congruent to 1 modulo lcm(2,k) whose product is at most Φ_k(q).Source: §5 · pp. 15–16
• For each essential type (d, e), there are ν_d,e = dφ(e)/ord_e(q) conditions, each of codimension ord_e(q).The conditions correspond to orbits of ξ ↦ ξ^(q^d) on the elements of order e.Source: §5 · p. 16
• For q=4 and n=6, the four essential conditions comprise one of codimension 1 and three of codimension 2, with total weight S=3/4.The three codimension-2 conditions form one component of weight 3/4.Source: §5 · p. 16

6 The number of essential conditions

• M(q,n)≤n for every pair (q,n), by bounding the local contributions to M in terms of q, v_p(n), and root degree.The proof reduces the bound to estimates for ρ(η)/p^a and sums over η∈μ_n′.Source: §6 · pp. 16–18
• For q≤4, sharper estimates use exact local maxima on finite ranges and tail bounds, with a hand proof for q=4 and odd n.The target bounds are λn with λ=0.41, 0.62, and 0.75 for q=2, 3, and 4, respectively, outside specified finite sets.Source: §6 · pp. 18–19
• For q=4, M(4,n)≤3n/4 for all n≥12.The proof first gives separate bounds for even and odd n.Source: §6 · p. 18
• For q=3 and 3|n, M(3,n)≤0.5983n; for 3∤n, M(3,n)≤0.6n+0.4 gcd(n,6560), hence M≤0.62n for n≥131200.The respective bounds use local estimates with and without a finite exceptional set of degrees.Source: §6 · p. 19
• For q=2, M(2,n)≤0.41n for every n≥3780.The estimate combines exact local maxima on finite ranges with a tail bound.Source: §6 · p. 19

Theorem 7.2 (structure of components)

• The structure theorem places component fibres inside µK and bounds their target orders, levels, codimensions, and the least common multiple of their p-free levels.The relevant K depends only on q and the minimal codimension; the fibres of the minimal-codimension condition lie in µK.Source: §7 · p. 20

Corollary 7.6

• Corollary 7.6 bounds component weight using either a least admissible K or a crude explicit choice, with both bounds depending only on q and the minimal codimension.The least admissible choice is used for q = 2, q = 3 with o0 ≤ 374, and the finite reduction; the crude choice is used for q ≥ 4 and q = 3 with o0 ≥ 375.Source: §7 · pp. 21, 23

Proposition 7.7

• For fixed q and minimal codimension o0, Proposition 7.7 reduces every component to one for an exponent n0 dividing N**, preserving its conditions and weight.Here N** = lcm(K, O∞), with K and O∞ supplied by the least admissible construction.Source: §7 · p. 23

Theorem 7.8 (weights)

• Every component without a codimension-one condition has weight at most W(q), with W(2) = 3/4 and W(3) = 4/9.These bounds are attained for (q, n) = (2, 6) and (3, 8), respectively.Source: §7 · pp. 24–25
• Exact computation handles the four exceptional pairs (q, o0) = (2, 3), (2, 6), (3, 2), and (3, 4), and establishes the required weight bounds.The computation reduces to divisors of N**; the resulting W(2) = 3/4 and W(3) = 4/9 bounds are attained at (q, n) = (2, 6) and (3, 8).Source: §7 · pp. 24–25

7 Structure of components

• The formal bounds check Tq(o1) ≤ W and (1 + 1/o1)^3 · 2.83 ≤ q at specified base cases, then use that Tq decreases in q and o0.The passage checks (q, o1, W) = (q, o1(q), W(q)) for 4 ≤ q ≤ 31, (3, 375, 0.051), and (32, 7, 0.0118).Source: §7 · p. 25
• For q ≥ 32 and 2 ≤ o0 ≤ 6, Wcr(q, o0) is at most 0.0118.The bound is evaluated at q = 32 using a cutoff of o0 + 41; it decreases as q increases.Source: §7 · p. 25

8 The main theorem

• Theorem 8.1 converts a component-weight bound into an explicit sufficient criterion, verified analytically for large n and computationally for remaining pairs with q < n.The computation leaves 70 pairs with less than one bit to spare; the other accepted pairs have at least one bit of margin.Source: §8 · pp. 25, 27, 28
• For the 70 exceptional pairs, explicit elements are certified to be primitive and normal over every intermediate field, completing the Morgan–Mullen property.The certificates give an element of order q^n − 1 and check normality over each F_{q^d} for d | n.Source: §8 · p. 28
• Every finite field F_{q^n} contains a primitive element completely normal over F_q.For n ≤ q, the proof invokes [38, Theorem 1.3]; for n > q it applies the criterion or explicit certificates.Source: §8 · p. 29

The numbers CNq(n) and PCNq(n)

• For every prime power q and n ≥ 1, CN_q(n) ≥ (q − 1)^n′ q^(p^a−1)n′, with equality if and only if n′ divides q − 1.Here n = p^a n′ with p not dividing n′; this proves Hachenberger’s conjectured lower bound for all pairs.Source: The numbers CNq(n) and PCNq(n) · pp. 29–30
• As q^n tends to infinity, PCN_q(n)/(θ CN_q(n)) tends to 1, so primitivity and complete normality are asymptotically independent.Here θ = φ(q^n − 1)/(q^n − 1); the convergence is uniform as n grows or as q grows.Source: The numbers CNq(n) and PCNq(n) · pp. 30–31
• A margin Δ0 in (∗) gives relative error below 2^-Δ0; for Proposition 8.4 pairs except 70, it is below 1/2, and Δ0 = 0 guarantees positivity.The relative error is |PCNq(n)/(θ CNq(n)) − 1|.Source: The numbers CNq(n) and PCNq(n) · pp. 31–32
• For every n, the completely normal proportion among primitive elements differs from δn, its proportion among all elements, by less than 20 q^-1/4.Source: The numbers CNq(n) and PCNq(n) · p. 32
• As q grows with n/q → 0, PCNq(n)/φ(q^n − 1) → 1; for n = q − 1, the ratio instead tends to 1/e.Source: The numbers CNq(n) and PCNq(n) · p. 32
• Hachenberger proved convergence for fixed n [53, Theorem 2], while his estimate for n ≥ 2 gives convergence whenever σ1(n) n log q = o(q) [53, (7)].Source: The numbers CNq(n) and PCNq(n) · p. 32

9 Computations

• Table 1 lists each computation-dependent statement, what is computed, and the program that carries it out.The reported run times were measured on one core of a laptop; the programs are short, self-contained Python 3 programs.Source: §9 · p. 32, Table 1 · p. 33

Formal verification

• The proof for n > q and Corollaries 8.8 and 8.9, including computer-assisted steps, is formalised in Lean 4 with Mathlib.The formalisation takes the case n ≤ q and a Rosser–Schoenfeld bound as axioms, and relies on Lean's compiler and interpreter for large computations.Source: Formal verification · p. 32

Code and data availability

• The repository provides the Python programs, library versions, and 70 certificates, and is archived on Zenodo.The Lean formalisation is available in the repository.Source: Code and data availability · pp. 32–33

Example setup

• The union bound gives no information for (2, 4599): its 1145 essential conditions have total weight about 3.41, while they form 63 components.The example is illustrative, not part of the proof; Proposition 8.4 settles this pair.Source: §10 · pp. 33–34

Component structure

• The component of the level-one condition with target of order 511 has weight approximately 0.0254, from the stated level-9 conditions.The passage gives the exact expression as 6663/218.Source: §10 · p. 34

Structure-theorem comparison

• The example's component has minimal codimension 9, and its stated level and codimension bounds are attained for o = 9.For o = 18, the first bound is 81 conditions while the passage reports an actual count of 7; 54 of the 81 bound conditions come from levels 2, 6, and 18, which require 2 | n.Source: §10 · p. 34

Criterion checks

• For this pair, Theorem 4.2(b)'s sufficient condition holds with a margin of about 901 bits.The example also reports that the cruder criterion of Theorem 8.1(b) holds with a margin of about 894 bits.Source: §10 · p. 34

Primitive count estimate

• The first inequality of Corollary 8.9(a) bounds the relative error in approximating PCN₂(4599) by θ CN₂(4599) by less than 2^-900.The exponent is the margin found for Theorem 4.2(b).Source: §10 · p. 35

Checks against definitions

• For 30 selected pairs with q^n ≤ 65536, the definition-based complete-normality test agrees with both the essential-fibre-sum test and the all-fibre-sums test.The pairs include cases with p | n and pairs that are not completely basic, including (2, 12), (3, 8), and (5, 6).Source: §11 · p. 35

Formula checks

• The passage states that the program checks the lower bound CN_q(n) ≥ (q − 1)^n′ q^(p^a−1)n′.Source: §11 · p. 35

Component-structure checks

• Across the tested ranges, about 1.1 · 10^5 components were checked against Theorem 7.2, with no violation found.The tests covered specified small q values through n bounds from 3000 for q = 2 to 300 for q ≥ 16, plus random n values up to 20 times those bounds.Source: §11 · p. 35

Example counts

• The order test accepted exactly φ(q^n − 1) elements, while the rank test accepted 6, 16, and 360 elements for PCN₂(6), PCN₃(4), and PCN₂(12), respectively.Those three counts match values obtained by a different program.Source: §11 · p. 35

Proof dependencies

• The proof uses the conjecture's n ≤ q case and Rosser–Schoenfeld's explicit lcm bound as external results, alongside the computations in Section 9.The paper reports exact integer or rational arithmetic except for specified floating-point checks.Source: §12 · p. 36

Sharpness and scope

• The component weight bounds are attained for q = 2 when 6 | n, with weight 3/4, and for q = 3 when 8 | n, with weight 4/9.Uniformity applies to component weights, not to the density δ_n, which for fixed q is not bounded away from 0.Source: §12 · p. 36

Relation to decomposition theory

• For (2, 21), the resolvent components split a dimension-18 summand of Hachenberger's finest agreeable decomposition into two dimension-9 components, each with 294 valid coordinate vectors.Theorem 3.2 then gives CN₂(21) = 259308.Source: §12 · p. 37
• The two factorisations of CN_q(n) need not coincide: the paper gives examples where its components are finer and where Hachenberger's factorisation is finer.For (2, 27), one component of dimension 18 corresponds to Hachenberger's count with three factors; the authors have not compared the decompositions systematically.Source: §12 · pp. 37–38

Contribution

• The structure theorem gives a component-weight bound uniform in n, enabling the character-sum argument for regular and non-regular pairs alike.The paper identifies this structure theorem and the resulting bound W(q) as its main novelty.Source: §12 · p. 38

Further questions

• The paper asks whether sieving whole low-weight components could lower thresholds or settle pairs without individual checks, and whether closed formulas for component pass probabilities exist.Such formulas would extend Hachenberger's formula for regular pairs and make the main term θ CN_q(n) explicit.Source: §12 · p. 38

Small fields

• For small fields, Corollary 8.9(a)'s error bounds can be trivial; for (2, 8), PCN₂(8) = 56 while θ CN₂(8) ≈ 64.25.The analogous lower bound PCN_q(n) ≥ φ(q^n − 1)(1 − 1/q)^n′ therefore fails for (2, 8).Source: §12 · pp. 38–39

Refinements

• The remarks propose combining component structure with trace conditions and ask when both a primitive element and its inverse can be completely normal.The cited trace result concerns many extensions of prime-power degree.Source: §12 · p. 39

Authorship and review

• The author attributes the research questions, overall direction, and final decisions to themselves, while saying AI models generated the arguments and drafted the text under their direction.The author says they checked every step of the final proof by hand and takes responsibility for the results.Source: Use of AI tools · p. 39
• The author ran and confirmed the AI-written Python programs but did not review their code line by line; the AI-generated Lean formalisation was also not reviewed in full.The author reports building and running the Lean audit files and checking the formal statements of the main theorem and Corollaries 8.8 and 8.9.Source: Use of AI tools · p. 39

• The appendix documents the formalisation mentioned in Sections 1 and 9 and is not needed for reading the rest of the paper.Source: A The Lean formalisation · p. 40

• The proof for n > q and Corollaries 8.8 and 8.9, including every computer-assisted step, is formalised in Lean 4 with Mathlib.Source: What is formalised · p. 40
• HasMMProperty states that E contains a generator of E× that is normal over every intermediate field, with normality defined by its Galois conjugates forming a basis.Source: What is formalised · p. 40
• CNq(n) counts elements normal over every intermediate field, while PCNq(n) counts those elements that also generate E×.Source: What is formalised · p. 40

• The main theorem has no sorry and depends on four additional axioms beyond Mathlib’s three foundational axioms, including the cited n ≤ q result and Rosser–Schoenfeld bound.Source: Axioms and trusted base · p. 40
• The 25 large Boolean checkers run outside Lean’s kernel, requiring trust in Lean’s compiler, interpreter, and native library code, while their soundness theorems are kernel-checked.Source: Axioms and trusted base · p. 40
• Smaller computations, including those for κ3 and κ4 in Proposition 6.5, are checked directly by the kernel.Source: Axioms and trusted base · p. 40
• External data and outputs of unverified routines are checked rather than trusted; the audit also verifies that checker constants lack implemented_by or extern attributes.Source: Axioms and trusted base · p. 41
• The trusted base includes the kernel, named axioms, compiler and interpreter, native code used by the checkers, and the formal statement’s short definitions; Python programs and data are not trusted.Source: Axioms and trusted base · p. 41

• Lemma 4.1 is proved by identifying E× with Z/(q^n − 1) and applying the ℓ1 argument to the indicator of primitive elements, rather than using explicit Vinogradov formula coefficients.The resulting character coefficients have ℓ1-norm at most 2^ωθ; the trivial character has coefficient θ and the others yield Gauss sums of absolute value q^(n/2).Source: Differences from the proofs in the paper · p. 41
• The formalisation otherwise follows the paper’s constants, tables, ranges, and thresholds, with some elementary steps rearranged, including a geometric-series derivation for R̂ξ = 1/d′ C_d,k.Source: Differences from the proofs in the paper · p. 41
• For Corollary 8.8, the formal proof uses a sufficient bound on M1 and Bernoulli’s inequality for q ≥ 3, and obtains strictness at q = 2 from a component with two distinct conditions.Source: Differences from the proofs in the paper · p. 41
• Proposition 6.3 is formalised for rational ϑ and Θ, which suffices for its applications.Source: Differences from the proofs in the paper · p. 41

Computations and definitions handled differently

• For Proposition 6.5, the formalisation checks externally computed factorizations by verifying their product and testing each factor by trial division, rather than factoring with sympy.Source: Computations and definitions handled… · p. 41
• The formalisation sets ordK(q) = 0 when gcd(q, K) > 1 and defines D∞ at an index after which the sequence is constant.It does not assume K is p-free; condition (ii) forces p ∤ K unless K = 0.Source: Computations and definitions handled… · p. 42
• For Theorem 7.8, the formalisation uses multiples of O∞ and D∞ that can be certified by congruences, unlike the Python program’s direct computation of those values.The formalisation also verifies the defining properties of computed labellings; the Python program uses the components themselves.Source: Computations and definitions handled… · p. 42
• For Proposition 8.4, the formalisation checks the stated q = 3 pairs using exact rational arithmetic, while the Python program checks all n < 131200.For tk it uses a sieve when φ(k)⌊log2 q⌋≤3000 and otherwise applies a bound with proved rational replacements.Source: Computations and definitions handled… · p. 42
• For Proposition 8.5, the formalisation certifies matrix rank by checking an inverse computed by an unverified routine, and checks only γq^d = γ for normality.It constructs f as monic of degree m and computes the prime list outside Lean, checking it there.Source: Computations and definitions handled… · p. 42

Statements that are not formalised

• Illustrative values, examples, comparisons, remarks, and the Section 11 checks (C1)–(C4) are among the statements not formalised.The omitted items include exact values and maxima, worked examples, and the stated sharpness results.Source: Statements that are not formalised · pp. 42–43