Segments: which multisets j ≡ ±c (mod n) are stable under a unit

For N(c) = #{1 ≤ j ≤ m | j ≡ ±c (mod n)} (with h = 2m) and n ≥ 3, N is stable under multiplication by a unit a ≢ ±1 iff n ∣ h, n ∣ h + 1 or n ∣ h + 2; in that case it is stable under every unit. The core is a lemma of Amiot: an interval of k elements of ℤ/n, 1 < k < n − 1, is not stable under multiplication by a unit a ≢ ±1. The proof reduces m to m mod n (complete periods), reflects r ↦ n − 1 − r, and counts #{x ∈ I | x + d ∈ I}.

The odd case is the same content as NotaPuente.Families.prop_4_2_odd (through SU(2m+1) = Sp(2m)), counted differently; no bridge between the two counts is formalized.

Main results

• Segmentos.amiot_interval: Amiot's lemma, for every n and every interval.
• Segmentos.seg_stable_of_dvd: if n ∣ h, h + 1 or h + 2, N is stable under every unit.
• Segmentos.lem_seg: the equivalence for n ≥ 3 and a ≢ ±1.
• Segmentos.familias, Segmentos.familias_m6: the column m mod n of the table of families and its examples for m = 6.

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

Objects

def Segmentos.N (n m : ℕ) (c : ZMod n) : ℕ

N^{(n)}(c) = #{1 ≤ j ≤ m : j ≡ ±c (mod n)}. It satisfies N(-c) = N(c), so it is the multiset of the paper on the classes (ℤ/n)/±1.

Equations

• Segmentos.N n m c = {j ∈ Finset.Icc 1 m | ↑j = c ∨ ↑j = -c}.card

def Segmentos.Stable (n m : ℕ) (a : ZMod n) : Prop

N^{(n)} is stable under c ↦ a c (as a multiset: N(a c) = N(c) for every class).

Equations

• Segmentos.Stable n m a = ∀ (c : ZMod n), Segmentos.N n m (a * c) = Segmentos.N n m c

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

n ∣ h, n ∣ h + 1 or n ∣ h + 2, with h = 2m.

Equations

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

@[instance_reducible]

instance Segmentos.instDecidableD (n m : ℕ) : Decidable (D n m)

Equations

• Segmentos.instDecidableD n m = id inferInstance

theorem Segmentos.N_neg (n m : ℕ) (c : ZMod n) : N n m (-c) = N n m c

Arithmetic helpers

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

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

theorem Segmentos.D_iff {n m : ℕ} (hn : 0 < n) : D n m ↔ m % n = 0 ∨ 2 * (m % n) = n ∨ 2 * (m % n) + 1 = n ∨ 2 * (m % n) + 2 = n ∨ m % n + 1 = n

D n m only depends on r = m mod n, and reads r ∈ {0, n-1}, 2r ∈ {n, n-1, n-2}.

theorem Segmentos.natCast_eq_zero_iff_mod {n : ℕ} (j : ℕ) : ↑j = 0 ↔ j % n = 0

theorem Segmentos.card_Ioc_period {n : ℕ} [NeZero n] (P : ZMod n → Prop) [DecidablePred P] (m : ℕ) : {j ∈ Finset.Ioc m (m + n) | P ↑j}.card = (Finset.filter P Finset.univ).card

n consecutive integers m+1, …, m+n represent each class of ℤ/n once.

theorem Segmentos.card_mul_unit {n : ℕ} [NeZero n] (u : (ZMod n)ˣ) (P : ZMod n → Prop) [DecidablePred P] : {x : ZMod n | P (↑u * x)}.card = (Finset.filter P Finset.univ).card

def Segmentos.K (n : ℕ) [NeZero n] (c : ZMod n) : ℕ

K(c) = #{x : x = ±c}: the contribution of one complete period.

Equations

• Segmentos.K n c = {x : ZMod n | x = c ∨ x = -c}.card

def Segmentos.K0 (n : ℕ) [NeZero n] (c : ZMod n) : ℕ

K0(c) = #{x ≠ 0 : x = ±c}.

Equations

• Segmentos.K0 n c = {x : ZMod n | x ≠ 0 ∧ (x = c ∨ x = -c)}.card

theorem Segmentos.K_unit {n : ℕ} [NeZero n] (u : (ZMod n)ˣ) (c : ZMod n) : K n (↑u * c) = K n c

theorem Segmentos.K0_unit {n : ℕ} [NeZero n] (u : (ZMod n)ˣ) (c : ZMod n) : K0 n (↑u * c) = K0 n c

theorem Segmentos.N_add_period {n : ℕ} [NeZero n] (m : ℕ) (c : ZMod n) : N n (m + n) c = N n m c + K n c

One more complete period adds K(c).

theorem Segmentos.N_add_mul {n : ℕ} [NeZero n] (r q : ℕ) (c : ZMod n) : N n (r + n * q) c = N n r c + q * K n c

theorem Segmentos.N_eq_mod {n : ℕ} [NeZero n] (m : ℕ) (c : ZMod n) : N n m c = N n (m % n) c + m / n * K n c

Complete periods contribute a unit-invariant multiset: N_m = N_{m mod n} + ⌊m/n⌋ K.

theorem Segmentos.stable_mod {n : ℕ} [NeZero n] (m : ℕ) (u : (ZMod n)ˣ) : Stable n m ↑u ↔ Stable n (m % n) ↑u

theorem Segmentos.N_reflect {n : ℕ} [NeZero n] {r : ℕ} (hr : r < n) (c : ZMod n) : N n r c + N n (n - 1 - r) c = K0 n c

Reflection: N_r + N_{n-1-r} = K0 for r < n.

theorem Segmentos.stable_reflect {n : ℕ} [NeZero n] {r : ℕ} (hr : r < n) (u : (ZMod n)ˣ) : Stable n r ↑u ↔ Stable n (n - 1 - r) ↑u

def Segmentos.Pm (n s : ℕ) (c : ZMod n) : Prop

The predicate "c ∈ [-s, s] and c ≠ 0".

Equations

• Segmentos.Pm n s c = ((c + ↑s).val < 2 * s + 1 ∧ c ≠ 0)

@[instance_reducible]

instance Segmentos.instDecidablePm (n s : ℕ) (c : ZMod n) : Decidable (Pm n s c)

Equations

• Segmentos.instDecidablePm n s c = id inferInstance

theorem Segmentos.N_small {n : ℕ} [NeZero n] {s : ℕ} (hs : 2 * s < n) (c : ZMod n) : N n s c = if Pm n s c then 1 else 0

For 2s < n the segment {±1, …, ±s} has no repetitions: N_s is the indicator of [-s, s] \ {0}.

theorem Segmentos.Pm_iff {n : ℕ} [NeZero n] {s : ℕ} (hs : 2 * s < n) (hcase : s = 0 ∨ n = 2 * s + 1 ∨ n = 2 * s + 2) (c : ZMod n) : Pm n s c ↔ s ≠ 0 ∧ c ≠ 0 ∧ c + c ≠ 0

In the three families, Pm is a unit-invariant condition.

theorem Segmentos.stable_small_of {n : ℕ} [NeZero n] {s : ℕ} (hs : 2 * s < n) (hcase : s = 0 ∨ n = 2 * s + 1 ∨ n = 2 * s + 2) (u : (ZMod n)ˣ) : Stable n s ↑u

Amiot's lemma

theorem Segmentos.nat_count {n k t : ℕ} (ht1 : 1 ≤ t) (htn : t < n) (hk : k ≤ n) : {i ∈ Finset.range n | i < k ∧ (i + t) % n < k}.card = k - t + (k - (n - t))

Exactly max(0, k-t) + max(0, k-n+t) elements i of {0,…,k-1} have i + t mod n in it.

theorem Segmentos.interval_count {n : ℕ} [NeZero n] {k : ℕ} (hk : k ≤ n) (c₀ d : ZMod n) (hd : d.val ≠ 0) : {x : ZMod n | (x - c₀).val < k ∧ (x + d - c₀).val < k}.card = k - d.val + (k - (n - d.val))

#{x ∈ I : x + d ∈ I} for the interval I = {c₀, …, c₀ + k - 1} of ℤ/n.

theorem Segmentos.amiot_interval {n k : ℕ} (hk1 : 1 < k) (hk2 : k < n - 1) (c₀ : ZMod n) (a : (ZMod n)ˣ) (ha1 : ↑a ≠ 1) (ha2 : ↑a ≠ -1) : ¬∀ (x : ZMod n), (x - c₀).val < k → (↑a * x - c₀).val < k

Amiot's lemma (core of lem:seg; [Ami09, Thm. 1]). Let 1 < k < n - 1 and let a be a unit of ℤ/n with a ≢ ±1. Then no interval I = {c₀, c₀+1, …, c₀+k-1} of k elements of ℤ/n satisfies a I ⊆ I (in particular a I ≠ I).

Lemma lem:seg

theorem Segmentos.small_only {n s : ℕ} [NeZero n] (hn : 3 ≤ n) (hs : 2 * s < n) (a : (ZMod n)ˣ) (ha1 : ↑a ≠ 1) (ha2 : ↑a ≠ -1) (H : Stable n s ↑a) : s = 0 ∨ n ≤ 2 * s + 2

theorem Segmentos.seg_stable_of_dvd {n m : ℕ} (hn : 3 ≤ n) (hD : D n m) (u : (ZMod n)ˣ) : Stable n m ↑u

lem:seg, second sentence: if n ∣ h, n ∣ h + 1 or n ∣ h + 2 (h = 2m), then N^{(n)} is stable under every unit.

theorem Segmentos.lem_seg {n m : ℕ} (hn : 3 ≤ n) (a : (ZMod n)ˣ) (ha1 : ↑a ≠ 1) (ha2 : ↑a ≠ -1) : Stable n m ↑a ↔ D n m

Lemma lem:seg (segments). Let n ≥ 3 and let a be a unit mod n with a ≢ ±1. Then N^{(n)} is stable under c ↦ a c iff n divides h, h + 1 or h + 2 (h = 2m).

theorem Segmentos.familias {n m : ℕ} (hn : 3 ≤ n) : (n ∣ 2 * m ↔ m % n = 0 ∨ 2 * (m % n) = n) ∧ (n ∣ 2 * m + 1 ↔ 2 * (m % n) + 1 = n) ∧ (n ∣ 2 * m + 2 ↔ m % n = n - 1 ∨ 2 * (m % n) + 2 = n)

The m mod n column of Table tab:familias.

theorem Segmentos.familias_m6 : {n ∈ Finset.Icc 3 30 | D n 6} = {3, 4, 6, 7, 12, 13, 14}

Examples column of Table tab:familias (m = 6, 3 ≤ n ≤ 30).