Prime powers and the doubling lemma for the orders of Sp(2m)

Two arithmetic pieces on the orders generated by character values of Sp(2m).

• Prime powers: when p ∣ T_m, with T_m = ∑_{j=1}^m j², for p ≥ 5, p = 3 and p = 2; when the auxiliary quantity H vanishes modulo p; the link p ∣ [O : A] ⇔ p ∣ T_m as a conditional statement whose hypothesis is the ring-theoretic step (not formalized here); the cases q = p, q = 27, q = 25.
• Half period and doubling: parts (i) and (ii), entry by entry in ZMod n and as equalities of column lattices in U → ℤ, and the identity 2 ŝ_n(c) = s_n(2c) − s_n(c).

Main results

• AritmeticaConductor.potencias_ge5, AritmeticaConductor.potencias_three, AritmeticaConductor.potencias_two, AritmeticaConductor.potencias_a_cond, AritmeticaConductor.potencias_q_primo, AritmeticaConductor.potencias_q27, AritmeticaConductor.potencias_q25: the prime-power statements.
• AritmeticaConductor.dobla_i, AritmeticaConductor.dobla_ii, AritmeticaConductor.dobla_ii_hat, AritmeticaConductor.two_sh: half period and doubling.

References

• C. Marín, Conductors of orders generated by character values of Sp(2m), preprint (2026); programs and outputs: Zenodo, doi:10.5281/zenodo.23090540.
• C. Marín, Where the character values of Sp(2m) at a torsion element fail to generate the ring of integers, Zenodo (2026), doi:10.5281/zenodo.22813216 (a longer preprint of the same work).

Part 1. prop:potencias: arithmetic of p ∣ T_m

def AritmeticaConductor.T (m : ℕ) : ℕ

T_m = ∑_{j=1}^m j².

Equations

• AritmeticaConductor.T m = ∑ j ∈ Finset.Icc 1 m, j ^ 2

theorem AritmeticaConductor.six_mul_T (m : ℕ) : 6 * T m = m * (m + 1) * (2 * m + 1)

6 T_m = m (m+1) (2m+1).

def AritmeticaConductor.P (m : ℕ) : ℕ

P m = m (m+1) (2m+1).

Equations

• AritmeticaConductor.P m = m * (m + 1) * (2 * m + 1)

theorem AritmeticaConductor.dvd_P_iff_mod (k m : ℕ) : k ∣ P m ↔ k ∣ P (m % k)

k ∣ P m only depends on m mod k.

theorem AritmeticaConductor.dvd_small {n x : ℕ} (hn : 0 < n) (hx : x < 3 * n) : n ∣ x ↔ x = 0 ∨ x = n ∨ x = 2 * n

theorem AritmeticaConductor.potencias_ge5 {p : ℕ} (hp : Nat.Prime p) (h5 : 5 ≤ p) (m : ℕ) : p ∣ T m ↔ m % p = 0 ∨ m % p = p - 1 ∨ m % p = (p - 1) / 2

prop:potencias (a), explicit form, p ≥ 5: p ∣ T_m ⇔ m ≡ 0, −1, (p−1)/2 (mod p).

theorem AritmeticaConductor.potencias_three (m : ℕ) : 3 ∣ T m ↔ m % 9 = 0 ∨ m % 9 = 4 ∨ m % 9 = 8

prop:potencias (a), explicit form, p = 3: 3 ∣ T_m ⇔ m ≡ 0, 4, 8 (mod 9).

theorem AritmeticaConductor.potencias_two (m : ℕ) : 2 ∣ T m ↔ m % 4 = 0 ∨ m % 4 = 3

prop:potencias (a), explicit form, p = 2: 2 ∣ T_m ⇔ m ≡ 0, 3 (mod 4).

The step "it remains to say when H ≡ 0 (mod p)"

theorem AritmeticaConductor.dvd_all_h_iff {p m : ℕ} (hm : 1 ≤ m) : (∀ k ∈ Finset.Icc 1 m, p ∣ T m * (m - 1).choose (k - 1) * 2 ^ (k - 1)) ↔ p ∣ T m

The linear coefficients h_k = T_m · C(m−1,k−1) · 2^{k−1} (1 ≤ k ≤ m) are all divisible by p iff p ∣ T_m (m ≥ 1; the case k = 1 gives h_1 = T_m).

theorem AritmeticaConductor.H_a_eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : -Polynomial.C ↑(T m) * (Polynomial.X - Polynomial.C 2) ^ (m - 1) = 0 ↔ p ∣ T m

prop:potencias (a), q = p^v: H = −T_m (X−2)^{m−1} vanishes in 𝔽_p[X] iff p ∣ T_m.

theorem AritmeticaConductor.H_b_eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a b U V : ℕ) : (Polynomial.X - Polynomial.C 2) ^ (a - 1) * (Polynomial.X + Polynomial.C 2) ^ (b - 1) * (Polynomial.C ↑V * (Polynomial.X - Polynomial.C 2) - Polynomial.C ↑U * (Polynomial.X + Polynomial.C 2)) = 0 ↔ p ∣ U ∧ p ∣ V

prop:potencias (b), q = 2p^v, m ≥ 2: H = (X−2)^{a−1} (X+2)^{b−1} (V_m(X−2) − U_m(X+2)) vanishes in 𝔽_p[X] (p odd) iff p ∣ U_m and p ∣ V_m.

theorem AritmeticaConductor.potencias_a_cond {p m idx : ℕ} (hm : 1 ≤ m) (h : ℕ → ℤ) (hIdx : p ∣ idx ↔ ∀ k ∈ Finset.Icc 1 m, ↑p ∣ h k) (hh : ∀ k ∈ Finset.Icc 1 m, (h k).natAbs = T m * (m - 1).choose (k - 1) * 2 ^ (k - 1)) : p ∣ idx ↔ p ∣ T m

prop:potencias (a), conditional link. The ring-theoretic part of the paper's proof (p ∣ [O : A] iff p divides every linear coefficient h_k, up to sign, of e_k(η_1,…,η_m) in the uniformiser t) is taken as the hypothesis hIdx; the value |h_k| = T_m C(m−1,k−1) 2^{k−1} (proved as Conductor.LinearCoeff.coeff_one_esymm_sq) as the hypothesis hh. Then p ∣ [O : A] ⇔ p ∣ T_m.

theorem AritmeticaConductor.potencias_q_primo {p m : ℕ} (hp : Nat.Prime p) (h5 : 5 ≤ p) (hm1 : 1 ≤ m) (hm : m < (p - 1) / 2) : ¬p ∣ T m

Remark after prop:potencias: for q = p prime (p ≥ 5), A ≠ ℤ forces 1 ≤ m < (p−1)/2, and then p ∤ T_m.

theorem AritmeticaConductor.potencias_q27 : {m ∈ Finset.Icc 1 13 | 27 ≠ 2 * m + 1 ∧ 27 ≠ 2 * m + 2 ∧ 3 ∣ T m} = {4, 8, 9}

Remark after prop:potencias, q = 27: for 1 ≤ m < 27/2 with A ≠ ℤ (27 ∉ {2m+1, 2m+2}, Proposition prop:AZ), 3 ∣ T_m exactly for m = 4, 8, 9.

theorem AritmeticaConductor.potencias_q25 : {m ∈ Finset.Icc 1 12 | 25 ≠ 2 * m + 1 ∧ 25 ≠ 2 * m + 2 ∧ 5 ∣ T m} = {2, 4, 5, 7, 9, 10}

Remark after prop:potencias, q = 25: 5 ∣ T_m exactly for m = 2, 4, 5, 7, 9, 10.

Part 2. lem:dobla: half period, and doubling

def AritmeticaConductor.s (n : ℕ) (c : ZMod n) : ℤ

The sawtooth s_n(0) = 0, s_n(c) = 2c − n for 1 ≤ c < n.

Equations

• AritmeticaConductor.s n c = if c.val = 0 then 0 else 2 * ↑c.val - ↑n

def AritmeticaConductor.sh (n : ℕ) (c : ZMod n) : ℤ

The signed residue ŝ_n(c) = ĉ ∈ (−n/2, n/2), with ŝ_n(n/2) = 0 for even n.

Equations

• AritmeticaConductor.sh n c = if 2 * c.val < n then ↑c.val else if 2 * c.val = n then 0 else ↑c.val - ↑n

theorem AritmeticaConductor.mod_cases {x n : ℕ} (h : x < 2 * n) : x < n ∧ x % n = x ∨ n ≤ x ∧ x % n = x - n

theorem AritmeticaConductor.sh_eq_half (n : ℕ) [NeZero n] (hn : Even n) (c : ZMod n) : 2 * sh n c = s n (c + ↑(n / 2))

lem:dobla (i), pointwise: ŝ_n(c) = ½ s_n(c + n/2) for even n.

theorem AritmeticaConductor.two_sh (n : ℕ) [NeZero n] (c : ZMod n) : 2 * sh n c = s n (2 * c) - s n c

"One identity, two regimes" (after lem:dobla): 2 ŝ_n(c) = s_n(2c) − s_n(c) for every n.

theorem AritmeticaConductor.mul_half_of_odd {n : ℕ} [NeZero n] (hn : Even n) (a : ZMod n) (ha : Odd a.val) : a * ↑(n / 2) = ↑(n / 2)

A residue with odd representative fixes the half period: a · (n/2) = n/2 in ZMod n.

theorem AritmeticaConductor.odd_val_of_unit {n : ℕ} (hn : Even n) (a : (ZMod n)ˣ) : Odd (↑a).val

A unit modulo an even n is odd.

def AritmeticaConductor.col {U : Type u_1} (n : ℕ) (f : ZMod n → ℤ) (w : U → ZMod n) (c : ZMod n) : U → ℤ

The column c of the matrix [f(w_u · c)]_u (rows indexed by u : U, multiplier w_u).

Equations

• AritmeticaConductor.col n f w c u = f (w u * c)

def AritmeticaConductor.L {U : Type u_1} (n : ℕ) (f : ZMod n → ℤ) (w : U → ZMod n) : Submodule ℤ (U → ℤ)

The column lattice: the ℤ-span of the columns c ∈ ZMod n.

Equations

• AritmeticaConductor.L n f w = Submodule.span ℤ (Set.range (AritmeticaConductor.col n f w))

theorem AritmeticaConductor.L_sin_cero {U : Type u_1} (n : ℕ) [NeZero n] (w : U → ZMod n) : Submodule.span ℤ (col n (s n) w '' {c : ZMod n | c ≠ 0}) = L n (s n) w

The paper indexes the columns of M_n by 1 ≤ c < n; adjoining the zero column c = 0 does not change the lattice.

theorem AritmeticaConductor.dobla_i_col {U : Type u_1} (n : ℕ) [NeZero n] (hn : Even n) (w : U → ZMod n) (hw : ∀ (u : U), Odd (w u).val) (c : ZMod n) : 2 • col n (sh n) w c = col n (s n) w (c + ↑(n / 2))

lem:dobla (i), column by column: the column c of M̂_n is half the column c + n/2 of M_n, for any multipliers w_u with odd representatives.

theorem AritmeticaConductor.dobla_i_core {U : Type u_1} (n : ℕ) [NeZero n] (hn : Even n) (w : U → ZMod n) (hw : ∀ (u : U), Odd (w u).val) : L n (s n) w = 2 • L n (sh n) w

lem:dobla (i), lattices, general multipliers with odd representatives: L_n = 2 L'_n.

theorem AritmeticaConductor.dobla_i {U : Type u_1} (n : ℕ) [NeZero n] (hn : Even n) (ι : U → (ZMod n)ˣ) : (L n (s n) fun (u : U) => ↑(ι u)⁻¹) = 2 • L n (sh n) fun (u : U) => ↑(ι u)⁻¹

lem:dobla (i) as stated: rows indexed by representatives ι u of (ℤ/n)ˣ/±1 (any family of units), M_n = [s_n(u⁻¹c)], M̂_n = [ŝ_n(u⁻¹c)]; then L_n = 2 L'_n, i.e. L'_n = ½ L_n.

lem:dobla (ii): n = 2r, r odd

@[reducible, inline]

abbrev AritmeticaConductor.red (r : ℕ) : ZMod (2 * r) →+* ZMod r

Reduction ZMod (2r) → ZMod r.

Equations

• AritmeticaConductor.red r = ZMod.castHom ⋯ (ZMod r)

def AritmeticaConductor.emb (r : ℕ) (c : ZMod r) : ZMod (2 * r)

The even lift c ↦ 2c of ZMod r into ZMod (2r).

Equations

• AritmeticaConductor.emb r c = ↑(2 * c.val)

theorem AritmeticaConductor.red_eq {r : ℕ} [NeZero r] (e : ZMod (2 * r)) : (red r) e = ↑e.val

theorem AritmeticaConductor.emb_val {r : ℕ} [NeZero r] (c : ZMod r) : (emb r c).val = 2 * c.val

theorem AritmeticaConductor.s_emb {r : ℕ} [NeZero r] (c : ZMod r) : s (2 * r) (emb r c) = 2 * s r c

s_{2r}(2c) = 2 s_r(c).

theorem AritmeticaConductor.mul_emb {r : ℕ} [NeZero r] (x : ZMod (2 * r)) (c : ZMod r) : x * emb r c = emb r ((red r) x * c)

x · (2c) = 2 (x c): multiplication commutes with the even lift.

theorem AritmeticaConductor.half_eq {r : ℕ} (hr : Odd r) {c e : ZMod r} (h : 2 * e = c) : 2⁻¹ * c = e

c* = 2⁻¹ c is characterised by 2 c* = c (r odd).

theorem AritmeticaConductor.s_odd {r : ℕ} [NeZero r] (hr : Odd r) (e : ZMod (2 * r)) (he : Odd e.val) : s (2 * r) e = 2 * (s r ((red r) e) - s r (2⁻¹ * (red r) e))

s_{2r}(ν(c)) = 2 (s_r(c) − s_r(c*)): for e ∈ ZMod (2r) with odd representative, c = e mod r and c* = 2⁻¹ c.

theorem AritmeticaConductor.odd_mul_val {r : ℕ} (x d : ZMod (2 * r)) (hx : Odd x.val) (hd : Odd d.val) : Odd (x * d).val

theorem AritmeticaConductor.even_eq_emb {r : ℕ} [NeZero r] (d : ZMod (2 * r)) (hd : Even d.val) : d = emb r ↑(d.val / 2)

theorem AritmeticaConductor.dobla_ii_col_even {U : Type u_1} {r : ℕ} [NeZero r] (w : U → ZMod (2 * r)) (c : ZMod r) : col (2 * r) (s (2 * r)) w (emb r c) = 2 • col r (s r) (fun (u : U) => (red r) (w u)) c

lem:dobla (ii), even columns: column 2c of M_{2r} is twice column c of M_r.

theorem AritmeticaConductor.dobla_ii_col_odd {U : Type u_1} {r : ℕ} [NeZero r] (hr : Odd r) (w : U → ZMod (2 * r)) (hw : ∀ (u : U), Odd (w u).val) (d : ZMod (2 * r)) (hd : Odd d.val) : col (2 * r) (s (2 * r)) w d = 2 • (col r (s r) (fun (u : U) => (red r) (w u)) ((red r) d) - col r (s r) (fun (u : U) => (red r) (w u)) (2⁻¹ * (red r) d))

lem:dobla (ii), odd columns: column ν(c) of M_{2r} is twice the difference of the columns c and c* = 2⁻¹c of M_r (rows with odd multipliers w_u).

theorem AritmeticaConductor.dobla_ii_core {U : Type u_1} {r : ℕ} [NeZero r] (hr : Odd r) (w : U → ZMod (2 * r)) (hw : ∀ (u : U), Odd (w u).val) : L (2 * r) (s (2 * r)) w = 2 • L r (s r) fun (u : U) => (red r) (w u)

lem:dobla (ii), lattices, general odd multipliers: L_{2r} = 2 L_r.

theorem AritmeticaConductor.inv_odd_red {r : ℕ} [NeZero r] (u : ℕ) (hu : Odd u) (hcop : u.Coprime r) : Odd (↑u)⁻¹.val ∧ (red r) (↑u)⁻¹ = (↑u)⁻¹

The odd representative u (coprime to r) has an odd inverse modulo 2r, which reduces to the inverse modulo r.

theorem AritmeticaConductor.dobla_ii {U : Type u_1} {r : ℕ} [NeZero r] (hr : Odd r) (ι : U → ℕ) (hodd : ∀ (u : U), Odd (ι u)) (hcop : ∀ (u : U), (ι u).Coprime r) : (L (2 * r) (s (2 * r)) fun (u : U) => (↑(ι u))⁻¹) = 2 • L r (s r) fun (u : U) => (↑(ι u))⁻¹

lem:dobla (ii) as stated: rows indexed by the same odd representatives ι u (coprime to r) of (ℤ/r)ˣ/±1 = (ℤ/2r)ˣ/±1, M_r = [s_r(u⁻¹c)], M_{2r} = [s_{2r}(u⁻¹c)]: L_{2r} = 2 L_r.

theorem AritmeticaConductor.dobla_ii_hat {U : Type u_1} {r : ℕ} [NeZero r] (hr : Odd r) (ι : U → ℕ) (hodd : ∀ (u : U), Odd (ι u)) (hcop : ∀ (u : U), (ι u).Coprime r) : (L (2 * r) (sh (2 * r)) fun (u : U) => (↑(ι u))⁻¹) = L r (s r) fun (u : U) => (↑(ι u))⁻¹

lem:dobla (ii), "hence L'_{2r} = L_r": the half-period lattice at 2r equals the lattice of M_r.

Sanity checks of the definitions (n = 6, n = 7)