The support of the conductor and the index: the arithmetic

With S(c) = ∑_{1≤j≤m, j≡c} j − ∑_{1≤j≤m, j≡−c} j (modulus n), this file proves the closed form of S and the arithmetic of the statements on the support of the conductor and on the index [O : A]. The ring-theoretic inputs (part (b) of the support theorem and the segment lemma Segmentos.lem_seg) enter as explicit hypotheses.

Main results

• SopIndice.S_formula: the four-case closed form of S(c) for m = k n + r, 0 ≤ r < n, 1 ≤ c ≤ n − 1.
• SopIndice.sop_c_ii: if n ∤ h, h + 1, h + 2 (h = 2m), then for every prime p some c with 2c ≢ 0 (mod n) has p ∤ S(c).
• SopIndice.sop_c: part (c) of the support theorem, from the hypotheses above.
• SopIndice.indice_val, SopIndice.indice_hminus, SopIndice.indice_dos, SopIndice.indice_small, SopIndice.indice_six, SopIndice.indice_prod: the valuations, the sufficient conditions for W₁ > d/2, the residues q' ∈ {1, 2, 3, 4, 6} and the product formula for [O : A].

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).

The moment S(c) and its closed form

def SopIndice.S (n m : ℕ) (c : ZMod n) : ℤ

S(c) = ∑_{1≤j≤m, j≡c (n)} j − ∑_{1≤j≤m, j≡−c (n)} j.

Equations

• SopIndice.S n m c = ∑ j ∈ Finset.Icc 1 m, ((if ↑j = c then ↑j else 0) - if ↑j = -c then ↑j else 0)

def SopIndice.Sform (n k r c : ℕ) : ℤ

The four cases of the proof of thm:sop(c), for m = kn + r and 1 ≤ c ≤ n − 1 (r < q' − c is written r + c < n).

Equations

• One or more equations did not get rendered due to their size.

def SopIndice.D (n m : ℕ) : Prop

D n m: n divides h = 2m, h + 1 or h + 2.

Equations

• SopIndice.D n m = (n ∣ 2 * m ∨ n ∣ 2 * m + 1 ∨ n ∣ 2 * m + 2)

theorem SopIndice.eq_of_dvd_lt {n x : ℕ} (h : n ∣ x) (h0 : 0 < x) (h2 : x < 2 * n) : x = n

theorem SopIndice.S_succ (n m : ℕ) (c : ZMod n) : S n (m + 1) c = S n m c + ((if ↑(m + 1) = c then ↑(m + 1) else 0) - if ↑(m + 1) = -c then ↑(m + 1) else 0)

theorem SopIndice.cast_eq_c {n k s c : ℕ} (hs : s < n) (hc : c < n) : ↑(k * n + s) = ↑c ↔ s = c

Membership of kn + s in the classes c and −c, for 0 < s < n, 0 < c < n.

theorem SopIndice.cast_eq_negc {n k s c : ℕ} (hs0 : 0 < s) (hs : s < n) (hc0 : 0 < c) (hc : c < n) : ↑(k * n + s) = -↑c ↔ s + c = n

theorem SopIndice.S_block (n k c : ℕ) (hc0 : 0 < c) (hcn : c < n) (h0 : S n (k * n) ↑c = Sform n k 0 c) (r : ℕ) : r < n → S n (k * n + r) ↑c = Sform n k r c

theorem SopIndice.S_zero_eq (n c : ℕ) (hc0 : 0 < c) (hcn : c < n) : S n 0 ↑c = Sform n 0 0 c

theorem SopIndice.S_formula (n k r c : ℕ) (hc0 : 0 < c) (hcn : c < n) (hr : r < n) : S n (k * n + r) ↑c = Sform n k r c

The count in the proof of thm:sop(c). For m = kn + r, 0 ≤ r < n, 1 ≤ c ≤ n−1: S(c) = (2k+1)c if c ≤ r < n−c; −(2k+1)(n−c) if n−c ≤ r < c; (k+1)(2c−n) if n−c ≤ r and c ≤ r; k(2c−n) if r < c and r < n−c.

thm:sop(c)

theorem SopIndice.r_of_not_D {n k r : ℕ} (hr : r < n) (hD : ¬D n (k * n + r)) : r ≠ 0 ∧ r + 1 ≠ n ∧ 2 * r + 1 ≠ n ∧ 2 * r + 2 ≠ n ∧ 2 * r ≠ n

If n ∤ h, h+1, h+2, the residue r = m mod n avoids the list of lem:seg.

theorem SopIndice.two_c_ne {n c : ℕ} (hc0 : 0 < c) (hcn : c < n) (h2 : 2 * c ≠ n) : 2 * ↑c ≠ 0

theorem SopIndice.not_dvd_both {p : ℕ} (hp : Nat.Prime p) {a b : ℤ} (hab : ∃ (x : ℤ) (y : ℤ), x * a + y * b = 1) : ¬(↑p ∣ a ∧ ↑p ∣ b)

theorem SopIndice.sop_c_ii {n m p : ℕ} (hn : 3 ≤ n) (hp : Nat.Prime p) (hD : ¬D n m) : ∃ (c : ZMod n), 2 * c ≠ 0 ∧ ¬↑p ∣ S n m c

Clause (ii) of thm:sop(b) holds when (i) does (proof of thm:sop(c)). For n ≥ 3 with n ∤ h, h+1, h+2 (h = 2m) and every prime p, including p = 2, some class c with 2c ≢ 0 (mod n) has p ∤ S(c): S(1) = 2k+1 and S(c*) ∈ {−k, −2k, k+1, 2(k+1)}.

def SopIndice.ClauseII (n m p E : ℕ) : Prop

Clause (ii) of thm:sop(b): E = 1, or S(c) ≢ 0 (mod p) for some c with 2c ≢ 0.

Equations

• SopIndice.ClauseII n m p E = (E = 1 ∨ ∃ (c : ZMod n), 2 * c ≠ 0 ∧ ¬↑p ∣ SopIndice.S n m c)

theorem SopIndice.sop_c {n m p E idx : ℕ} (hn : 3 ≤ n) (hp : Nat.Prime p) (I : Prop) (hb : p ∣ idx ↔ ¬I ∨ ¬ClauseII n m p E) (hseg : ¬I ↔ D n m) : p ∣ idx ↔ D n m

thm:sop(c), conditional. Hypotheses: hb is thm:sop(b) (p ∣ [O:A] iff (i) or (ii) fails; it needs the ring-theoretic infrastructure of orders, not formalized), and hseg is lem:seg read as "(i) fails iff n ∣ h, h+1 or h+2" (proved as Segmentos.lem_seg and Segmentos.seg_stable_of_dvd; it needs a unit a ≢ ±1, i.e. q' ∉ {1,2,3,4,6}). The arithmetic step, (ii) holds whenever (i) does, is sop_c_ii.

cor:indice

theorem SopIndice.indice_val (d e : ℕ) (W : ℕ → ℕ) (hW0 : W 0 = 1) (hd : 1 ≤ d) (hle : W 1 ≤ d) (he : e = 1 ∨ e = 2) (hc : e = 1 ↔ W 1 = d) (v vf : ℕ) (hv : v = ∑ i ∈ Finset.range e, (d - W i)) (hvf : vf = ∑ i ∈ Finset.range e, W i) : v = 2 * d - 1 - W 1 ∧ v = d - 1 + (d - W 1) ∧ vf = if W 1 = d then 1 else 1 + W 1

cor:indice, the valuations. From thm:loc(d), v_p([O:A]) = ∑_{i<e}(d − W_i) and v_p([A:f]) = ∑_{i<e} W_i, with W₀ = 1, W₁ ≤ d, e ∈ {1, 2} (from prop:mono(b) / prop:cert(b)) and e = 1 ↔ W₁ = d (thm:loc(c)): v_p([O:A]) = 2d − 1 − W₁, which is (d − 1) + (d − W₁), and v_p([A:f]) = 1 if W₁ = d, 1 + W₁ otherwise.

theorem SopIndice.indice_hminus (d W1 k vh : ℕ) (hle : W1 ≤ d) (hk : d - W1 = k) (hkv : k ≤ vh) (hv : 2 * vh < d) : d < 2 * W1

cor:indice, families of thm:hminus(a). d − W₁ = k ≤ v_p(h⁻) < d/2 gives W₁ > d/2.

theorem SopIndice.indice_dos (d W1 t : ℕ) (hle : W1 ≤ d) (ht : 3 ≤ t) (htd : t ∣ d) (h : d - W1 = d / t) : 2 * d ≤ 3 * W1 ∧ (0 < d → d < 2 * W1)

cor:indice, case (b) of cor:dos. d − W₁ = d/t with t ≥ 3, t ∣ d gives W₁ ≥ 2d/3, hence W₁ > d/2 when d > 0.

theorem SopIndice.indice_small (h n : ℕ) (he : Even h) (hn : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4) : n ∣ h ∨ n ∣ h + 1 ∨ n ∣ h + 2

cor:indice, proof. h even and q' ∈ {1,2,3,4} force q' ∣ h, h+1 or h+2 ("4 divides h or h+2, and 3 divides one of three consecutive integers").

theorem SopIndice.indice_six (m : ℕ) : ¬D 6 m ↔ m % 3 = 1

cor:indice, proof, q' = 6. 6 ∤ h, h+1, h+2 (h = 2m) iff m ≡ 1 (mod 3).

theorem SopIndice.indice_six_S (k : ℕ) : S 6 (6 * k + 1) ↑1 = 2 * ↑k + 1 ∧ S 6 (6 * k + 1) ↑2 = -(2 * ↑k) ∧ S 6 (6 * k + 4) ↑1 = 2 * ↑k + 1 ∧ S 6 (6 * k + 4) ↑2 = -(2 * (↑k + 1))

cor:indice, proof, q' = 6: "S(1) = 2k+1 and S(2) = −2k or −2(k+1) for m = 6k+1 or m = 6k+4".

theorem SopIndice.indice_six_ii {m p : ℕ} (hp : Nat.Prime p) (hm : m % 3 = 1) (E : ℕ) : ClauseII 6 m p E

cor:indice, proof, q' = 6: "these are coprime, so (ii) holds". For m ≡ 1 (mod 3) and every prime p, ClauseII 6 m p E holds (through c = 1 or c = 2).

theorem SopIndice.indice_prod {idx : ℕ} (hidx : idx ≠ 0) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (d W : ℕ → ℕ) (hv : ∀ (p : ℕ), Nat.Prime p → idx.factorization p = if p ∈ P then d p - 1 + (d p - W p) else 0) : idx = ∏ p ∈ P, p ^ (d p - 1 + (d p - W p))

cor:indice, the product formula. If v_p([O:A]) = d_p − 1 + (d_p − W₁(p)) for the primes p of a finite set P and v_p([O:A]) = 0 for every other prime (thm:sop(a),(c) and the case q' = 6, as hypotheses), then [O:A] = ∏_{p∈P} p^{d_p − 1 + (d_p − W₁(p))}.

Controls against a mistyped definition