Rectangular Fusion bounds after binary Waring compilation

The degree-parametric compiler satisfies a one-term critical-layer decomposition at every multiplication. Consequently every rectangular split and the optimized split profile yield ordinary arithmetic-circuit lower bounds, with exact source-to-target cost accounting.

def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.CriticalLayerOrPowerAtMultiplications {K : Type} [Field K] (degree : ℕ) (circuit : Circuit (Arithmetic.signature K) degree 1) : Prop

Circuit-level rectangular critical-layer restriction.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.decompositionAtMost_one_of_criticalLayerOrPower {K : Type} [Field K] (degree : ℕ) (polynomial : MvPolynomial (Fin degree) K) (restricted : CriticalLayerOrPower degree polynomial) : Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.AtMost degree 1 polynomial

A zero-or-one-power critical layer is a one-term Waring decomposition.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.gadget_multiplicationAtomProperty {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (operation : SumOfTerms.Op (Term K degree)) (sourceArguments : Fin (SumOfTerms.arity operation) → MvPolynomial (Fin degree) K) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin degree) K)) (present : atom ∈ circuitAtoms ((Translation.Binary.translation degree).operation operation) (Arithmetic.interpretation ⇑MvPolynomial.C) (ContextualTranslation.appendInputs MvPolynomial.X sourceArguments)) : MultiplicationAtomProperty degree atom

Every atom in a rectangular binary contextual gadget satisfies the local critical-layer multiplication property.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_criticalLayerOrPowerAtMultiplications {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) : CriticalLayerOrPowerAtMultiplications degree ((Translation.Binary.translation degree).compile circuit)

Compiled rectangular Waring circuits satisfy the exact critical-layer restriction.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_decompositionAtMultiplications_one {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) : Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Decomposition.AtMultiplications id degree ((Translation.Binary.translation degree).compile circuit) 1

Every compiled multiplication has a one-term critical-layer decomposition, uniformly across all rectangular splits.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_constructs {K : Type} [Field K] (degree : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : (Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.problem K degree).Constructs ((Translation.Binary.translation degree).compile circuit) (Arithmetic.interpretation ⇑MvPolynomial.C)

Rectangular compilation preserves construction of the squarefree target.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_choose_lowerBound {K : Type} [Field K] [CharZero K] (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : degree.choose split ≤ ((Translation.Binary.translation degree).compile circuit).cost Arithmetic.multiplicationCost

Every split gives its full choose degree split multiplication lower bound on the compiled ordinary arithmetic circuit.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_profile_lowerBound {K : Type} [Field K] [CharZero K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : (Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound degree fun (x : Fin (degree + 1)) => 1) ≤ ((Translation.Binary.translation degree).compile circuit).cost Arithmetic.multiplicationCost

The maximum certified over every split is also a compiled-circuit lower bound.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.compiled_middle_lowerBound {K : Type} [Field K] [CharZero K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : degree.choose (degree / 2) ≤ ((Translation.Binary.translation degree).compile circuit).cost Arithmetic.multiplicationCost

The rank-one profile specializes exactly to the middle rectangular split.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.choose_le_termCost_mul_sourceTermCost {K : Type} [Field K] [CharZero K] (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : degree.choose split ≤ Translation.Binary.termMultiplicationCount degree * circuit.cost SumOfTerms.termCost

Exact source-term tradeoff at an arbitrary rectangular split.

theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.choose_le_linearLogCost_mul_sourceTermCost {K : Type} [Field K] [CharZero K] (degree split : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 1) (constructs : (problem K degree).Constructs circuit (SumOfTerms.interpretation termValue)) : degree.choose split ≤ (degree + 2 * degree.log2 + 1) * circuit.cost SumOfTerms.termCost

Closed source-term tradeoff using the logarithmic binary-power bound.