Biquanimous partitions and signed zero sums

A multiset of naturals is biquanimous if it splits into two parts of equal sum. For n ≥ 3, every partition of n into exactly four parts is biquanimous iff n ∈ {3, 4, 6}. The number of sign vectors ε ∈ {±1}^l with ∑ w_i ε_i = 0, up to ε ~ −ε, is ½ #{A ⊆ [l] | 2 ∑_A w = n}; it is 0 iff the weights are not biquanimous, and 0 for odd n. The same count holds for an abstract singular locus, with the description of that locus as an explicit hypothesis.

Main results

• P3c.thm_clasificacion_comb: the classification of n for four-part partitions.
• P3c.cor_cuenta_signos: 2 · #(sign classes) = #{A | 2 ∑_A w = n}.
• P3c.cor_cuenta_cero_iff, P3c.cor_cuenta_impar: when the count vanishes.
• P3c.cor_cuenta_sing: the count for an abstract singular locus.

References

• C. Marín, Subsets of F_p with two prescribed moments, Part I: the pair (1,3), Zenodo (2026), doi:10.5281/zenodo.22886540.

Part 1: four-part partitions (thm:clasificacion, combinatorial half)

def P3c.Biquanimous (s : Multiset ℕ) : Prop

A multiset of naturals is biquanimous if some sub-multiset carries half the total.

Equations

• P3c.Biquanimous s = ∃ A ≤ s, 2 * A.sum = s.sum

theorem P3c.biquanimous_iff_powerset (s : Multiset ℕ) : Biquanimous s ↔ ∃ A ∈ s.powerset, 2 * A.sum = s.sum

@[instance_reducible]

instance P3c.instDecidableBiquanimous (s : Multiset ℕ) : Decidable (Biquanimous s)

Equations

• P3c.instDecidableBiquanimous s = decidable_of_iff (∃ A ∈ s.powerset, 2 * A.sum = s.sum) ⋯

theorem P3c.sum_le_of_le {A B : Multiset ℕ} (h : A ≤ B) : A.sum ≤ B.sum

theorem P3c.le_sum_of_mem' {a : ℕ} {A : Multiset ℕ} (h : a ∈ A) : a ≤ A.sum

def P3c.lamStar (n : ℕ) (hn : 4 ≤ n) : n.Partition

The witness λ* = (n-3,1,1,1) as a partition of n (needs n ≥ 4).

Equations

• P3c.lamStar n hn = { parts := {n - 3, 1, 1, 1}, parts_pos := ⋯, parts_sum := ⋯ }

theorem P3c.lamStar_card (n : ℕ) (hn : 4 ≤ n) : (lamStar n hn).parts.card = 4

theorem P3c.lamStar_not_biquanimous (n : ℕ) (hn : 5 ≤ n) (h6 : n ≠ 6) : ¬Biquanimous (lamStar n ⋯).parts

λ* = (n-3,1,1,1) is not biquanimous for n ≥ 5, n ≠ 6 (by size for n > 6, by parity for n = 5).

theorem P3c.four_parts_biq (n : ℕ) (hn : n = 4 ∨ n = 6) (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (hs : a + b + c + d = n) : Biquanimous {a, b, c, d}

Four positive parts with total 6 (or 4) always split evenly: finite check.

theorem P3c.thm_clasificacion_comb (n : ℕ) (hn : 3 ≤ n) : (∀ (p : n.Partition), p.parts.card = 4 → Biquanimous p.parts) ↔ n = 3 ∨ n = 4 ∨ n = 6

thm:clasificacion, combinatorial half. For n ≥ 3, every partition of n with exactly four parts is biquanimous iff n ∈ {3, 4, 6} (n = 3 vacuously).

Part 2: the count of cor:cuenta

def P3c.eps {l : ℕ} (A : Finset (Fin l)) : Fin l → ℤˣ

The sign vector of a subset: ε_A i = +1 on A, -1 off A.

Equations

• P3c.eps A i = if i ∈ A then 1 else -1

def P3c.plusSet {l : ℕ} (ε : Fin l → ℤˣ) : Finset (Fin l)

The subset of a sign vector: the +1 coordinates.

Equations

• P3c.plusSet ε = {i : Fin l | ε i = 1}

theorem P3c.neg_one_ne_one_units : -1 ≠ 1

theorem P3c.plusSet_eps {l : ℕ} (A : Finset (Fin l)) : plusSet (eps A) = A

theorem P3c.eps_plusSet {l : ℕ} (ε : Fin l → ℤˣ) : eps (plusSet ε) = ε

theorem P3c.sum_eps {l : ℕ} (w : Fin l → ℤ) (A : Finset (Fin l)) : ∑ i : Fin l, w i * ↑(eps A i) = 2 * ∑ i ∈ A, w i - ∑ i : Fin l, w i

Σ wᵢ ε_A(i) = 2 Σ_A w - Σ w.

def P3c.signZeros {l : ℕ} (w : Fin l → ℤ) : Finset (Fin l → ℤˣ)

Sign vectors with Σ wᵢ εᵢ = 0.

Equations

• P3c.signZeros w = {ε : Fin l → ℤˣ | ∑ i : Fin l, w i * ↑(ε i) = 0}

def P3c.halfSets {l : ℕ} (w : Fin l → ℤ) : Finset (Finset (Fin l))

Equal-sum splittings: subsets A with 2 Σ_A w = n, n = Σ w.

Equations

• P3c.halfSets w = {A : Finset (Fin l) | 2 * ∑ i ∈ A, w i = ∑ i : Fin l, w i}

theorem P3c.card_signZeros {l : ℕ} (w : Fin l → ℤ) : (signZeros w).card = (halfSets w).card

Sign vectors with Σ wε = 0 ↔ subsets with 2 Σ_A w = n (bijection A ↦ ε_A).

theorem P3c.neg_mem_signZeros {l : ℕ} (w : Fin l → ℤ) {ε : Fin l → ℤˣ} (h : ε ∈ signZeros w) : -ε ∈ signZeros w

theorem P3c.ne_neg {l : ℕ} (hl : 0 < l) (ε : Fin l → ℤˣ) : ε ≠ -ε

theorem P3c.two_mul_card_image {l : ℕ} {P : Type u_1} [DecidableEq P] (hl : 0 < l) (w : Fin l → ℤ) (pt : (Fin l → ℤˣ) → P) (hpt : ∀ (ε η : Fin l → ℤˣ), pt η = pt ε ↔ η = ε ∨ η = -ε) : 2 * (Finset.image pt (signZeros w)).card = (signZeros w).card

Abstract fiber count: if pt ε = pt η ↔ η = ±ε, the image of signZeros w under pt has exactly half as many elements.

def P3c.signClass {l : ℕ} (ε : Fin l → ℤˣ) : Sym2 (Fin l → ℤˣ)

The class of ε modulo ε ~ -ε, as the unordered pair {ε, -ε}.

Equations

• P3c.signClass ε = s(ε, -ε)

def P3c.signZerosMod {l : ℕ} (w : Fin l → ℤ) : Finset (Sym2 (Fin l → ℤˣ))

Solutions Σ wε = 0 modulo ±.

Equations

• P3c.signZerosMod w = Finset.image P3c.signClass (P3c.signZeros w)

theorem P3c.signClass_eq_iff {l : ℕ} (ε η : Fin l → ℤˣ) : signClass η = signClass ε ↔ η = ε ∨ η = -ε

theorem P3c.cor_cuenta_signos {l : ℕ} (hl : 0 < l) (w : Fin l → ℤ) : 2 * (signZerosMod w).card = (halfSets w).card

cor:cuenta, counting content. For l ≥ 1 weights w with total n, 2 · #({ε ∈ {±1}^l : Σ wε = 0} / ±) = #{A ⊆ [l] : 2 Σ_A w = n}.

theorem P3c.cor_cuenta_cero_iff {l : ℕ} (hl : 0 < l) (w : Fin l → ℤ) : (signZerosMod w).card = 0 ↔ ¬∃ (A : Finset (Fin l)), 2 * ∑ i ∈ A, w i = ∑ i : Fin l, w i

cor:cuenta, "in particular" (1). The count vanishes iff the weights are not biquanimous (no subset carries half the total).

theorem P3c.cor_cuenta_impar {l : ℕ} (hl : 0 < l) (w : Fin l → ℤ) (hodd : Odd (∑ i : Fin l, w i)) : (signZerosMod w).card = 0

cor:cuenta, "in particular" (2). For odd total n the count is 0.

theorem P3c.cor_cuenta_sing {l : ℕ} {P : Type u_1} [DecidableEq P] (hl : 0 < l) (w : Fin l → ℤ) (pt : (Fin l → ℤˣ) → P) (hpt : ∀ (ε η : Fin l → ℤˣ), pt η = pt ε ↔ η = ε ∨ η = -ε) (Sing : Finset P) (hSing : Sing = Finset.image pt (signZeros w)) : 2 * Sing.card = (halfSets w).card

cor:cuenta with lem:sing as hypothesis. P stands for projective space, pt ε = [ε] with [ε] = [η] ↔ η = ±ε (true for ±1-vectors in characteristic ≠ 2), and Lemma lem:sing (cited, not ours) is the hypothesis hSing : Sing = {[ε] : Σ wε = 0}. Then 2 · #Sing = #{A : 2 Σ_A w = n}.