Power-sum moments of the half-system T_k in F_p

For a prime p > 7, m = (p-1)/2 and k <= m with 8k(k+1)+1 = 0 in F_p, the half-system T_k = {1,...,k} u {-(k+1),...,-m} of F_p has odd power-sum moments M_3 = -1/128, M_5 = 7/1536, M_7 = -245/49152 (all in F_p). The proof reduces M_j(T_k) = 2F_j(k) - F_j(m) for odd j, proves the Faulhaber closed forms for j = 3, 5, 7 over the integers by induction, and substitutes k(k+1) = -1/8 and m(m+1) = -1/4. The existence and uniqueness of k (needs (2|p) = 1), the half-system and centring claims and the semigroup S_{T_k} = <3,5,7> are NOT formalized here; k is taken as a hypothesis.

Main results

• P3a.moments_Tk: M_3, M_5, M_7 of T_k equal -1/128, 7/1536, -245/49152 in F_p for p > 7
• P3a.moment_Tk_odd: M_j(T_k) = 2F_j(k) - F_j(m) for odd j

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:familia.

def P3a.Tk (p k : ℕ) : Finset (ZMod p)

The half-system T_k = {1,…,k} ∪ {-(k+1),…,-m} in 𝔽_p, m = (p-1)/2.

Equations

• P3a.Tk p k = Finset.image (fun (r : ℕ) => ↑r) (Finset.Icc 1 k) ∪ Finset.image (fun (r : ℕ) => -↑r) (Finset.Icc (k + 1) ((p - 1) / 2))

def P3a.moment {p : ℕ} (T : Finset (ZMod p)) (j : ℕ) : ZMod p

The j-th power-sum moment of a finite subset of 𝔽_p.

Equations

• P3a.moment T j = ∑ t ∈ T, t ^ j

def P3a.F (j t : ℕ) : ℤ

Partial power sum F_j(t) = ∑_{r=1}^t r^j in ℤ.

Equations

• P3a.F j t = ∑ r ∈ Finset.Icc 1 t, ↑r ^ j

theorem P3a.F_succ (j t : ℕ) : F j (t + 1) = F j t + (↑t + 1) ^ j

theorem P3a.F3 (t : ℕ) : 4 * F 3 t = (↑t * (↑t + 1)) ^ 2

theorem P3a.F5 (t : ℕ) : 12 * F 5 t = (↑t * (↑t + 1)) ^ 2 * (2 * (↑t * (↑t + 1)) - 1)

theorem P3a.F7 (t : ℕ) : 24 * F 7 t = (↑t * (↑t + 1)) ^ 2 * (3 * (↑t * (↑t + 1)) ^ 2 - 4 * (↑t * (↑t + 1)) + 2)

theorem P3a.tk_disjoint {p : ℕ} (hp : 2 < p) (k : ℕ) : Disjoint (Finset.image (fun (r : ℕ) => ↑r) (Finset.Icc 1 k)) (Finset.image (fun (r : ℕ) => -↑r) (Finset.Icc (k + 1) ((p - 1) / 2)))

theorem P3a.moment_Tk_odd {p : ℕ} (hp : 2 < p) (k : ℕ) (hk : k ≤ (p - 1) / 2) (j : ℕ) (hj : Odd j) : moment (Tk p k) j = 2 * ↑(F j k) - ↑(F j ((p - 1) / 2))

theorem P3a.uv {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (k : ℕ) (hk8 : 8 * ↑k * (↑k + 1) + 1 = 0) : 8 * (↑k * (↑k + 1)) = -1 ∧ 4 * (↑((p - 1) / 2) * (↑((p - 1) / 2) + 1)) = -1

k(k+1) = -1/8 and m(m+1) = -1/4 in 𝔽_p, from 8k(k+1)+1 = 0 and 2m+1 = p.

theorem P3a.moments_Tk {p : ℕ} [Fact (Nat.Prime p)] (hp : 7 < p) (k : ℕ) (hk : k ≤ (p - 1) / 2) (hk8 : 8 * ↑k * (↑k + 1) + 1 = 0) : moment (Tk p k) 3 = -1 / 128 ∧ moment (Tk p k) 5 = 7 / 1536 ∧ moment (Tk p k) 7 = -245 / 49152

Moments of T_k (paper prop:familia): M₃ = -1/128, M₅ = 7/1536, M₇ = -245/49152 in 𝔽_p, for a prime p > 7 and k ≤ m = (p-1)/2 with 8k(k+1)+1 = 0.