Quadratic Monomials

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.exponent_degree_le_two {σ : Type u_1} (d : σ →₀ ℕ) (h : (d.sum fun (x : σ) (n : ℕ) => n) ≤ 2) : d = 0 ∨ (∃ (i : σ), d = Finsupp.single i 1) ∨ ∃ (i : σ) (j : σ), d = Finsupp.single i 1 + Finsupp.single j 1

Every monomial of total degree at most two is constant, a variable, or a product of two variables (allowing a repeated variable).