Degree-visible catalecticant fusion

The middle catalecticant at half-degree n only reads coefficients of total degree 2 * n. Consequently every lower-degree polynomial is invisible to the feature. This supplies a structural way to discharge the invisible branch of PowerOrInvisibleAtMultiplications.

The resulting ordinary-circuit subclass permits arbitrary lower-degree multiplication outputs and charges only critical-degree outputs, which must be scalar multiples of 2n-th powers of linear forms.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.coeff_entryExponent_eq_zero_of_totalDegree_lt {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (small : polynomial.totalDegree < 2 * n) (row column : SumOfTerms.MatrixRank.Layer (2 * n) n) : polynomial.coeff (SumOfTerms.Waring.entryExponent n row column) = 0

Every coefficient read by the middle catalecticant vanishes below the critical total degree.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.catalecticant_eq_zero_of_totalDegree_lt {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (small : polynomial.totalDegree < 2 * n) : (SumOfTerms.Waring.catalecticant K n) polynomial = 0

A polynomial below total degree 2n has zero middle catalecticant.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.feature_eq_zero_of_totalDegree_lt {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (small : polynomial.totalDegree < 2 * n) : (SumOfTerms.Waring.feature K n) polynomial = 0

A polynomial below total degree 2n is invisible to the catalecticant linear-map feature.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.entryExponent_degree (n : ℕ) (row column : SumOfTerms.MatrixRank.Layer (2 * n) n) : Finsupp.degree (SumOfTerms.Waring.entryExponent n row column) = 2 * n

Every exponent queried by the middle catalecticant has Finsupp degree exactly 2n.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.catalecticant_homogeneousComponent {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) : (SumOfTerms.Waring.catalecticant K n) ((MvPolynomial.homogeneousComponent (2 * n)) polynomial) = (SumOfTerms.Waring.catalecticant K n) polynomial

The middle catalecticant only sees the critical homogeneous component.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.feature_homogeneousComponent {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) : (SumOfTerms.Waring.feature K n) ((MvPolynomial.homogeneousComponent (2 * n)) polynomial) = (SumOfTerms.Waring.feature K n) polynomial

The catalecticant linear-map feature factors through the critical homogeneous component.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.feature_eq_zero_of_homogeneousComponent_eq_zero {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (invisible : (MvPolynomial.homogeneousComponent (2 * n)) polynomial = 0) : (SumOfTerms.Waring.feature K n) polynomial = 0

Vanishing of the critical homogeneous component is the exact structural invisibility condition needed by the feature.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.linearForm_isHomogeneous {K : Type} {n : ℕ} [CommSemiring K] (term : SumOfTerms.Waring.Term K n) : (SumOfTerms.Waring.linearForm term).IsHomogeneous 1

A Waring linear form is homogeneous of degree one.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.termValue_isHomogeneous {K : Type} {n : ℕ} [CommSemiring K] (term : SumOfTerms.Waring.Term K n) : (SumOfTerms.Waring.termValue term).IsHomogeneous (2 * n)

A charged Waring term is homogeneous of the critical degree.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.homogeneousComponent_termValue {K : Type} {n : ℕ} [CommSemiring K] (term : SumOfTerms.Waring.Term K n) : (MvPolynomial.homogeneousComponent (2 * n)) (SumOfTerms.Waring.termValue term) = SumOfTerms.Waring.termValue term

Projecting a Waring term to the critical homogeneous component leaves it unchanged.

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

Layer-exact ordinary-circuit restriction: the critical homogeneous component of each multiplication output is either zero or one Waring term. All off-layer terms are unrestricted.

Equations

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

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

Structural ordinary-circuit restriction: each multiplication output is either below the critical degree or 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.Degree.criticalLayerOrPower_of_lowDegreeOrPower {K C : Type} [Field K] (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (restricted : LowDegreeOrPowerAtMultiplications constant n circuit) : CriticalLayerOrPowerAtMultiplications constant n circuit

The total-degree restriction is a special case of the layer-exact restriction.

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

Layer-exact critical components give atom-level catalecticant rank at most one.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.criticalLayer_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 : CriticalLayerOrPowerAtMultiplications constant n circuit) : n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

Every layer-exact critical-component circuit for the squarefree target needs central-binomial multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.criticalLayer_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 : CriticalLayerOrPowerAtMultiplications constant n circuit) : 4 ^ n < n * circuit.size

Explicit exponential size lower bound for the layer-exact critical-component circuit class.

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

The structural degree-or-power restriction implies the semantic power-or-invisible restriction.

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

Degree-or-power multiplication outputs have catalecticant rank at most one.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.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 : LowDegreeOrPowerAtMultiplications constant n circuit) : n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Degree.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 : LowDegreeOrPowerAtMultiplications constant n circuit) : 4 ^ n < n * circuit.size

Explicit exponential size lower bound for the structural degree-or-power ordinary arithmetic circuit subclass.