Stable families of segments

If r divides n − 1, n or n + 1, the SU(n) segment is stable at q': the multiset of its exponents modulo q' is invariant under multiplication by every unit of ZMod q'.

Model: the exponents are integers a_j (j < n) cast into ZMod q'; the count is cnt f n c = #{j < n | f j = c} and Stable f n means cnt f n (u c) = cnt f n c for every unit u and every c. The three cases are

• n = 2m + 1: a_j = j − m (segment −m..m), q' = r;
• n = 2m, p = 2: a_j = n − 1 − 2j, q' = r with r odd;
• n = 2m, p odd: a_j = n − 1 − 2j, q' = 2r. All three follow from one abstract statement (stable_of_period): f periodic of period P, injective on [0, P), with image stable under units; the exceptional class c₀ satisfies 2 c₀ = 0, hence is fixed by every unit (unit_mul_fixed).

Main results

• NotaPuente.Families.stable_of_period: the abstract counting statement.
• NotaPuente.Families.prop_4_2_odd, NotaPuente.Families.prop_4_2_even_r, NotaPuente.Families.prop_4_2_even_2r: the three cases.

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

def NotaPuente.Families.cnt {M : ℕ} (f : ℕ → ZMod M) (n : ℕ) (c : ZMod M) : ℕ

cnt f n c = #{j < n : f j = c}.

Equations

• NotaPuente.Families.cnt f n c = {j ∈ Finset.range n | f j = c}.card

def NotaPuente.Families.Stable {M : ℕ} (f : ℕ → ZMod M) (n : ℕ) : Prop

Stability at M = q': the counting function is invariant under multiplication by units.

Equations

• NotaPuente.Families.Stable f n = ∀ (u : (ZMod M)ˣ) (c : ZMod M), NotaPuente.Families.cnt f n (↑u * c) = NotaPuente.Families.cnt f n c

theorem NotaPuente.Families.cnt_sum {M : ℕ} (f : ℕ → ZMod M) (n : ℕ) (c : ZMod M) : cnt f n c = ∑ j ∈ Finset.range n, if f j = c then 1 else 0

theorem NotaPuente.Families.cnt_zero {M : ℕ} (f : ℕ → ZMod M) (c : ZMod M) : cnt f 0 c = 0

theorem NotaPuente.Families.cnt_succ {M : ℕ} (f : ℕ → ZMod M) (n : ℕ) (c : ZMod M) : cnt f (n + 1) c = cnt f n c + if f n = c then 1 else 0

theorem NotaPuente.Families.cnt_periodic {M : ℕ} (f : ℕ → ZMod M) {P : ℕ} (hper : ∀ (j : ℕ), f (P + j) = f j) (c : ZMod M) (s k : ℕ) : cnt f (k * P + s) c = k * cnt f P c + cnt f s c

theorem NotaPuente.Families.cnt_period {M : ℕ} (f : ℕ → ZMod M) {P : ℕ} (hinj : ∀ i < P, ∀ j < P, f i = f j → i = j) (c : ZMod M) : cnt f P c = if c ∈ Finset.image f (Finset.range P) then 1 else 0

theorem NotaPuente.Families.unit_mul_fixed {M : ℕ} [NeZero M] (u : (ZMod M)ˣ) {c0 : ZMod M} (h : 2 * c0 = 0) : ↑u * c0 = c0

If 2 c0 = 0 in ZMod M, every unit fixes c0.

theorem NotaPuente.Families.unit_mul_eq_iff {M : ℕ} [NeZero M] (u : (ZMod M)ˣ) {c0 : ZMod M} (h : 2 * c0 = 0) (c : ZMod M) : c0 = ↑u * c ↔ c0 = c

theorem NotaPuente.Families.stable_of_period {M : ℕ} [NeZero M] (f : ℕ → ZMod M) {P : ℕ} (hper : ∀ (j : ℕ), f (P + j) = f j) (hinj : ∀ i < P, ∀ j < P, f i = f j → i = j) (hT : ∀ (u : (ZMod M)ˣ) (c : ZMod M), ↑u * c ∈ Finset.image f (Finset.range P) ↔ c ∈ Finset.image f (Finset.range P)) {n : ℕ} (hn : (∃ (k : ℕ), n = k * P) ∨ (∃ (k : ℕ), n = k * P + 1) ∧ 2 * f 0 = 0 ∨ (∃ (k : ℕ), n + 1 = k * P) ∧ 2 * f n = 0) : Stable f n

Abstract stability. f of period P, injective on [0, P), with image T stable under units. If P | n, or n = kP + 1 with 2 f 0 = 0, or n + 1 = kP with 2 f n = 0, then the counting function is invariant under units.

The three cases of Proposition 4.2

theorem NotaPuente.Families.image_eq_univ {M : ℕ} [NeZero M] (f : ℕ → ZMod M) (hinj : ∀ i < M, ∀ j < M, f i = f j → i = j) : Finset.image f (Finset.range M) = Finset.univ

theorem NotaPuente.Families.natCast_inj_of_lt {M i j : ℕ} (hi : i < M) (hj : j < M) (h : ↑i = ↑j) : i = j

theorem NotaPuente.Families.prop_4_2_odd {r : ℕ} (hr : 0 < r) (m : ℕ) (h : r ∣ 2 * m ∨ r ∣ 2 * m + 1 ∨ r ∣ 2 * m + 2) : Stable (fun (j : ℕ) => ↑(↑j - ↑m)) (2 * m + 1)

Proposition 4.2, n = 2m + 1 odd (segment -m..m, q' = r).

def NotaPuente.Families.fe (M m : ℕ) : ℕ → ZMod M

The even-case exponent map j ↦ n - 1 - 2j, n = 2m.

Equations

• NotaPuente.Families.fe M m j = ↑(2 * ↑m - 1 - 2 * ↑j)

theorem NotaPuente.Families.even_hn {M r : ℕ} (m : ℕ) (h2r : 2 * ↑r = 0) (h : r ∣ 2 * m - 1 ∨ r ∣ 2 * m ∨ r ∣ 2 * m + 1) (hm : 1 ≤ m) : (∃ (k : ℕ), 2 * m = k * r) ∨ (∃ (k : ℕ), 2 * m = k * r + 1) ∧ 2 * fe M m 0 = 0 ∨ (∃ (k : ℕ), 2 * m + 1 = k * r) ∧ 2 * fe M m (2 * m) = 0

The divisibility hypothesis in the even case, for any M with 2 r = 0 in ZMod M.

theorem NotaPuente.Families.fe_per {M r : ℕ} (m : ℕ) (h2r : 2 * ↑r = 0) (j : ℕ) : fe M m (r + j) = fe M m j

theorem NotaPuente.Families.prop_4_2_even_r {r : ℕ} (hr : Odd r) (m : ℕ) (h : r ∣ 2 * m - 1 ∨ r ∣ 2 * m ∨ r ∣ 2 * m + 1) : Stable (fe r m) (2 * m)

Proposition 4.2, n = 2m even, p = 2 (q' = r, r odd).

theorem NotaPuente.Families.odd_unit {r : ℕ} [NeZero (2 * r)] (u : (ZMod (2 * r))ˣ) : Odd ↑u

Units of ZMod (2 r) are odd.

theorem NotaPuente.Families.prop_4_2_even_2r {r : ℕ} (hr : 0 < r) (m : ℕ) (h : r ∣ 2 * m - 1 ∨ r ∣ 2 * m ∨ r ∣ 2 * m + 1) : Stable (fe (2 * r) m) (2 * m)

Proposition 4.2, n = 2m even, p odd (q' = 2r; the segment runs through the odd classes).