Rectangular catalecticant Fusion for ordinary arithmetic circuits

Lift the degree/split-parametric Waring flattening to ordinary arithmetic circuits. For total degree d ≥ 2, constants and input variables are invisible. A local interaction-rank bound r therefore yields

ceil(choose d k / r) ≤ multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.entryExponent_ne_zero (degree split : ℕ) (positive : 0 < degree) (row column : SumOfTerms.MatrixRank.Layer degree split) : SumOfTerms.Waring.Rectangular.entryExponent degree split row column ≠ 0

Queried degree-d exponents are nonzero when d is positive.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.entryExponent_ne_single (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (row column : SumOfTerms.MatrixRank.Layer degree split) (input : Fin degree) : SumOfTerms.Waring.Rectangular.entryExponent degree split row column ≠ Finsupp.single input 1

Queried degree-d exponents are not degree-one input exponents when d ≥ 2.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.catalecticant_C_eq_zero {K : Type} [Field K] (degree split : ℕ) (positive : 0 < degree) (scalar : K) : (SumOfTerms.Waring.Rectangular.catalecticant K degree split) (MvPolynomial.C scalar) = 0

Constants have zero rectangular catalecticant.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.catalecticant_X_eq_zero {K : Type} [Field K] (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (input : Fin degree) : (SumOfTerms.Waring.Rectangular.catalecticant K degree split) (MvPolynomial.X input) = 0

Input variables have zero rectangular catalecticant in degree at least two.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.feature_C_eq_zero {K : Type} [Field K] (degree split : ℕ) (positive : 0 < degree) (scalar : K) : (SumOfTerms.Waring.Rectangular.feature K degree split) (MvPolynomial.C scalar) = 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.feature_X_eq_zero {K : Type} [Field K] (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (input : Fin degree) : (SumOfTerms.Waring.Rectangular.feature K degree split) (MvPolynomial.X input) = 0

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.problem (K : Type) [Field K] (degree : ℕ) : Problem (MvPolynomial (Fin degree) K)

Ordinary arithmetic problem of constructing the degree-d squarefree monomial.

Equations

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

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.certificate {K C : Type} [Field K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) : Certificate (fun (scalar : C) => MvPolynomial.C (constant scalar)) (problem K degree)

Interaction certificate induced by the degree/split catalecticant.

Equations

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.LocalRankAtMost {K C : Type} [Field K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (interactionRank : ℕ) : Prop

Local rank restriction on the actual multiplication interactions.

Equations

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.MultiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (interactionRank : ℕ) : Prop

Atom-level local rank restriction.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.localRankAtMost_of_multiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (interactionRank : ℕ) (bound : MultiplicationOutputRankAtMost constant degree split degreeAtLeastTwo circuit interactionRank) : LocalRankAtMost constant degree split degreeAtLeastTwo circuit interactionRank

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.choose_ceilDiv_lowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (interactionRank : ℕ) (rankPositive : 0 < interactionRank) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant degree split degreeAtLeastTwo circuit interactionRank) : degree.choose split ⌈/⌉ interactionRank ≤ circuit.cost Arithmetic.multiplicationCost

General rectangular local-rank tradeoff.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.choose_le_cost_mul_rank {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (interactionRank : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant degree split degreeAtLeastTwo circuit interactionRank) : degree.choose split ≤ circuit.cost Arithmetic.multiplicationCost * interactionRank

Undivided rectangular rank/cost tradeoff.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.rankOne_multiplication_lowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant degree split degreeAtLeastTwo circuit 1) : degree.choose split ≤ circuit.cost Arithmetic.multiplicationCost

Rank-one multiplication outputs force the full layer-size lower bound.

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.PowerOrInvisibleAtMultiplications {K C : Type} [Field K] (constant : C → K) (degree split : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) : Prop

Concrete subclass: every multiplication output is invisible or a single degree-d Waring term.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.multiplicationOutputRankAtMost_one_of_powerOrInvisible {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (restricted : PowerOrInvisibleAtMultiplications constant degree split circuit) : MultiplicationOutputRankAtMost constant degree split degreeAtLeastTwo circuit 1

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.powerOrInvisible_multiplication_lowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (restricted : PowerOrInvisibleAtMultiplications constant degree split circuit) : degree.choose split ≤ circuit.cost Arithmetic.multiplicationCost

Power-or-invisible circuits inherit the binomial multiplication lower bound.