Local catalecticant-rank bounds for arithmetic circuits

Use the normalized middle catalecticant from the Waring lower bound as a linear-map feature of an ordinary arithmetic circuit. Constants and input variables have zero feature. With the generic linear interaction certificate, the interaction created by a multiplication is the catalecticant of that gate's product output.

Hence an explicit circuit-local restriction—every multiplication output has middle-catalecticant rank at most r—forces the squarefree target to use at least centralBinom n / r multiplication gates. For r = 1 this is an exponential single-output lower bound for the restricted ordinary arithmetic circuit model.

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

Every queried middle-catalecticant exponent is nonzero for a positive half-degree.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.entryExponent_ne_single (n : ℕ) (row column : SumOfTerms.MatrixRank.Layer (2 * n) n) (input : Fin (2 * n)) : SumOfTerms.Waring.entryExponent n row column ≠ Finsupp.single input 1

Every queried middle-catalecticant exponent has degree bigger than one for a positive half-degree.

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

Constants have zero normalized middle catalecticant.

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

Input variables have zero normalized middle catalecticant.

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

Constants have zero catalecticant linear-map feature.

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

Input variables have zero catalecticant linear-map feature.

@[reducible, inline]

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

Ordinary arithmetic problem of constructing the squarefree product of all 2n input variables.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.problem K n = { inputCount := 2 * n, inputs := MvPolynomial.X, target := Algebraic.Fusion.SumOfTerms.Waring.target K n }

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.certificate {K C : Type} [Field K] (constant : C → K) (n : ℕ) (positive : 0 < n) : Certificate (fun (scalar : C) => MvPolynomial.C (constant scalar)) (problem K n)

Linear interaction certificate induced by the normalized middle catalecticant. A multiplication interaction is the feature of its product.

Equations

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.LocalRankAtMost {K C : Type} [Field K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (interactionRank : ℕ) : Prop

Circuit-local restriction saying that every multiplication output has normalized middle-catalecticant rank at most interactionRank.

Equations

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.MultiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (interactionRank : ℕ) : Prop

Atom-level version of the local restriction: directly bound the catalecticant rank of each multiplication output.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.localRankAtMost_of_multiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (interactionRank : ℕ) (bound : MultiplicationOutputRankAtMost constant n positive circuit interactionRank) : LocalRankAtMost constant n positive circuit interactionRank

Atom-level multiplication-output bounds imply the filtered local-rank condition.

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

A concrete ordinary-circuit subclass: every multiplication output is either invisible to the middle catalecticant or is one scalar multiple of a 2n-th power of a linear form.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.multiplicationOutputRankAtMost_one_of_powerOrInvisible {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (restricted : PowerOrInvisibleAtMultiplications constant n circuit) : MultiplicationOutputRankAtMost constant n positive circuit 1

Power-or-invisible multiplication outputs have local catalecticant rank at most one.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.localRankAtMost_one_of_powerOrInvisible {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (restricted : PowerOrInvisibleAtMultiplications constant n circuit) : LocalRankAtMost constant n positive circuit 1

Power-or-invisible multiplication outputs satisfy the filtered rank-one condition used by the lower bound.

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

General local-rank tradeoff for the squarefree target.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.centralBinom_le_cost_mul_rank {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (interactionRank : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant n positive circuit interactionRank) : n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost * interactionRank

Undivided exponential tradeoff: target rank is at most multiplication cost times the actual local interaction-rank bound.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.rankOne_multiplication_lowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant n positive circuit 1) : n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

Rank-one multiplication outputs force a central-binomial multiplication lower bound.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.powerOrInvisible_multiplication_lowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (restricted : PowerOrInvisibleAtMultiplications constant n circuit) : n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

Every power-or-invisible ordinary arithmetic circuit for the squarefree target needs central-binomial multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.four_pow_lt_mul_multiplicationCost {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant n ⋯ circuit 1) : 4 ^ n < n * circuit.cost Arithmetic.multiplicationCost

Explicit exponential single-output multiplication lower bound for locally rank-one arithmetic circuits.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.four_pow_lt_mul_size {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (localBound : LocalRankAtMost constant n ⋯ circuit 1) : 4 ^ n < n * circuit.size

Explicit exponential raw-size lower bound for locally rank-one arithmetic circuits.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.powerOrInvisible_four_pow_lt_mul_size {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (restricted : PowerOrInvisibleAtMultiplications constant n circuit) : 4 ^ n < n * circuit.size

Explicit exponential single-output size lower bound for the concrete power-or-invisible ordinary arithmetic circuit subclass.