The split locus of superelliptic curves: determination for small fields, and members that are neither maximal nor Hermitian quotients

The F₁6 = F₂[X]/(X⁴+X+1) model of Witness.lean is a field: commutative ring axioms on all 16³ triples, and X has multiplicative order 15

Over F₁6 the pair n = 3, f = prod over the F₂-hyperplane 0,...,7 of (x - r) = x⁸+x⁴+x²+x satisfies (H1'), (H4) and delta = 0: f splits into 8 distinct linear factors, its value set is 0,1, and 1 is a cube; the smooth model of y³ = f(x) has 32 affine points, 33 in all, and genus 7

Both halves of prob-splitlocus are NO: the F₁6 curve of SS2 has 33 rational points against a maximality bound of 16+1+2*7*4 = 73, so it is not maximal, and genus 7 > 6 = the genus of the Hermitian curve over F₁6, so it is not a quotient of it

The source's own thm-hermitian at q₀ = 4, n = 5 reproduced from the same field tables: R is the set of fifth roots of unity, f = x⁵+1, delta = 0, d = 5, N = 55, 2g = 12, and the curve has 55+5+5 = 65 = 16+1+2*6*4 points – it is maximal

Negative controls for the F₁6 witness: delta = 0 fails for two nearby 8-element root sets, the point counter separates 65 from 33, and both hypotheses (H4) and d >= 3 are live

An infinite family of counterexamples: for every even m = 2e >= 4 and every n >= 3 dividing 2ᵐ - 1, the curve yⁿ = Tr_(F_(2ᵐ)/F₂)(x) lies in the split locus and satisfies pointCount < maxBound and twoGenus > twoHermGenus – proved uniformly in e and n, in the kernel, with no finite data for the two arithmetic inequalities (membership in the split locus rests on the trace identity checked at q = 16, 64, 256 – label aligned with ground 2026-08-28)

Negative controls for the uniform family: at e = 1 (over F₄) the point count EQUALS the maximality bound and the two genera agree, so the hypothesis 2 <= e is exactly what separates the Hermitian case; and n = 1 is degenerate

The split locus over F_q is completely determined for q = 4, 5, 7, 8, 9, 11, 13, 19: the counts of admissible root sets by degree, over all 2^q subsets, with each field model certified; totals 5, 22, 73, 51, 216, 278, 1032 and 7206 pairs (n,R)

The split locus over F₁6, by (n,d): 2101 admissible pairs (n,R) and 7395 pairs (n,f); the source's Hermitian family thm-hermitian is exactly the single cell (n,d) = (5,5) with 48 entries, and the cell (3,8) with 270 entries contains the counterexample of SS2/SS3

Negative controls for the census: only 270 of the 12870 eight-element subsets of F₁6 are admissible at n = 3 and the count at d = 13 is zero, so the sweep is selective; and the counts at d = q and d = q-1 are 1 and q for every field, the degenerate tail of the problem as literally posed

The family instantiated at F₆4 = F₂[X]/(X⁶+X+1) and F₂56 = F₂[X]/(X⁸+X⁴+X³+X²+1): the absolute trace has exactly q/2 roots and value 1 elsewhere, and each admissible n has exactly n n-th roots of unity, giving #X = q/2 + n q/2 + 1 as in Family.pointCount

Negative control on the field certificate: it rejects the reducible modulus X⁶+X²+1 = (X³+X+1)² (whose quotient ring has seven non-invertible nonzero elements) and the AES modulus X⁸+X⁴+X³+X+1, in which X has order 51 rather than 255

The split locus completely determined for q = 23, 25, 27, 29, 31, 32 as well: 26476, 124662, 107988, 388924, 752780 and 3939 admissible pairs (n,R), by (n,d)

The trace polynomial Tr = ∑_(i<m) X^(pⁱ) over any field with pᵐ elements: Trᵖ - Tr = X^(pᵐ) - X, Tr | X^q - X, Tr monic of degree pᵐ⁻¹, separable, with pᵐ⁻¹ distinct roots and equal to ∏ (X - a) over them; every value lies in the prime subfield; and eval Tr = algebraMap ∘ Algebra.trace

For every m >= 3, every field F with 2ᵐ elements and every n | 2ᵐ - 1, the pair (n, Tr_(F/F₂)) satisfies (H1'), (H4) and δ = 0 — it lies in the split locus of prob-splitlocus, with d = 2ᵐ⁻¹; proved uniformly, with no field model and no finite data, and covering odd m which SS6 cannot reach

Negative controls for the uniform statement: at m = 2 the degree is 2 < 3 so the pair is NOT in the split locus (m >= 3 is the exact boundary); the roots are a proper subset (2ᵐ⁻¹ < 2ᵐ); the value 1 is attained so the value set is 0,1 and not 0; the trace identity fails in the wrong characteristic (F₃, p = 2, at x = 1); and the uniform theorem reproduces the 8, 32, 128 of the three checked models

n-th powers in a finite field: a nonzero x with x^((q-1)/n) = 1 is an n-th power, for every n | q - 1

The split locus in odd characteristic: for every prime p, every m with pᵐ⁻¹ >= 3 and every n | (pᵐ - 1)/(p - 1), (n, Tr_(F/Fₚ)) lies in the split locus; and for q = p²ᵉ with e >= 2 the curve yⁿ = Tr(x) is not maximal for every n >= 2, with genus above the Hermitian genus whenever n >= p + 1. Smallest member q = 81, d = 27, n = 4: 244 points against a bound of 784, 2g = 78 > 72

Negative controls in odd characteristic: at e = 1 the point count EQUALS the maximality bound (checked at (p,n) = (3,4) and (5,6)), so e >= 2 is the exact boundary; at p = 3, e = 2, n = 2 the curve is non-maximal but has genus BELOW the Hermitian genus, so n >= p+1 is not decoration; and n | (q-1)/(p-1) is strictly stronger than (H4) in odd characteristic (8 | 8 but 8 ∤ 4 over F₉) while the two coincide in characteristic two

The maximality dichotomy of the linearized family: over F_(p²ᵉ), for every j | 2e with 0 < j < 2e and every n >= 2, the curve yⁿ = Tr_(F_q/F_(pʲ))(x) attains the Hasse-Weil bound iff j = e — equality at j = e for every p, e, n, strict inequality for every 1 <= j < e, and (H1') forces j <= e because the largest proper divisor of 2e is e

Controls for the dichotomy: over F₈1 with n = 5 (admissible in both columns, 5 | 40 and 5 | 10, checked in the statement) the three j behave as the dichotomy says (j=1: 298 < 1018; j=2=e: 370 = 370; j=4=2e: d = 1 < 3, fails (H1')); the hypothesis j | 2e is live (j = 3 > e = 2 is not a divisor of 4); the j = 1 column IS TraceOdd's family by rfl; and over F₁6 the two columns reproduce 33 < 73 (the Witness.lean counterexample) and 65 = 65 with 2g = 12 (the invariants of the source's thm-hermitian member at q₀ = 4, n = 5)

The general j: Tr_(F_q/F_(pʲ)) splits into (pʲ)ʳ⁻¹ distinct linear factors over any field with (pʲ)ʳ elements, its values satisfy x^(pʲ) = x, and for every n >= 1 dividing (q-1)/(pʲ-1) with d = (pʲ)ʳ⁻¹ >= 3 the pair (n, Tr_(F/F_(pʲ))) lies in the split locus; with j r = 2e, (pʲ)ʳ⁻¹ = relDeg p e j

MEASUREMENT — formalization cost of the uniform finite-field half plus the dichotomy: 1,079 Lean lines (422 + 287 + 370) and 67 declarations, warm 13.5 / 19.8 / 21.6 s at 6.97-7.02 GB against an import Mathlib baseline of 10.22 s / 6.58 GB (marginal 3.3-11.4 s and 0.39-0.44 GB), 17 lake env lean invocations on the three modules of which 4 failed — all four in the first pass over the polynomial API; the arithmetic and the lift to general j needed none — 28 min of Lean wall in a 3.8 h dispatch; seven named Mathlib gaps had to be filled, four names were renamed/deprecated

The NORM tower lies in the split locus: for every prime p, every j >= 1 and r >= 2, every field F with (pʲ)ʳ elements, every b in F_(pʲ)^* and every n >= 1 dividing k = (q-1)/(pʲ-1) with k >= 3, the pair (n, xᵏ - b) satisfies (H1'), (H4) and delta = 0, with d = k – proved uniformly, no field model and no finite data. The source's thm-hermitian is the single level r = 2, b = -1

The split locus is invariant under x -> x - t: if (n,f) satisfies (H1'), (H4) and delta = 0 then so does (n, f(x-t)); hence every member of either tower comes in q translates, which is what makes the census counts 48 = 3*16 and 20 = 5*4 over F₁6, 18 = 2*9 and 12 = 4*3 over F₉ come out

The maximality dichotomy of the NORM tower: over F_(p²ᵉ), for every j | 2e with 0 < j < 2e and every n >= 2 dividing d = (q-1)/(pʲ-1), the curve yⁿ = xᵈ - b attains the Hasse-Weil bound iff j = e – equality at j = e for every p, e, n, strict inequality for every 1 <= j < e; and at j = e the additive and multiplicative members have DIFFERENT degrees (sqrt q and sqrt q + 1) but the SAME genus and the SAME point count, both maximal

Controls for the norm tower: over F₁6 the j = e = 2 member reproduces the thm-hermitian invariants d = 5, 2g = 12, 65 = 65 of SS4 and the j = 1 member is the degenerate d = q-1 column; over F₈1 with n = 5 (admissible in both levels) j = 1 gives 250 < 1450 and j = 2 = e gives 370 = 370 = relPointCount; and n | (q-1)/(pʲ-1) is strictly stronger than (H4) (7 | 63 but 7 does not divide 9, over F₆4 at j = 3)

The two smallest cells of the split locus are EXACTLY the two towers at j = e: over F₉ and F₁6, for every admissible n, the admissible root sets of size sqrt q are exactly the sqrt q (sqrt q + 1) F_(sqrt q)-lines and those of size sqrt q + 1 are exactly the (sqrt q - 1) q norm sets a: (a-t)^(sqrt q + 1) = b, both nonempty iff n | sqrt q + 1, and nothing smaller occurs – set equality checked over all 2^q subsets. This is the equality case of the source's own pigeonhole bound, and on it the answer to both halves of prob-splitlocus is YES

Negative controls for the cell classification: over F₁6 the exponents n = 3, 15 (which do not divide q₀+1 = 5) admit NO root set of size 4 or 5, and none of size 3 for any n although (H1') allows d = 3; over F₉ the exponent n = 8 admits none of size 3 or 4; no line is a norm set; sameSetB rejects a list with an element dropped and a list with a repeat; and the independent sweep of Cells.lean reproduces countByD 16 5 at d = 4, 5

Inversion duality on the split locus: if (n,f) satisfies (H1'), (H4) and delta = 0, f(0) = 0, n | deg f + 1, and the monic normalisation (f.coeff 1)⁻1 is an n-th power, then (n, f*) satisfies them too, where f* is the monic polynomial whose root multiset is the image of f's under x -> x⁻1; the mechanism is the identity f*(a) = (f.coeff 1)⁻1 * a^(deg f + 1) * f(1/a) for every a!= 0. The map is an involution, so this is a bijection of the split locus onto itself, not merely a map into it. Proved uniformly over every finite field, with no field model and no finite data

The inverted trace family: invPoly(Tr_(F/Fₚ)) = sum_(i<m) X^(pᵐ⁻¹+1-pⁱ), an explicit sparse polynomial whose root set is 0 u v⁻1: v in ker Tr_(F/Fₚ), v!= 0. For every prime p, every m with pᵐ⁻¹ >= 3, every field with pᵐ elements and every n >= 1 dividing BOTH (pᵐ-1)/(p-1) and pᵐ⁻¹+1, the pair lies in the split locus with d = pᵐ⁻¹; for even m = 2e >= 4 that covers every n | p+1, and at n = p+1 the curve is not maximal and has genus strictly above the Hermitian genus, so these pairs refute both halves of prob-splitlocus. At p = 2, m = 4, n = 3 this is X⁸+X⁷+X⁵+X over F₁6 – the family's FIRST member whose branch locus is not a coset of an Fₚ-subspace

Controls for the inversion duality: f -> f* is an involution; at m = 2 – the Hermitian level j = e of SS28 – inversion FIXES the trace polynomial (Tr* = Xᵖ + X = Tr), which is why SS28's minimal-cell classification is not contradicted, while for m >= 3 it does not (Tr* and Tr differ at the coefficient of Xᵖ); Tr* has a nonzero coefficient at an exponent that is not a power of p; the hypothesis n | d+1 is live (gcd(2³+1, 2⁴-1) = 3, so over F₁6 only n = 3 of the exponents allowed by (H4) survives, and gcd(3³+1, (3⁴-1)/2) = 4 over F₈1); and the F₁6 member reproduces the invariants d = 8, #X = 33, bound 73, 2g = 14 > 12 of SS2/SS6

The split locus is organised by PGL(2,q), and that closes the cells left open on 2026-08-30. With B = R when n | d and B = R u infinity when gcd(n,d) = 1 (so n | |B| in both cases), delta = 0 is a PGL(2,q)-invariant property of the branch divisor B of yⁿ = f(x), and the cells d = |B| and d = |B|-1 are the two halves of one orbit. Over F₁6 the PGL(2,16)-orbit of 0..7 u infinity has 510 members, whose 270 members containing infinity are EXACTLY the cell (n,d) = (3,8) and whose 240 others are EXACTLY the cell (3,9) – both complete over all 2¹6 subsets, and the 270 split as 30 affine hyperplanes plus the 240 affine images of the root set of X⁸+X⁷+X⁵+X (SS31). Over F₉ at n = 2 and n = 4 the two minimal cells are one orbit of 30 = 12 + 18, and over F₁6 at n = 5 the two minimal cells of SS28 are one orbit of 68 = 20 + 48 – which is why the trace and norm towers at j = e have the same genus and the same point count at different degrees (the kumᵣelₛameᵢnvariants coincidence of SS26). Over F₂7 (tool, not kernel) the cell (13,13) of 405 root sets is EXACTLY the PGL(2,27)-orbit of the norm set, all 756 of whose members are admissible – the 13 unexplained translation orbits of the 2026-08-30 journal are one PGL orbit, and there is no third structure

Controls for the PGL(2,q) organisation: the hypothesis n | |B| is not decoration – at n = 15 and at n = 5 the same 510-member orbit over F₁6 is NOT inside the split locus (neither half matches its cell), and the cells (15,8) and (5,8) have only the 30 hyperplanes; at n = 5 the orbit half and the cell (5,9) both have 240 members and are different families, so counts alone would not have decided it; the root set of X⁸+X⁷+X⁵+X is not closed under addition while the hyperplane 0,...,7 is; |PGL(2,16)| = 4080 and |PGL(2,9)| = 720 with each element listed once; and sameSetB still rejects a list with an element dropped