Cayley and Segre cubics, Newton's identities, and subsets of 𝔽_p with e₁ = e₃ = 0

• Models: over a field with 6 ≠ 0, the matrix of the four nodes has determinant −8 and turns the cubic F = 2x₀³ + x₁³ + x₂³ + x₃³ − (2x₀ + x₁ + x₂ + x₃)³ into 24 σ₃; the singular points of F = 0 are exactly the four columns. The ten ±1 points of the Segre cubic are nodes, and they are all its singular points.
• Newton: over ZMod p (p > 3), and over any domain with 3 ≠ 0, the first and third power sums of T vanish iff the coefficients e₁ and e₃ of ∏_{t ∈ T} (X − t) do (Mathlib's MvPolynomial.mul_esymm_eq_sum).
• Counts: for #T ≤ 4, e₁ = e₃ = 0 iff T = −T; the number C(n, p) of n-subsets of ZMod p with both moments zero is (p − 1)/2 for n = 3 and (p − 1)(p − 3)/8 for n = 4.

Main results

• P3c.prop_modelos_cayley, P3c.prop_modelos_cayley_nodes, P3c.prop_modelos_segre.
• P3c.lem_newton, P3c.lem_newton_domain.
• P3c.n34_esym_iff_symm, P3c.prop_n34_three, P3c.prop_n34_four.

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: prop:modelos

Part (2): Cayley's nodal cubic

noncomputable def P3c.cayleyF {R : Type u_1} [CommRing R] : MvPolynomial (Fin 4) R

F = 2x₁³+x₂³+x₃³+x₄³-(2x₁+x₂+x₃+x₄)³ (indices 0..3).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def P3c.cayleyStd {R : Type u_1} [CommRing R] : MvPolynomial (Fin 4) R

Equations

• One or more equations did not get rendered due to their size.

def P3c.nodeMat {R : Type u_1} [CommRing R] : Matrix (Fin 4) (Fin 4) R

Matrix whose columns are the four nodes.

Equations

• P3c.nodeMat = !![1, 1, 1, 1; -1, -1, -1, 1; -1, -1, 1, -1; -1, 1, -1, -1]

theorem P3c.cayley_identity {R : Type u_1} [CommRing R] : (MvPolynomial.aeval fun (i : Fin 4) => ∑ j : Fin 4, MvPolynomial.C (nodeMat i j) * MvPolynomial.X j) cayleyF = 24 * cayleyStd

theorem P3c.det_nodeMat {R : Type u_1} [CommRing R] : nodeMat.det = -8

theorem P3c.node_singular {R : Type u_1} [CommRing R] (j : Fin 4) : (MvPolynomial.eval fun (i : Fin 4) => nodeMat i j) cayleyF = 0 ∧ ∀ (i : Fin 4), (MvPolynomial.eval fun (i : Fin 4) => nodeMat i j) ((MvPolynomial.pderiv i) cayleyF) = 0

theorem P3c.eval_pderiv_cayleyF {R : Type u_1} [CommRing R] (x : Fin 4 → R) : (MvPolynomial.eval x) ((MvPolynomial.pderiv 0) cayleyF) = 6 * x 0 ^ 2 - 6 * (2 * x 0 + x 1 + x 2 + x 3) ^ 2 ∧ ∀ (i : Fin 4), i ≠ 0 → (MvPolynomial.eval x) ((MvPolynomial.pderiv i) cayleyF) = 3 * x i ^ 2 - 3 * (2 * x 0 + x 1 + x 2 + x 3) ^ 2

theorem P3c.cayley_sing_classification {k : Type u_2} [Field k] (h6 : 6 ≠ 0) (x : Fin 4 → k) (hx : x ≠ 0) (hsing : ∀ (i : Fin 4), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) cayleyF) = 0) : ∃ (j : Fin 4) (c : k), c ≠ 0 ∧ x = c • fun (i : Fin 4) => nodeMat i j

The singular points of F = 0 in ℙ³ (char k ∤ 6) are exactly the four nodes.

theorem P3c.cayleyF_eq_elim {R : Type u_1} [CommRing R] (x : Fin 4 → R) : 2 * x 0 ^ 3 + x 1 ^ 3 + x 2 ^ 3 + x 3 ^ 3 + (-(2 * x 0 + x 1 + x 2 + x 3)) ^ 3 = (MvPolynomial.eval x) cayleyF

F is the cubic of V_(2,1^4) after eliminating x₅ = -(2x₁+x₂+x₃+x₄).

theorem P3c.prop_modelos_cayley {k : Type u_2} [Field k] (h6 : 6 ≠ 0) : nodeMat.det = -8 ∧ -8 ≠ 0 ∧ 24 ≠ 0 ∧ (MvPolynomial.aeval fun (i : Fin 4) => ∑ j : Fin 4, MvPolynomial.C (nodeMat i j) * MvPolynomial.X j) cayleyF = 24 * cayleyStd

prop:modelos (2): over a field with char k ∤ 6, M is invertible (det M = -8 ≠ 0) and F ∘ M = 24 · (u₀u₁u₂ + u₀u₁u₃ + u₀u₂u₃ + u₁u₂u₃) with 24 ≠ 0: V_(2,1^4) is projectively equivalent over k to Cayley's cubic, with no rescaling.

theorem P3c.prop_modelos_cayley_nodes {k : Type u_2} [Field k] (h6 : 6 ≠ 0) (x : Fin 4 → k) (hx : x ≠ 0) : (∀ (i : Fin 4), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) cayleyF) = 0) ↔ ∃ (j : Fin 4) (c : k), c ≠ 0 ∧ x = c • fun (i : Fin 4) => nodeMat i j

prop:modelos (2), the nodes: over a field with char k ∤ 6, the singular points of F = 0 in ℙ³ are exactly the four columns of M (up to a nonzero scalar).

Part (1): the Segre cubic

noncomputable def P3c.segreL {R : Type u_1} [CommRing R] : MvPolynomial (Fin 6) R

Linear form Σ yᵢ of the Segre cubic.

Equations

• P3c.segreL = ∑ i : Fin 6, MvPolynomial.X i

noncomputable def P3c.segreG {R : Type u_1} [CommRing R] : MvPolynomial (Fin 6) R

Cubic form Σ yᵢ³ of the Segre cubic.

Equations

• P3c.segreG = ∑ i : Fin 6, MvPolynomial.X i ^ 3

def P3c.segreNode {R : Type u_1} [CommRing R] (A : Finset (Fin 6)) : Fin 6 → R

The sign vector with +1 on A and -1 off A.

Equations

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

theorem P3c.eval_pderiv_segreL {R : Type u_1} [CommRing R] (y : Fin 6 → R) (i : Fin 6) : (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreL) = 1

theorem P3c.eval_pderiv_segreG {R : Type u_1} [CommRing R] (y : Fin 6 → R) (i : Fin 6) : (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreG) = 3 * y i ^ 2

theorem P3c.sum_segreNode {R : Type u_1} [CommRing R] (A : Finset (Fin 6)) : ∑ i : Fin 6, segreNode A i = 2 * ↑A.card - 6

theorem P3c.segre_node_singular {R : Type u_1} [CommRing R] (A : Finset (Fin 6)) (hA : A.card = 3) : (MvPolynomial.eval (segreNode A)) segreL = 0 ∧ (MvPolynomial.eval (segreNode A)) segreG = 0 ∧ ∀ (i : Fin 6), (MvPolynomial.eval (segreNode A)) ((MvPolynomial.pderiv i) segreG) = 3 * (MvPolynomial.eval (segreNode A)) ((MvPolynomial.pderiv i) segreL)

theorem P3c.segre_sing_classification {k : Type u_2} [Field k] (h6 : 6 ≠ 0) (y : Fin 6 → k) (hy : y ≠ 0) (hL : (MvPolynomial.eval y) segreL = 0) (hrank : ∃ (a : k) (b : k), (a ≠ 0 ∨ b ≠ 0) ∧ ∀ (i : Fin 6), a * (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreL) + b * (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreG) = 0) : ∃ (s : k), s ≠ 0 ∧ ∃ (A : Finset (Fin 6)), A.card = 3 ∧ y = s • segreNode A

theorem P3c.segreNode_compl {R : Type u_1} [CommRing R] (A : Finset (Fin 6)) : segreNode Aᶜ = -segreNode A

The nodes come in antipodal pairs A ↔ Aᶜ (same projective point).

theorem P3c.card_three_subsets : (Finset.powersetCard 3 Finset.univ).card = 20

#{A ⊆ [6] : #A = 3} = 20, i.e. ten projective nodes after A ~ Aᶜ.

theorem P3c.prop_modelos_segre {k : Type u_2} [Field k] (h6 : 6 ≠ 0) (y : Fin 6 → k) (hy : y ≠ 0) : ((MvPolynomial.eval y) segreL = 0 ∧ (MvPolynomial.eval y) segreG = 0 ∧ ∃ (a : k) (b : k), (a ≠ 0 ∨ b ≠ 0) ∧ ∀ (i : Fin 6), a * (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreL) + b * (MvPolynomial.eval y) ((MvPolynomial.pderiv i) segreG) = 0) ↔ ∃ (s : k), s ≠ 0 ∧ ∃ (A : Finset (Fin 6)), A.card = 3 ∧ y = s • segreNode A

prop:modelos (1): over a field with char k ∤ 6, the singular points of {Σyᵢ = Σyᵢ³ = 0} ⊂ ℙ⁵ (points where the 2×6 Jacobian has rank < 2) are exactly the multiples of the sign vectors with three +1 and three -1.

Part 2: lem:newton and prop:n34

def P3c.moment {R : Type u_1} [CommRing R] (j : ℕ) (T : Finset R) : R

Power sum M_j(T) = Σ_{t∈T} t^j.

Equations

• P3c.moment j T = ∑ t ∈ T, t ^ j

def P3c.esym {R : Type u_1} [CommRing R] (j : ℕ) (T : Finset R) : R

Elementary symmetric function e_j(T).

Equations

• P3c.esym j T = T.val.esymm j

theorem P3c.newton_three {R : Type u_1} [CommRing R] (T : Finset R) : 3 * esym 3 T = moment 3 T - esym 1 T * moment 2 T + esym 2 T * moment 1 T

theorem P3c.esym_one {R : Type u_1} [CommRing R] (T : Finset R) : esym 1 T = moment 1 T

theorem P3c.moments_iff_esym {R : Type u_1} [CommRing R] [IsDomain R] (h3 : 3 ≠ 0) (T : Finset R) : moment 1 T = 0 ∧ moment 3 T = 0 ↔ esym 1 T = 0 ∧ esym 3 T = 0

M₁ = M₃ = 0 ⇔ e₁ = e₃ = 0 when 3 ≠ 0 in a domain.

theorem P3c.prod_sub_eq_sum_esym {R : Type u_1} [CommRing R] (T : Finset R) (x : R) : ∏ t ∈ T, (x - t) = ∑ j ∈ Finset.range (T.card + 1), (-1) ^ j * esym j T * x ^ (T.card - j)

Value of ∏_{t∈T} (x - t) in terms of the e_j.

noncomputable def P3c.coeffZ {R : Type u_1} [CommRing R] (P : Polynomial R) (m : ℤ) : R

Coefficient of X^m for an integer exponent m (zero when m < 0), so that "the coefficient of X^{n-3}" is meaningful for every n.

Equations

• P3c.coeffZ P m = if m < 0 then 0 else P.coeff m.toNat

theorem P3c.coeffZ_prod {R : Type u_1} [CommRing R] (T : Finset R) (j : ℕ) : coeffZ (∏ t ∈ T, (Polynomial.X - Polynomial.C t)) (↑T.card - ↑j) = (-1) ^ j * esym j T

theorem P3c.lem_newton_domain {R : Type u_1} [CommRing R] [IsDomain R] (h3 : 3 ≠ 0) (T : Finset R) : moment 1 T = 0 ∧ moment 3 T = 0 ↔ coeffZ (∏ t ∈ T, (Polynomial.X - Polynomial.C t)) (↑T.card - 1) = 0 ∧ coeffZ (∏ t ∈ T, (Polynomial.X - Polynomial.C t)) (↑T.card - 3) = 0

lem:newton, over any domain in which 3 ≠ 0.

def P3c.SymmNeg {R : Type u_1} [Ring R] (T : Finset R) : Prop

T = -T (as a property: T is stable under negation).

Equations

• P3c.SymmNeg T = ∀ x ∈ T, -x ∈ T

@[instance_reducible]

instance P3c.instDecidableSymmNegOfDecidableEq {R : Type u_1} [Ring R] [DecidableEq R] (T : Finset R) : Decidable (SymmNeg T)

Equations

• P3c.instDecidableSymmNegOfDecidableEq T = id inferInstance

theorem P3c.two_ne_zero_zmod {p : ℕ} (hp3 : 3 < p) : 2 ≠ 0

theorem P3c.three_ne_zero_zmod {p : ℕ} (hp3 : 3 < p) : 3 ≠ 0

theorem P3c.moment_odd_eq_zero {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) {T : Finset (ZMod p)} (hT : SymmNeg T) {j : ℕ} (hj : Odd j) : moment j T = 0

A set stable under negation has vanishing odd power sums (p odd).

theorem P3c.n34_esym_iff_symm {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) (T : Finset (ZMod p)) (hn : T.card ≤ 4) : esym 1 T = 0 ∧ esym 3 T = 0 ↔ SymmNeg T

prop:n34, first claim: for p > 3 and #T ≤ 4, e₁ = e₃ = 0 ⇔ T = -T.

theorem P3c.lem_newton {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) (T : Finset (ZMod p)) : moment 1 T = 0 ∧ moment 3 T = 0 ↔ coeffZ (∏ t ∈ T, (Polynomial.X - Polynomial.C t)) (↑T.card - 1) = 0 ∧ coeffZ (∏ t ∈ T, (Polynomial.X - Polynomial.C t)) (↑T.card - 3) = 0

lem:newton (p > 3): M₁(T) = M₃(T) = 0 iff the coefficients of X^{n-1} and X^{n-3} in ∏_{t∈T} (X - t) vanish, n = #T.

def P3c.C13 (n p : ℕ) [NeZero p] : ℕ

C(n,p): number of n-subsets T ⊆ 𝔽_p with M₁(T) = M₃(T) = 0.

Equations

• P3c.C13 n p = {T ∈ Finset.powersetCard n Finset.univ | P3c.moment 1 T = 0 ∧ P3c.moment 3 T = 0}.card

def P3c.halfReps (p : ℕ) [NeZero p] : Finset (ZMod p)

Representatives of the antipodal pairs: {x : 1 ≤ val x ≤ p/2}.

Equations

• P3c.halfReps p = {x : ZMod p | 1 ≤ x.val ∧ x.val ≤ p / 2}

theorem P3c.card_halfReps (p : ℕ) [NeZero p] : (halfReps p).card = p / 2

theorem P3c.zero_notMem_halfReps (p : ℕ) [NeZero p] : 0 ∉ halfReps p

theorem P3c.halfReps_xor {p : ℕ} [Fact (Nat.Prime p)] (hodd : p % 2 = 1) {x : ZMod p} (hx : x ≠ 0) : x ∈ halfReps p ↔ -x ∉ halfReps p

For x ≠ 0 and p odd, exactly one of x, -x is a representative.

theorem P3c.card_symm {p : ℕ} [Fact (Nat.Prime p)] (hodd : p % 2 = 1) {T : Finset (ZMod p)} (hT : SymmNeg T) : T.card = 2 * {x ∈ T | x ∈ halfReps p}.card + if 0 ∈ T then 1 else 0

Cardinality of a negation-stable set: #T = 2·#(T ∩ H) + [0 ∈ T].

def P3c.symmOf {p : ℕ} (b : Bool) (S : Finset (ZMod p)) : Finset (ZMod p)

The negation-stable set generated by S ⊆ H, with 0 added iff b.

Equations

• P3c.symmOf b S = (if b = true then {0} else ∅) ∪ (S ∪ Finset.image (fun (x : ZMod p) => -x) S)

theorem P3c.symmOf_symm {p : ℕ} (b : Bool) (S : Finset (ZMod p)) : SymmNeg (symmOf b S)

theorem P3c.symmOf_filter {p : ℕ} [Fact (Nat.Prime p)] (hodd : p % 2 = 1) (b : Bool) {S : Finset (ZMod p)} (hS : S ⊆ halfReps p) : {x ∈ symmOf b S | x ∈ halfReps p} = S

theorem P3c.zero_mem_symmOf_iff {p : ℕ} [Fact (Nat.Prime p)] (b : Bool) {S : Finset (ZMod p)} (hS : S ⊆ halfReps p) : 0 ∈ symmOf b S ↔ b = true

theorem P3c.symm_ext {p : ℕ} [Fact (Nat.Prime p)] (hodd : p % 2 = 1) {T T' : Finset (ZMod p)} (hT : SymmNeg T) (hT' : SymmNeg T') (h0 : 0 ∈ T ↔ 0 ∈ T') (hf : {x ∈ T | x ∈ halfReps p} = {x ∈ T' | x ∈ halfReps p}) : T = T'

Two negation-stable sets with the same representatives and the same 0-status coincide.

theorem P3c.card_symm_sets {p : ℕ} [Fact (Nat.Prime p)] (hodd : p % 2 = 1) (b : Bool) (k : ℕ) : {T ∈ Finset.powersetCard (2 * k + if b = true then 1 else 0) Finset.univ | SymmNeg T ∧ (0 ∈ T ↔ b = true)}.card = (p / 2).choose k

Counting negation-stable n-sets with prescribed 0-status: they are in bijection with k-subsets of H, n = 2k + [b].

theorem P3c.odd_of_prime {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) : p % 2 = 1

theorem P3c.moments_iff_symm {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) (T : Finset (ZMod p)) (hn : T.card ≤ 4) : moment 1 T = 0 ∧ moment 3 T = 0 ↔ SymmNeg T

For #T = n ≤ 4: M₁ = M₃ = 0 ⇔ T = -T (lem:newton + first claim of prop:n34).

theorem P3c.C_eq_card_symm {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) (b : Bool) (k : ℕ) (hk : (2 * k + if b = true then 1 else 0) ≤ 4) (hpar : ∀ (T : Finset (ZMod p)), (T.card = 2 * k + if b = true then 1 else 0) → SymmNeg T → (0 ∈ T ↔ b = true)) : C13 (2 * k + if b = true then 1 else 0) p = (p / 2).choose k

theorem P3c.prop_n34_three {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) : 2 * C13 3 p = p - 1 ∧ C13 3 p = (p - 1) / 2

prop:n34, n = 3: C(3,p) = (p-1)/2 (and 2·C(3,p) = p-1).

theorem P3c.prop_n34_four {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 < p) : 8 * C13 4 p = (p - 1) * (p - 3) ∧ C13 4 p = (p - 1) * (p - 3) / 8

prop:n34, n = 4: C(4,p) = (p-1)(p-3)/8 (and 8·C(4,p) = (p-1)(p-3)).