The defect delta = 2 does not occur at n = 4, h = 1

For a centred spectrum of four elements of a field K (char not 2, 3) with e_3 != 0 (the consequence of trivial stabiliser h = 1), Newton's identities give M_2 = 0 => M_5 = 0 and M_3 = 3 e_3. With the generating rule S = <e, {0<j<e | M_j != 0}> (P3b.genSet), e >= 4 and e + 1 prime (so e != 5), M_2 = 0 makes 1, 2, 5 gaps (genus >= 3), and M_2 != 0 gives genus < 2 via two_le_genus_iff; hence genus != 2. Implicit hypotheses made explicit: h = 1 => e_3 != 0 is taken as hypothesis he3 (stabiliser not formalised); finiteness of the gap set; e + 1 prime is needed to exclude e = 5, where <3,4,5> would have genus 2. Not formalised: the derivation of the generating rule (Part I) and of e_3 != 0 from h = 1.

Main results

• P3b.pow4_five_eq_zero: Centred, M_2 = 0 implies M_5 = 0 for four elements (char != 2).
• P3b.pow4_three_eq: Centred: M_3 = 3 e_3.
• P3b.genus_ne_two_of_four: At n = 4, h = 1 the genus of S_T is never 2.

References

• C. Marín, The order generated by a column of the SU(n)ₖ S-matrix is locally a numerical semigroup ring (Part II), Zenodo (2026), doi:10.5281/zenodo.22864267, prop:n4.

def P3b.pow4 {K : Type u_1} [Field K] (t : Fin 4 → K) (k : ℕ) : K

Power sum M_k of a 4-element spectrum.

Equations

• P3b.pow4 t k = ∑ i : Fin 4, t i ^ k

def P3b.esymm3 {K : Type u_1} [Field K] (t : Fin 4 → K) : K

The third elementary symmetric function of four elements.

Equations

• P3b.esymm3 t = t 0 * t 1 * t 2 + t 0 * t 1 * t 3 + t 0 * t 2 * t 3 + t 1 * t 2 * t 3

theorem P3b.pow4_five_eq_zero {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (t : Fin 4 → K) (h1 : pow4 t 1 = 0) (hM2 : pow4 t 2 = 0) : pow4 t 5 = 0

Newton cascade: centred, M₂ = 0 ⇒ M₅ = 0 (char ≠ 2).

theorem P3b.pow4_three_eq {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (t : Fin 4 → K) (h1 : pow4 t 1 = 0) : pow4 t 3 = 3 * esymm3 t

Centred: M₃ = 3 e₃.

theorem P3b.genus_ne_two_of_four {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (t : Fin 4 → K) {e : ℕ} (he : 4 ≤ e) (hp : Nat.Prime (e + 1)) (h1 : pow4 t 1 = 0) (he3 : esymm3 t ≠ 0) (hfin : (P3a.gaps (genSet e fun (j : ℕ) => pow4 t j = 0)).Finite) : P3a.genus (genSet e fun (j : ℕ) => pow4 t j = 0) ≠ 2

Proposition prop:n4: at n = 4, h = 1 the defect δ = 2 does not occur.