Locally decomposable rectangular critical layers

If the degree-d homogeneous component of a multiplication output is a sum of r degree-d Waring terms, every split-k catalecticant has rank at most r. This module supplies uniform and per-occurrence weighted forms of the resulting choose d k Fusion lower bound.

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.AtMost {K : Type} [Field K] (degree termCount : ℕ) (polynomial : MvPolynomial (Fin degree) K) : Prop

The degree-d homogeneous component is a sum of at most termCount degree-d powers.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.zero_atMost {K : Type} [Field K] (degree termCount : ℕ) : AtMost degree termCount 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.add {K : Type} [Field K] (degree leftCount rightCount : ℕ) (left right : MvPolynomial (Fin degree) K) (leftDecomposes : AtMost degree leftCount left) (rightDecomposes : AtMost degree rightCount right) : AtMost degree (leftCount + rightCount) (left + right)

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.succ {K : Type} [Field K] (degree termCount : ℕ) (polynomial : MvPolynomial (Fin degree) K) (decomposes : AtMost degree termCount polynomial) : AtMost degree (termCount + 1) polynomial

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.feature_rank_le {K : Type} [Field K] [CharZero K] (degree split termCount : ℕ) (polynomial : MvPolynomial (Fin degree) K) (decomposes : AtMost degree termCount polynomial) : ((SumOfTerms.Waring.Rectangular.feature K degree split) polynomial).rank ≤ ↑termCount

An r-term critical-layer decomposition has rank at most r at every split.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.multiplicationOccurrences {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) : List (Fin 2 → MvPolynomial (Fin degree) K)

Evaluated multiplication occurrences for the degree-d squarefree problem.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.multiplicationOccurrences_length {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) : (multiplicationOccurrences constant degree circuit).length = circuit.cost Arithmetic.multiplicationCost

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.multiplicationOutput {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) (index : Fin (multiplicationOccurrences constant degree circuit).length) : MvPolynomial (Fin degree) K

Polynomial produced at one evaluated multiplication occurrence.

Equations

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.AtOccurrences {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (circuit : Circuit (Arithmetic.signature C) degree 1) (budget : Fin (multiplicationOccurrences constant degree circuit).length → ℕ) : Prop

A nonuniform decomposition budget for every multiplication occurrence.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.occurrenceIndexedBound_of_atOccurrences {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (budget : Fin (multiplicationOccurrences constant degree circuit).length → ℕ) (restricted : AtOccurrences constant degree circuit budget) : Rank.Occurrence.IndexedBound (certificate constant degree split degreeAtLeastTwo) circuit budget

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.choose_le_sum_occurrenceBudget {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))) (budget : Fin (multiplicationOccurrences constant degree circuit).length → ℕ) (restricted : AtOccurrences constant degree circuit budget) : degree.choose split ≤ ∑ index : Fin (multiplicationOccurrences constant degree circuit).length, budget index

Weighted rectangular Fusion bound over actual multiplication occurrences.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.exists_occurrence_budget_ge_choose_ceilDiv {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (splitLe : split ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (budget : Fin (multiplicationOccurrences constant degree circuit).length → ℕ) (restricted : AtOccurrences constant degree circuit budget) : ∃ (index : Fin (multiplicationOccurrences constant degree circuit).length), degree.choose split ⌈/⌉ circuit.cost Arithmetic.multiplicationCost ≤ budget index

If the chosen layer is nonempty, some gate carries at least the ceiling average rectangular decomposition budget.

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

Uniform decomposition restriction on every multiplication output.

Equations

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

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

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

Uniform locally decomposable critical layers yield the rectangular rank/cost tradeoff.