Rectangular-degree catalecticants for Waring sums

Parameterize the squarefree Waring flattening by an arbitrary total degree d and layer split k. Both matrix axes are indexed by k-subsets; the column is complemented before forming the queried exponent, so its contribution has degree d-k. The squarefree target becomes a scalar identity matrix of dimension choose d k, while every d-th power of a linear form remains rank one.

structure Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Term (K : Type) (degree : ℕ) : Type

One scalar multiple of a degree-d power of a linear form.

• scale : K

  Scalar multiplying the power.

• coefficients : Fin degree → K

  Coefficients of the linear form in degree variables.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.linearForm {K : Type} [CommSemiring K] {degree : ℕ} (term : Term K degree) : MvPolynomial (Fin degree) K

Linear form represented by a rectangular-degree Waring term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.linearForm term = ∑ index : Fin degree, term.coefficients index • MvPolynomial.X index

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.termValue {K : Type} [CommSemiring K] {degree : ℕ} (term : Term K degree) : MvPolynomial (Fin degree) K

Polynomial value of a charged degree-d Waring term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.termValue term = MvPolynomial.C term.scale * Algebraic.Fusion.SumOfTerms.Waring.Rectangular.linearForm term ^ degree

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.complementSet {degree split : ℕ} (set : MatrixRank.Layer degree split) : Finset (Fin degree)

Complement of a layer index, viewed as a set rather than forced back into the same layer.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.complementSet set = (↑set)ᶜ

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.complementSet_def {degree split : ℕ} (set : MatrixRank.Layer degree split) : complementSet set = (↑set)ᶜ

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.entryExponent (degree split : ℕ) (row column : MatrixRank.Layer degree split) : Fin degree →₀ ℕ

Exponent queried by the split-k catalecticant entry.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.entryExponent_eq_targetExponent_iff (degree split : ℕ) (row column : MatrixRank.Layer degree split) : entryExponent degree split row column = exponent Finset.univ ↔ row = column

A row set plus a complemented column set is the all-ones exponent exactly on the matrix diagonal.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.entryExponent_sum (degree split : ℕ) (row column : MatrixRank.Layer degree split) : ((entryExponent degree split row column).sum fun (x : Fin degree) (multiplicity : ℕ) => multiplicity) = degree

Every queried entry exponent has total degree degree.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.catalecticant (K : Type) [Field K] (degree split : ℕ) : MvPolynomial (Fin degree) K →ₗ[K] Matrix (MatrixRank.Layer degree split) (MatrixRank.Layer degree split) K

Normalized degree-d, split-k catalecticant.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.catalecticant_apply {K : Type} [Field K] (degree split : ℕ) (polynomial : MvPolynomial (Fin degree) K) (row column : MatrixRank.Layer degree split) : (catalecticant K degree split) polynomial row column = polynomial.coeff (entryExponent degree split row column) / ↑(entryExponent degree split row column).multinomial

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.entryExponent_multinomial_ne_zero {K : Type} [Field K] [CharZero K] (degree split : ℕ) (row column : MatrixRank.Layer degree split) : ↑(entryExponent degree split row column).multinomial ≠ 0

Every normalization denominator is nonzero in characteristic zero.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.entryExponent_prod {degree split : ℕ} {K : Type} [CommMonoid K] (coefficients : Fin degree → K) (row column : MatrixRank.Layer degree split) : ((entryExponent degree split row column).prod fun (index : Fin degree) (multiplicity : ℕ) => coefficients index ^ multiplicity) = (∏ index ∈ ↑row, coefficients index) * ∏ index ∈ complementSet column, coefficients index

Coefficient products factor across the row and complemented column.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.coeff_linearForm_pow_entryExponent {degree split : ℕ} {K : Type} [CommSemiring K] (term : Term K degree) (row column : MatrixRank.Layer degree split) : (linearForm term ^ degree).coeff (entryExponent degree split row column) = ↑(entryExponent degree split row column).multinomial * ((∏ index ∈ ↑row, term.coefficients index) * ∏ index ∈ complementSet column, term.coefficients index)

Coefficient formula for a linear-form power at a queried exponent.

def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.leftVector {degree split : ℕ} {K : Type} [CommMonoid K] (term : Term K degree) : MatrixRank.Layer degree split → K

Row vector in the rank-one rectangular catalecticant of a power term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.leftVector term row = term.scale * ∏ index ∈ ↑row, term.coefficients index

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.rightVector {degree split : ℕ} {K : Type} [CommMonoid K] (term : Term K degree) : MatrixRank.Layer degree split → K

Complement-reindexed column vector.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.rightVector term column = ∏ index ∈ Algebraic.Fusion.SumOfTerms.Waring.Rectangular.complementSet column, term.coefficients index

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.catalecticant_termValue {degree : ℕ} {K : Type} [Field K] [CharZero K] (term : Term K degree) (split : ℕ) : (catalecticant K degree split) (termValue term) = Matrix.vecMulVec (leftVector term) (rightVector term)

A normalized rectangular catalecticant of a power term is an outer product.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetExponent (degree : ℕ) : Fin degree →₀ ℕ

All-ones exponent of the degree-d squarefree target.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetExponent degree = Algebraic.Fusion.SumOfTerms.Waring.exponent Finset.univ

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.target (K : Type) [CommSemiring K] (degree : ℕ) : MvPolynomial (Fin degree) K

Product of all degree variables.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.target K degree = (MvPolynomial.monomial (Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetExponent degree)) 1

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.target_eq_prod_X (K : Type) [CommSemiring K] (degree : ℕ) : target K degree = ∏ index : Fin degree, MvPolynomial.X index

The generalized target is literally the product of all variables.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetScalar (K : Type) [Field K] (degree : ℕ) : K

The inverse, in K, of the multinomial coefficient of the target exponent; it appears on the target catalecticant diagonal. It is nonzero in characteristic zero (targetScalar_ne_zero).

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetScalar K degree = (↑(Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetExponent degree).multinomial)⁻¹

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetScalar_ne_zero {K : Type} [Field K] [CharZero K] (degree : ℕ) : targetScalar K degree ≠ 0

The target normalizing scalar is nonzero in characteristic zero.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.catalecticant_target {K : Type} [Field K] (degree split : ℕ) : (catalecticant K degree split) (target K degree) = targetScalar K degree • 1

The squarefree target has a scalar identity at every layer split.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.feature (K : Type) [Field K] (degree split : ℕ) : MvPolynomial (Fin degree) K →ₗ[K] (MatrixRank.Layer degree split → K) →ₗ[K] MatrixRank.Layer degree split → K

Rectangular catalecticant followed by matrix-to-linear-map conversion.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Rectangular.feature K degree split = ↑Matrix.toLin' ∘ₗ Algebraic.Fusion.SumOfTerms.Waring.Rectangular.catalecticant K degree split

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.feature_target {K : Type} [Field K] (degree split : ℕ) : (feature K degree split) (target K degree) = targetScalar K degree • LinearMap.id

The target feature is targetScalar K degree times the identity map, over any field. The scalar is nonzero in characteristic zero (targetScalar_ne_zero).

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.target_rank_ge {K : Type} [Field K] [CharZero K] (degree split : ℕ) : ↑(degree.choose split) ≤ ((feature K degree split) (target K degree)).rank

Target rank is the full choose degree split layer dimension.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.targetRank_le_middle (degree split : ℕ) : degree.choose split ≤ degree.choose (degree / 2)

Among the rectangular splits, the middle layer maximizes the raw target rank. Off-center splits are useful only when they improve the corresponding local interaction-rank bound.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.term_rank_le_one {degree : ℕ} {K : Type} [Field K] [CharZero K] (term : Term K degree) (split : ℕ) : ((feature K degree split) (termValue term)).rank ≤ 1

Every charged degree-d power has rectangular feature rank at most one.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.SumOfTerms.Waring.Rectangular.problem (K : Type) [CommSemiring K] (degree : ℕ) : Problem (MvPolynomial (Fin degree) K)

Construct the degree-d squarefree monomial from degree-d powers.

Equations

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

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.certificate (K : Type) [Field K] [CharZero K] (degree split : ℕ) : RankCertificate termValue (problem K degree)

Full rectangular-rank certificate for the squarefree target.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.certificate_targetRank (K : Type) [Field K] [CharZero K] (degree split : ℕ) : (certificate K degree split).targetRank = degree.choose split

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.certificate_termRank (K : Type) [Field K] [CharZero K] (degree split : ℕ) : (certificate K degree split).termRank = 1

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.choose_lowerBound {K : Type} [Field K] [CharZero K] (degree split : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : degree.choose split ≤ circuit.cost SumOfTerms.termCost

Split-k rectangular catalecticants force choose d k Waring terms.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.centralBinom_lowerBound {K : Type} [Field K] [CharZero K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K (2 * n))) 0 1) (constructs : (problem K (2 * n)).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ circuit.cost SumOfTerms.termCost

The middle split recovers the central-binomial lower bound at even degree.