Stable intervals in ZMod n and two Laurent identities

An affine bijection x ↦ u x + b of ZMod n (u a unit) that maps a block of k consecutive residues onto itself, with 2 ≤ k ≤ n − 2, has u = ±1. The second part proves two identities for the elementary symmetric functions a1, a2 of the spectrum t^(L−1−2j), j < L.

Main results

• NotaPuente.C_interval_eq_iff: for the block {0, …, k − 1}, the number of x with x and x + t in the block is k − 1 iff t = ±1.
• NotaPuente.lemma_4_1: an affine bijection fixing a block of k consecutive residues, 2 ≤ k ≤ n − 2, has u = 1 ∨ u = −1.
• NotaPuente.lemma_5_5: for t ≠ 0 and L ≥ 2, with τ₊ = t^(L−1) + t^(−(L−1)) and τ₋ = t^(L+1) + t^(−(L+1)): (a1² − a2) τ₊ = a1 (1 + a1² − 2 a2) and a2 τ₋ = a1 (a1² − 2 a2 − 1) (division-free, through a Chebyshev recurrence and Cassini's identity).

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.

Lemma 5.5

def NotaPuente.a1 {K : Type u_1} [Field K] (t : K) (L : ℕ) : K

a1 t L = Σ_{j<L} t^(L-1-2j) (first elementary symmetric function of the spectrum).

Equations

• NotaPuente.a1 t L = ∑ j ∈ Finset.range L, t ^ (↑L - 1 - 2 * ↑j)

def NotaPuente.a2 {K : Type u_1} [Field K] (t : K) (L : ℕ) : K

a2 t L = Σ_{i<j<L} s_i s_j, s_j = t^(L-1-2j) (second elementary symmetric function).

Equations

• NotaPuente.a2 t L = ∑ j ∈ Finset.range L, ∑ i ∈ Finset.range j, t ^ (↑L - 1 - 2 * ↑i) * t ^ (↑L - 1 - 2 * ↑j)

theorem NotaPuente.s_succ {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L i : ℕ) : t ^ (↑(L + 1) - 1 - 2 * ↑i) = t * t ^ (↑L - 1 - 2 * ↑i)

theorem NotaPuente.s_last {K : Type u_1} [Field K] {t : K} (L : ℕ) : t ^ (↑(L + 1) - 1 - 2 * ↑L) = (t ^ L)⁻¹

theorem NotaPuente.s_pred {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L j : ℕ) : t ^ (↑(L + 1) - 1 - 2 * ↑(j + 1)) = t⁻¹ * t ^ (↑L - 1 - 2 * ↑j)

theorem NotaPuente.a1_succ {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a1 t (L + 1) = t * a1 t L + (t ^ L)⁻¹

x_{L+1} = t x_L + t^(-L).

theorem NotaPuente.a1_succ' {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a1 t (L + 1) = t⁻¹ * a1 t L + t ^ L

x_{L+1} = t⁻¹ x_L + t^L.

theorem NotaPuente.a1_zero {K : Type u_1} [Field K] {t : K} : a1 t 0 = 0

theorem NotaPuente.a1_two {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a1 t (L + 2) = t ^ (L + 1) + a1 t L + (t ^ (L + 1))⁻¹

x_{L+2} = t^(L+1) + x_L + t^(-(L+1)).

theorem NotaPuente.a1_cheb {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a1 t (L + 2) + a1 t L = (t + t⁻¹) * a1 t (L + 1)

Chebyshev recurrence: x_{L+2} + x_L = (t + t⁻¹) x_{L+1}.

theorem NotaPuente.a1_cassini {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a1 t (L + 1) ^ 2 - a1 t L * a1 t (L + 2) = 1

Cassini: x_{L+1}² - x_L x_{L+2} = 1.

theorem NotaPuente.a2_succ {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : a2 t (L + 1) = t ^ 2 * a2 t L + t * (t ^ L)⁻¹ * a1 t L

a2_{L+1} = t² a2_L + t · t^(-L) · x_L (spectrum of L+1 = t · spectrum of L, plus t^(-L)).

theorem NotaPuente.a2_zero {K : Type u_1} [Field K] {t : K} : a2 t 0 = 0

theorem NotaPuente.a2_one {K : Type u_1} [Field K] {t : K} : a2 t 1 = 0

theorem NotaPuente.a2_mul {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) (L : ℕ) : (t + t⁻¹) * a2 t (L + 1) = a1 t (L + 1) * a1 t L

[2] · a2_{L+1} = x_{L+1} x_L with [2] = t + t⁻¹.

theorem NotaPuente.lemma_5_5 {K : Type u_1} [Field K] {t : K} (ht : t ≠ 0) {L : ℕ} (hL : 2 ≤ L) : (a1 t L ^ 2 - a2 t L) * (t ^ (↑L - 1) + t ^ (-(↑L - 1))) = a1 t L * (1 + a1 t L ^ 2 - 2 * a2 t L) ∧ a2 t L * (t ^ (↑L + 1) + t ^ (-(↑L + 1))) = a1 t L * (a1 t L ^ 2 - 2 * a2 t L - 1)

Lemma 5.5 of the note. For L ≥ 2, t ≠ 0 in a field, spectrum s_j = t^(L-1-2j) (j < L), a1 = Σ s_j, a2 = Σ_{i<j} s_i s_j, τ₊ = t^(L-1) + t^(-(L-1)), τ₋ = t^(L+1) + t^(-(L+1)): (a1² - a2) τ₊ = a1 (1 + a1² - 2 a2) and a2 τ₋ = a1 (a1² - 2 a2 - 1). Valid for every t ≠ 0 (no t² ≠ 1 hypothesis): the proof is division-free, via the recurrences x_{L+2} + x_L = [2] x_{L+1}, Cassini x_{L+1}² - x_L x_{L+2} = 1, and [2] a2_{L+1} = x_{L+1} x_L.

Lemma 4.1

def NotaPuente.C {n : ℕ} (I : Finset (ZMod n)) (t : ZMod n) : ℕ

Autocorrelation C I t = #{x ∈ I : x + t ∈ I} = |I ∩ (I - t)| (same cardinality as the paper's |I ∩ (I + t)|, by the translation x ↦ x + t).

Equations

• NotaPuente.C I t = {x ∈ I | x + t ∈ I}.card

theorem NotaPuente.C_affine {n : ℕ} (u : (ZMod n)ˣ) (b : ZMod n) (J : Finset (ZMod n)) (t : ZMod n) : C (Finset.image (fun (x : ZMod n) => ↑u * x + b) J) (↑u * t) = C J t

Affine invariance: for α x = u x + b (u a unit), C (α J) (u t) = C J t.

theorem NotaPuente.arith {n a m k : ℕ} (ha : a < n) (hm : m < n) (hk : k ≤ n) : a < k ∧ (a + m) % n < k ↔ a < k - m ∨ n - m ≤ a ∧ a < k

theorem NotaPuente.mem_J {n : ℕ} [NeZero n] {k : ℕ} (hk : k ≤ n) (x : ZMod n) : x ∈ Finset.image Nat.cast (Finset.range k) ↔ x.val < k

theorem NotaPuente.C_J {n : ℕ} [NeZero n] {k : ℕ} (hk : k ≤ n) (t : ZMod n) : C (Finset.image Nat.cast (Finset.range k)) t = k - t.val + (k - (n - t.val))

Exact count for the block {0, …, k-1}: C = (k - m) + (k - (n - m)), m = t.val (truncated subtraction, i.e. max(0, k-m) + max(0, k-n+m)).

theorem NotaPuente.C_interval_eq_iff {n : ℕ} [NeZero n] {k : ℕ} (hk2 : 2 ≤ k) (hkn : k + 2 ≤ n) (t : ZMod n) : C (Finset.image Nat.cast (Finset.range k)) t = k - 1 ↔ t = 1 ∨ t = -1

Counting fact. For the block {0,…,k-1} ⊆ ZMod n, 2 ≤ k ≤ n - 2: C t = k - 1 ↔ t = 1 ∨ t = -1.

theorem NotaPuente.lemma_4_1 {n : ℕ} (hn : 3 ≤ n) {k : ℕ} (hk2 : 2 ≤ k) (hkn : k + 2 ≤ n) (b0 : ZMod n) (u : (ZMod n)ˣ) (b : ZMod n) (h : Finset.image (fun (x : ZMod n) => ↑u * x + b) (Finset.image (fun (i : ℕ) => b0 + ↑i) (Finset.range k)) = Finset.image (fun (i : ℕ) => b0 + ↑i) (Finset.range k)) : u = 1 ∨ u = -1

Lemma 4.1 of the note (stable intervals). Let n ≥ 3 (n = q'), I = {b0, b0+1, …, b0+k-1} ⊆ ZMod n with 2 ≤ k ≤ n - 2, and α x = u x + b with u a unit. If α(I) = I then u = 1 ∨ u = -1.