The type-C residue identity and the capacity criterion

For a vector x ∈ ℤ^m, taken through its reduction modulo q as a list over ZMod q (or over a finite abelian group G), the residue R x of the type-C positive roots in ℤ[G] satisfies 2 R x + 2m = P(x)² + P(2x). Counting classes gives 4 N + 2m = ∑_g o(g)² + ∑_{2g = 0} o(g), where o(g) is the multiplicity of g. Hence N_q(x) ≥ N_q(ρ) with equality iff x meets the capacities o(g) ≤ d (d q = 2m + 2), and then R x = R ρ.

Main results

• ResidueCapacity.eq_res: the residue identity.
• ResidueCapacity.four_N: the class count.
• ResidueCapacity.cap_criterion_gen, ResidueCapacity.conj_cap: the capacity criterion.
• ResidueCapacity.prop_res_cap: R x = R ρ under the capacities.

References

• C. Marín, Integer character values on the ρ-line of Sp(2m), Zenodo (2026), doi:10.5281/zenodo.22683560.

@[reducible, inline]

noncomputable abbrev ResidueCapacity.s {G : Type u_1} (g : G) : AddMonoidAlgebra ℤ G

The basis element X^g of ℤ[G].

Equations

• ResidueCapacity.s g = AddMonoidAlgebra.single g 1

theorem ResidueCapacity.s_mul {G : Type u_1} [AddCommGroup G] (a b : G) : s a * s b = s (a + b)

theorem ResidueCapacity.s_zero {G : Type u_1} [AddCommGroup G] : s 0 = 1

noncomputable def ResidueCapacity.P {G : Type u_1} [AddCommGroup G] : List G → AddMonoidAlgebra ℤ G

P_x = Σ_i (X^{x_i} + X^{-x_i}).

Equations

• ResidueCapacity.P [] = 0
• ResidueCapacity.P (a :: xs) = ResidueCapacity.s a + ResidueCapacity.s (-a) + ResidueCapacity.P xs

def ResidueCapacity.posRootVals {G : Type u_1} [AddCommGroup G] : List G → List G

The values (x,α) for the positive roots α of C_m, listed recursively: for x = (a, x₂, …) the roots 2e₁, then e₁ - e_j, e₁ + e_j (j > 1), then those of the tail.

Equations

• ResidueCapacity.posRootVals [] = []
• ResidueCapacity.posRootVals (a :: xs) = 2 • a :: List.flatMap (fun (b : G) => [a - b, a + b]) xs ++ ResidueCapacity.posRootVals xs

noncomputable def ResidueCapacity.R {G : Type u_1} [AddCommGroup G] (x : List G) : AddMonoidAlgebra ℤ G

ℛ_x = Σ_{α ∈ Φ(C_m)} X^{(x,α)}, with Φ = Φ⁺ ∪ -Φ⁺.

Equations

• ResidueCapacity.R x = (List.map (fun (v : G) => ResidueCapacity.s v + ResidueCapacity.s (-v)) (ResidueCapacity.posRootVals x)).sum

theorem ResidueCapacity.cross {G : Type u_1} [AddCommGroup G] (a : G) (xs : List G) : (s a + s (-a)) * P xs = (List.map (fun (v : G) => s v + s (-v)) (List.flatMap (fun (b : G) => [a - b, a + b]) xs)).sum

theorem ResidueCapacity.eq_res {G : Type u_1} [AddCommGroup G] (x : List G) : 2 • R x + (2 * x.length) • 1 = P x ^ 2 + P (List.map (fun (a : G) => 2 • a) x)

Part 2: occupancies and the count N_q

def ResidueCapacity.o {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) : ℤ

Coefficient of P_x at g: o_x(g) = #{i : x_i = g} + #{i : -x_i = g}.

Equations

• ResidueCapacity.o x g = (List.map (fun (b : G) => (if b = g then 1 else 0) + if -b = g then 1 else 0) x).sum

def ResidueCapacity.Nq {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) : ℕ

N_q(x) = #{α > 0 : (x,α) ≡ 0}.

Equations

• ResidueCapacity.Nq x = List.count 0 (ResidueCapacity.posRootVals x)

@[simp]

theorem ResidueCapacity.o_nil {G : Type u_1} [AddCommGroup G] [DecidableEq G] (g : G) : o [] g = 0

theorem ResidueCapacity.o_cons {G : Type u_1} [AddCommGroup G] [DecidableEq G] (a : G) (xs : List G) (g : G) : o (a :: xs) g = ((if a = g then 1 else 0) + if -a = g then 1 else 0) + o xs g

theorem ResidueCapacity.o_neg {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) : o x (-g) = o x g

theorem ResidueCapacity.o_sum {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (x : List G) : ∑ g : G, o x g = 2 * ↑x.length

theorem ResidueCapacity.o_nonneg {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) : 0 ≤ o x g

theorem ResidueCapacity.fixed_iff {G : Type u_1} [AddCommGroup G] (a : G) : 2 • a = 0 ↔ -a = a

theorem ResidueCapacity.o_fixed_even {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) (hg : 2 • g = 0) : Even (o x g)

theorem ResidueCapacity.count_eq_sum {G : Type u_1} [DecidableEq G] (l : List G) (a : G) : ↑(List.count a l) = (List.map (fun (v : G) => if v = a then 1 else 0) l).sum

theorem ResidueCapacity.cross_count {G : Type u_1} [AddCommGroup G] [DecidableEq G] (a : G) (xs : List G) : (List.map (fun (v : G) => if v = 0 then 1 else 0) (List.flatMap (fun (b : G) => [a - b, a + b]) xs)).sum = o xs a

theorem ResidueCapacity.Nq_cons {G : Type u_1} [AddCommGroup G] [DecidableEq G] (a : G) (xs : List G) : ↑(Nq (a :: xs)) = (if 2 • a = 0 then 1 else 0) + o xs a + ↑(Nq xs)

theorem ResidueCapacity.sum_u_mul {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (a : G) (f : G → ℤ) : ∑ g : G, ((if a = g then 1 else 0) + if -a = g then 1 else 0) * f g = f a + f (-a)

theorem ResidueCapacity.sum_u_sq {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (a : G) : ∑ g : G, ((if a = g then 1 else 0) + if -a = g then 1 else 0) ^ 2 = 2 + 2 * if 2 • a = 0 then 1 else 0

theorem ResidueCapacity.sum_fix_u {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (a : G) : (∑ g : G, if 2 • g = 0 then (if a = g then 1 else 0) + if -a = g then 1 else 0 else 0) = 2 * if 2 • a = 0 then 1 else 0

theorem ResidueCapacity.four_N {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (x : List G) : 4 * ↑(Nq x) + 2 * ↑x.length = ∑ g : G, (o x g ^ 2 + if 2 • g = 0 then o x g else 0)

Key identity (equivalent to eq:Nclases of the paper): 4 N_q(x) + 2m = Σ_g o_x(g)² + Σ_{2g=0} o_x(g).

Part 3: capacities and the criterion N_q(x) = r_q (Corollary conj:cap)

def ResidueCapacity.occ {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) : ℕ

Folded occupancy n_c: number of entries of x lying in the folded class {g, -g}.

Equations

• ResidueCapacity.occ x g = List.countP (fun (a : G) => decide (a = g ∨ a = -g)) x

theorem ResidueCapacity.o_eq_occ {G : Type u_1} [AddCommGroup G] [DecidableEq G] (x : List G) (g : G) : o x g = if 2 • g = 0 then 2 * ↑(occ x g) else ↑(occ x g)

o_x(g) = 2 n_c on a fixed class (2g = 0), o_x(g) = n_c on a non-fixed one.

def ResidueCapacity.Cap {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (x : List G) : Prop

The capacities of Corollary conj:cap: each non-fixed folded class holds at most d entries and each fixed class (2g = 0, i.e. g = -g) at most ⌊d/2⌋.

Equations

• ResidueCapacity.Cap d x = ∀ (g : G), (2 • g ≠ 0 → ResidueCapacity.occ x g ≤ d) ∧ (2 • g = 0 → ResidueCapacity.occ x g ≤ d / 2)

theorem ResidueCapacity.cap_iff {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (x : List G) : Cap d x ↔ ∀ (g : G), o x g ≤ ↑d

The capacities say exactly o_x(g) ≤ d for every g.

def ResidueCapacity.eps (d : ℕ) : ℤ

ε(d) = 1 for d even, 0 for d odd.

Equations

• ResidueCapacity.eps d = if Even d then 1 else 0

def ResidueCapacity.slack {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (g : G) (n : ℤ) : ℤ

Per-class slack of the cost n² + [2g=0] n above its supporting line of slope 2d-1.

Equations

• ResidueCapacity.slack d g n = if 2 • g = 0 then (n - ↑d + 1) ^ 2 - ResidueCapacity.eps d else (n - ↑d) * (n - ↑d + 1)

def ResidueCapacity.cst {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (g : G) : ℤ

Per-class intercept of that supporting line.

Equations

• ResidueCapacity.cst d g = if 2 • g = 0 then (↑d - 1) ^ 2 - ResidueCapacity.eps d else ↑d * (↑d - 1)

theorem ResidueCapacity.cost_eq {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (g : G) (n : ℤ) : (n ^ 2 + if 2 • g = 0 then n else 0) = slack d g n + (2 * ↑d - 1) * n - cst d g

theorem ResidueCapacity.slack_nonneg {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (x : List G) (g : G) : 0 ≤ slack d g (o x g)

theorem ResidueCapacity.le_of_slack_zero {G : Type u_1} [AddCommGroup G] [DecidableEq G] (d : ℕ) (g : G) (n : ℤ) (h : slack d g n = 0) : n ≤ ↑d

def ResidueCapacity.bump {G : Type u_1} [AddCommGroup G] [DecidableEq G] (c g : G) : ℤ

bump c g = [g = c] + [g = -c] (the coefficient of X^c + X^{-c} at g).

Equations

• ResidueCapacity.bump c g = (if c = g then 1 else 0) + if -c = g then 1 else 0

theorem ResidueCapacity.sum_deficit {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) (hcard : ↑(Fintype.card G) * ↑d = 2 * ↑x.length + 2) : ∑ h : G, (↑d - o x h) = 2

theorem ResidueCapacity.slack_eq_zero_of_cap {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) (hcard : ↑(Fintype.card G) * ↑d = 2 * ↑x.length + 2) (hcap : ∀ (g : G), o x g ≤ ↑d) (g : G) : slack d g (o x g) = 0

theorem ResidueCapacity.four_N_slack {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) : 4 * ↑(Nq x) + 2 * ↑x.length = ∑ g : G, slack d g (o x g) + (2 * ↑d - 1) * (2 * ↑x.length) - ∑ g : G, cst d g

theorem ResidueCapacity.cap_criterion_gen {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x y : List G) (hlen : x.length = y.length) (hcard : ↑(Fintype.card G) * ↑d = 2 * ↑y.length + 2) (hy : ∀ (g : G), o y g ≤ ↑d) : Nq y ≤ Nq x ∧ (Nq x = Nq y ↔ ∀ (g : G), o x g ≤ ↑d)

Generic form of the capacity criterion: if a reference vector y meets the capacities and |G| · d = 2m + 2, then N(y) ≤ N(x) for every x of the same length, with equality iff x meets the capacities.

Shape of the occupancies under the capacities

theorem ResidueCapacity.shape_even {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) (hcard : ↑(Fintype.card G) * ↑d = 2 * ↑x.length + 2) (hcap : ∀ (g : G), o x g ≤ ↑d) (hd : Even d) : ∃ (c : G), ∀ (g : G), o x g = ↑d - bump c g

d even: exactly one folded class {c, -c} falls short, o_x = d - [g=c] - [g=-c].

theorem ResidueCapacity.shape_odd {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) (hcard : ↑(Fintype.card G) * ↑d = 2 * ↑x.length + 2) (hcap : ∀ (g : G), o x g ≤ ↑d) (hd : ¬Even d) (hfix : 2 ≤ ∑ g : G, if 2 • g = 0 then 1 else 0) (g : G) : o x g = ↑d - if 2 • g = 0 then 1 else 0

d odd: the capacities are saturated, o_x = d - [2g = 0], provided G has at least two fixed points (true for ZMod q, q even).

P_x through its coefficients

theorem ResidueCapacity.P_eq_sum {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (x : List G) : P x = ∑ g : G, o x g • s g

theorem ResidueCapacity.P2_eq_sum {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (x : List G) : P (List.map (fun (a : G) => 2 • a) x) = ∑ g : G, o x g • s (2 • g)

theorem ResidueCapacity.T_mul_s {G : Type u_1} [AddCommGroup G] [Fintype G] (c : G) : (∑ g : G, s g) * s c = ∑ g : G, s g

theorem ResidueCapacity.T_mul_T {G : Type u_1} [AddCommGroup G] [Fintype G] : (∑ g : G, s g) * ∑ g : G, s g = ↑(Fintype.card G) * ∑ g : G, s g

theorem ResidueCapacity.val_even {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (d : ℕ) (x : List G) (c : G) (h : ∀ (g : G), o x g = ↑d - bump c g) : P x ^ 2 + P (List.map (fun (a : G) => 2 • a) x) = (↑d * ↑d * ↑(Fintype.card G) - 4 * ↑d) * ∑ g : G, s g + 2 + ↑d * ∑ g : G, s (2 • g)

d even: with P_x = d·T - X^c - X^{-c}, the value of P_x² + P_x(X²) does not depend on c.

theorem ResidueCapacity.two_smul_cancel {G : Type u_1} {a b : AddMonoidAlgebra ℤ G} (h : 2 • a = 2 • b) : a = b

ℤ[G] is torsion-free: 2a = 2b → a = b.

Part 4: G = ZMod q, the vector ρ, and the paper's statements

def ResidueCapacity.rho (q m : ℕ) : List (ZMod q)

ρ = (m, m-1, …, 1), reduced mod q.

Equations

• ResidueCapacity.rho q m = List.map (fun (i : ℕ) => ↑(i + 1)) (List.range m).reverse

theorem ResidueCapacity.rho_length (q m : ℕ) : (rho q m).length = m

theorem ResidueCapacity.rho_succ (q m : ℕ) : rho q (m + 1) = ↑(m + 1) :: rho q m

theorem ResidueCapacity.o_rho (q m : ℕ) (g : ZMod q) : o (rho q m) g = ∑ i ∈ Finset.range m, ((if ↑(i + 1) = g then 1 else 0) + if -↑(i + 1) = g then 1 else 0)

theorem ResidueCapacity.sum_ite_card {ι : Type u_2} (t : Finset ι) (p : ι → Prop) [DecidablePred p] : (∑ i ∈ t, if p i then 1 else 0) = ↑(Finset.filter p t).card

theorem ResidueCapacity.card_bound {q m d : ℕ} [NeZero q] (hd : d * q = 2 * m + 2) (g : ZMod q) : {i ∈ Finset.range m | ↑(i + 1) = g}.card + {i ∈ Finset.range m | -↑(i + 1) = g}.card ≤ d

Every residue class mod q meets {±1, …, ±m} (an interval of dq - 2 integers) at most d times.

theorem ResidueCapacity.o_rho_le {q m d : ℕ} [NeZero q] (hd : d * q = 2 * m + 2) (g : ZMod q) : o (rho q m) g ≤ ↑d

ρ meets the capacities: o_ρ(g) ≤ d for every residue g.

theorem ResidueCapacity.card_hyp {q m d : ℕ} [NeZero q] (hd : d * q = 2 * m + 2) (x : List (ZMod q)) (hx : x.length = m) : ↑(Fintype.card (ZMod q)) * ↑d = 2 * ↑x.length + 2

theorem ResidueCapacity.two_fixed {q : ℕ} [NeZero q] (hq : Even q) : 2 ≤ ∑ g : ZMod q, if 2 • g = 0 then 1 else 0

ZMod q with q even has the two fixed points 0 and q/2.

theorem ResidueCapacity.conj_cap {q m d : ℕ} [NeZero q] (hd : d * q = 2 * m + 2) (x : List (ZMod q)) (hx : x.length = m) : Nq (rho q m) ≤ Nq x ∧ (Nq x = Nq (rho q m) ↔ Cap d x)

Corollary conj:cap. Let q ∣ 2m+2, d = (2m+2)/q (hypothesis d * q = 2m + 2), and let x be any vector of length m over ZMod q (e.g. ℓ = λ + ρ reduced mod q; Nq x is then N_q(ℓ) = #{α > 0 : q ∣ (ℓ, α)}). Then N_q(ρ) ≤ N_q(x), and N_q(x) = r_q = N_q(ρ) iff each non-fixed folded class mod q holds at most d entries and each fixed class at most ⌊d/2⌋ (Cap d x).

theorem ResidueCapacity.prop_res_cap {q m d : ℕ} [NeZero q] (hd : d * q = 2 * m + 2) (x : List (ZMod q)) (hx : x.length = m) (hcap : Cap d x) : R x = R (rho q m)

Proposition prop:res, second half. For q ∣ 2m+2 (d * q = 2m+2) and every x of length m over ZMod q meeting the capacities of conj:cap, ℛ_x = ℛ_ρ in ℤ[ZMod q].