The number of monomials e₂^a e₃^b of weight k

The power sum s_k at e₁ = 0 is, by Newton–Waring, a combination with no vanishing coefficient of the monomials e₂^a e₃^b with 2a + 3b = k; dividing out the common monomial leaves a polynomial Q_k in u = e₂³/e₃² with deg Q_k = #{(a, b) ∈ ℕ² | 2a + 3b = k} − 1. This file proves the combinatorial half of that statement: the count of pairs in closed form, #{(a, b) | 2a + 3b = k} = ⌊k/6⌋ + 1 − [k ≡ 1 (mod 6)], and that for k ≥ 3 it equals 1 (i.e. deg Q_k = 0) exactly for k ∈ {3, 4, 5, 7}.

The identification of deg Q_k + 1 with this count (Newton–Waring with nonvanishing coefficients) is not formalized here.

Main results

• P3d.card_degreePairs: #{(a, b) | 2a + 3b = k} = k / 6 + 1 − [k % 6 = 1], for every k.
• P3d.card_degreePairs_eq_one_iff: for k ≥ 3, the count is 1 iff k ∈ {3, 4, 5, 7}.

References

• C. Marín, Subsets of F_p with two prescribed moments, Part II: every exponent, Zenodo (2026), doi:10.5281/zenodo.22886543, Proposition prop:grado.

def P3d.degreePairs (k : ℕ) : Finset (ℕ × ℕ)

The pairs (a, b) ∈ ℕ² with 2a + 3b = k (both coordinates are at most k).

Equations

• P3d.degreePairs k = {p ∈ Finset.range (k + 1) ×ˢ Finset.range (k + 1) | 2 * p.1 + 3 * p.2 = k}

theorem P3d.mem_degreePairs {k : ℕ} {p : ℕ × ℕ} : p ∈ degreePairs k ↔ 2 * p.1 + 3 * p.2 = k

theorem P3d.card_degreePairs_eq_count (k : ℕ) : (degreePairs k).card = Nat.count (fun (x : ℕ) => x ≡ k [MOD 2]) (k / 3 + 1)

Projecting to b: the pairs are in bijection with b < k / 3 + 1, b ≡ k (mod 2).

theorem P3d.card_degreePairs (k : ℕ) : (degreePairs k).card = k / 6 + 1 - if k % 6 = 1 then 1 else 0

Proposition prop:grado (combinatorial half): #{(a, b) ∈ ℕ² | 2a + 3b = k} = ⌊k/6⌋ + 1 − [k ≡ 1 (mod 6)].

theorem P3d.card_degreePairs_eq_one_iff {k : ℕ} (hk : 3 ≤ k) : (degreePairs k).card = 1 ↔ k = 3 ∨ k = 4 ∨ k = 5 ∨ k = 7

For k ≥ 3 the count is 1 (deg Q_k = 0) exactly for k ∈ {3, 4, 5, 7}.