Locally decomposable critical layers

Generalize the rank-one critical-layer restriction to multiplication outputs whose degree-2n homogeneous component is a sum of r Waring terms. Rank subadditivity turns such a semantic decomposition into a local catalecticant rank bound r, yielding the tradeoff

centralBinom n / r ≤ multiplication cost.

The Fin r presentation allows zero-scaled terms to pad shorter decompositions, so it represents "at most r" terms over a field.

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

The critical homogeneous layer is a sum of at most termCount Waring terms, with zero-scaled terms available as padding.

Equations

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

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

The zero polynomial has an r-term decomposition for every r.

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

Decomposition budgets add under polynomial addition.

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

A decomposition can be padded by one zero-scaled Waring term.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.atMost_one_of_term {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (term : SumOfTerms.Waring.Term K n) (critical : (MvPolynomial.homogeneousComponent (2 * n)) polynomial = SumOfTerms.Waring.termValue term) : AtMost n 1 polynomial

One critical-layer Waring term gives a one-term decomposition.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.atMost_one_of_criticalLayerOrPower {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (restricted : (MvPolynomial.homogeneousComponent (2 * n)) polynomial = 0 ∨ ∃ (term : SumOfTerms.Waring.Term K n), (MvPolynomial.homogeneousComponent (2 * n)) polynomial = SumOfTerms.Waring.termValue term) : AtMost n 1 polynomial

The earlier zero-or-one-power restriction is a one-term decomposition.

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

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

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.FeatureAtMost {K : Type} [Field K] (n termCount : ℕ) (interaction : (SumOfTerms.MatrixRank.Layer (2 * n) n → K) →ₗ[K] SumOfTerms.MatrixRank.Layer (2 * n) n → K) : Prop

A linear-map interaction is explicitly a sum of termCount catalecticant features of Waring terms.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.featureAtMost_of_atMost {K : Type} [Field K] (n termCount : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (decomposes : AtMost n termCount polynomial) : FeatureAtMost n termCount ((SumOfTerms.Waring.feature K n) polynomial)

A polynomial critical-layer decomposition induces the corresponding feature decomposition.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.featureDecomposition_rank_le {K : Type} [Field K] [CharZero K] (n termCount : ℕ) (interaction : (SumOfTerms.MatrixRank.Layer (2 * n) n → K) →ₗ[K] SumOfTerms.MatrixRank.Layer (2 * n) n → K) (decomposes : FeatureAtMost n termCount interaction) : interaction.rank ≤ ↑termCount

A feature decomposition by r Waring terms has rank at most r.

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

Evaluated multiplication-gate occurrences for the squarefree catalecticant problem.

Equations

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

@[simp]

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

The specialized occurrence list has exactly the circuit's multiplication cost.

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

A possibly different Waring-decomposition budget for every multiplication gate occurrence. Equal semantic products at distinct gates retain distinct indices and may receive different budgets.

Equations

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

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

A semantic Waring budget depending on multiplication arguments. Its list sum still charges repeated occurrences separately.

Equations

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

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

Occurrence-local Waring decompositions induce the generic occurrence-indexed rank budget.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.argumentBound_of_argumentAtMost {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (budget : (Fin 2 → MvPolynomial (Fin (2 * n)) K) → ℕ) (restricted : ArgumentAtMost constant n circuit budget) : Rank.Occurrence.ArgumentBound (certificate constant n positive) circuit budget

Semantic argument-local Waring decompositions induce the generic argument-dependent rank budget.

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

Weighted catalecticant Fusion bound indexed directly by multiplication gate occurrences.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.exists_occurrence_budget_ge_centralBinom_ceilDiv {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))) (budget : Fin (multiplicationOccurrences constant n circuit).length → ℕ) (restricted : AtOccurrences constant n circuit budget) : ∃ (index : Fin (multiplicationOccurrences constant n circuit).length), n.centralBinom ⌈/⌉ circuit.cost Arithmetic.multiplicationCost ≤ budget index

Concentration form of the weighted bound: some actual multiplication gate needs at least the ceiling-average local Waring budget.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.centralBinom_le_sum_argumentBudget {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))) (budget : (Fin 2 → MvPolynomial (Fin (2 * n)) K) → ℕ) (restricted : ArgumentAtMost constant n circuit budget) : n.centralBinom ≤ (List.map budget (multiplicationOccurrences constant n circuit)).sum

Argument-dependent weighted catalecticant bound, expressed as a list sum over the evaluated multiplication gates.

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.IndexedAtMost {K C : Type} [Field K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (budget : Fin (interactions (certificate constant n positive) (circuitAtoms circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) MvPolynomial.X)).length → ℕ) : Prop

Nonuniform Waring-feature decomposition budget for the actual retained interaction occurrences of one evaluated circuit.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.indexedBound_of_indexedAtMost {K C : Type} [Field K] [CharZero K] (constant : C → K) (n : ℕ) (positive : 0 < n) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (budget : Fin (interactions (certificate constant n positive) (circuitAtoms circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) MvPolynomial.X)).length → ℕ) (decomposes : IndexedAtMost constant n positive circuit budget) : Rank.Local.IndexedBound (certificate constant n positive) circuit budget

Indexed Waring-feature decompositions imply the generic indexed rank budget.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.centralBinom_le_sum_indexedBudget {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))) (budget : Fin (interactions (certificate constant n positive) (circuitAtoms circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) MvPolynomial.X)).length → ℕ) (decomposes : IndexedAtMost constant n positive circuit budget) : n.centralBinom ≤ ∑ index : Fin (interactions (certificate constant n positive) (circuitAtoms circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) MvPolynomial.X)).length, budget index

Weighted nonuniform Fusion lower bound: the total local Waring decomposition budget across multiplication occurrences is at least the central binomial coefficient.

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

Circuit-local decomposition predicate for every multiplication output.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.atOccurrences_const_of_atMultiplications {K C : Type} [Field K] (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (termCount : ℕ) (restricted : AtMultiplications constant n circuit termCount) : AtOccurrences constant n circuit fun (x : Fin (multiplicationOccurrences constant n circuit).length) => termCount

A uniform atom-level restriction yields the corresponding constant per-occurrence budget.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.argumentAtMost_const_of_atMultiplications {K C : Type} [Field K] (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (termCount : ℕ) (restricted : AtMultiplications constant n circuit termCount) : ArgumentAtMost constant n circuit fun (x : Fin 2 → MvPolynomial (Fin (2 * n)) K) => termCount

The same uniform restriction yields a constant semantic argument budget.

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

Local r-term decompositions imply the atom-level catalecticant rank bound r.

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

Locally r-decomposable critical layers force the central-binomial rank/cost tradeoff.

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

Undivided form of the locally decomposable critical-layer tradeoff.