Waring decompositions as rectangular rank profiles

Uniform local Waring decompositions produce a constant rectangular rank profile. This small adapter keeps the generic profile API independent of the chosen structural proof of its local bounds.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.Decomposition.multiplicationOutputRankAtMost {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (termCount : ℕ) (restricted : Decomposition.AtMultiplications constant degree circuit termCount) : MultiplicationOutputRankAtMost constant degree degreeAtLeastTwo circuit fun (x : Fin (degree + 1)) => termCount

A uniform local Waring decomposition gives the same rank bound at every rectangular split.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.Decomposition.certifiedLowerBound {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree : ℕ) (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 : Decomposition.AtMultiplications constant degree circuit termCount) : (Profile.certifiedLowerBound degree fun (x : Fin (degree + 1)) => termCount) ≤ circuit.cost Arithmetic.multiplicationCost

The profile-optimized lower bound obtained from a uniform local Waring decomposition. Keeping it in profile form lets later adapters combine it with split-sensitive estimates without changing the circuit theorem.