Divisibility counts of the six positive-root values of G2 at q = 2, 3

Combinatorial half of Corollary cor:g2 of "characters at a_P". For lambda = a w1 + b w2, the six values (lambda+rho, alpha) are u, v, u+v, 2u+v, 3u+v, 3u+2v with u = a+1, v = 3(b+1); N_q counts those divisible by q and r_q the same count on 1,3,4,5,6,9. We prove N_3 = r_3 iff a is not 2 mod 3 and N_2 = r_2 iff a, b are not both odd, together with the strict forms N_q > r_q. The identification of "character vanishes at a_P^k" with "N_q > r_q" is the paper's criterion and is NOT formalized; no Lie theory is used.

Main results

• KostantAlphabet.G2Counts.N_three_eq_iff: N_3 = r_3 iff a is not 2 mod 3
• KostantAlphabet.G2Counts.N_two_eq_iff: N_2 = r_2 iff a, b are not both odd
• KostantAlphabet.G2Counts.N_three_gt_iff: r_3 < N_3 iff a = 2 mod 3
• KostantAlphabet.G2Counts.N_two_gt_iff: r_2 < N_2 iff a, b both odd

References

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

def KostantAlphabet.G2Counts.values (a b : ℕ) : List ℕ

The six values (λ+ρ, α) for λ = aω₁ + bω₂.

Equations

• KostantAlphabet.G2Counts.values a b = [a + 1, 3 * (b + 1), a + 1 + 3 * (b + 1), 2 * (a + 1) + 3 * (b + 1), 3 * (a + 1) + 3 * (b + 1), 3 * (a + 1) + 2 * (3 * (b + 1))]

def KostantAlphabet.G2Counts.N (q a b : ℕ) : ℕ

N_q(λ): number of the six values divisible by q.

Equations

• KostantAlphabet.G2Counts.N q a b = List.countP (fun (x : ℕ) => decide (q ∣ x)) (KostantAlphabet.G2Counts.values a b)

def KostantAlphabet.G2Counts.r (q : ℕ) : ℕ

r_q: multiples of q among 1,3,4,5,6,9.

Equations

• KostantAlphabet.G2Counts.r q = List.countP (fun (x : ℕ) => decide (q ∣ x)) [1, 3, 4, 5, 6, 9]

theorem KostantAlphabet.G2Counts.r_three : r 3 = 3

theorem KostantAlphabet.G2Counts.r_two : r 2 = 2

theorem KostantAlphabet.G2Counts.N_three_eq_iff (a b : ℕ) : N 3 a b = r 3 ↔ ¬a % 3 = 2

q = 3: N₃ = r₃ ↔ a ≢ 2 (3).

theorem KostantAlphabet.G2Counts.N_two_eq_iff (a b : ℕ) : N 2 a b = r 2 ↔ ¬(a % 2 = 1 ∧ b % 2 = 1)

q = 2: N₂ = r₂ ↔ ¬(a, b both odd).

theorem KostantAlphabet.G2Counts.N_three_gt_iff (a b : ℕ) : r 3 < N 3 a b ↔ a % 3 = 2

q = 3: N₃ > r₃ exactly when a ≡ 2 (3) (and N₃ ≥ r₃ always).

theorem KostantAlphabet.G2Counts.N_two_gt_iff (a b : ℕ) : r 2 < N 2 a b ↔ a % 2 = 1 ∧ b % 2 = 1

q = 2: N₂ > r₂ exactly when a, b both odd.