Graded restriction of compiled Waring circuits

The contextual Waring compiler emits only three kinds of multiplication outputs: scalar multiples of variables, proper intermediate powers of a linear form, and full 2n-th powers (optionally with the term scale). The first two are invisible in the critical homogeneous layer; the last kind is a single Waring term. Hence every compiled Waring circuit satisfies the layer-exact rank-one restriction used by catalecticant Fusion.

def Algebraic.Fusion.SumOfTerms.Waring.Restriction.CriticalLayerOrPower {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) : Prop

A polynomial's critical degree-2n component is either zero or one charged Waring term.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.criticalLayerOrPower_of_isHomogeneous_ne {K : Type} [Field K] (n degree : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (homogeneous : polynomial.IsHomogeneous degree) (notCritical : degree ≠ 2 * n) : CriticalLayerOrPower n polynomial

A homogeneous polynomial away from the critical degree is invisible.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.criticalLayerOrPower_termValue {K : Type} {n : ℕ} [Field K] (term : Term K n) : CriticalLayerOrPower n (termValue term)

A charged Waring term occupies the critical layer by itself.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_expressionSum {K : Type} [Field K] (n : ℕ) (expressions : List (Arithmetic.Expression K (2 * n))) (each : ∀ expression ∈ expressions, Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) expression) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) (Translation.expressionSum expressions)

Multiplication-property closure under a right-associated expression sum.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_coefficientVariable {K : Type} [Field K] (n : ℕ) (_positive : 0 < n) (coefficient : K) (index : Fin (2 * n)) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) ((Arithmetic.Expression.constant coefficient).mul (Arithmetic.Expression.input index))

Every coefficient-times-variable product in the linear-form gadget is invisible at positive half-degree.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_linearFormExpression {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (term : Term K n) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) (Translation.linearFormExpression term)

Every multiplication in the linear-form expression is invisible at the critical layer.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_expressionPower {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (term : Term K n) (exponent : ℕ) (bounded : exponent ≤ 2 * n) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) (Translation.expressionPower (Translation.linearFormExpression term) exponent)

Every multiplication in a proper-or-full power expression has an invisible critical layer or is one full Waring power.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_termExpression {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (term : Term K n) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower n) (Translation.termExpression term)

The complete Waring term expression satisfies the critical-layer multiplication property.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_sharedPowerExpression {K : Type} [Field K] (n : ℕ) (_positive : 0 < n) (term : Term K n) (exponent : ℕ) (bounded : exponent ≤ 2 * n) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) (fun (x : Fin 1) => linearForm term) (CriticalLayerOrPower n) (Translation.sharedPowerExpression exponent)

Every multiplication in the shared-input power chain produces a proper or full power of the already-computed linear form.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.multiplicationProperty_scaleExpression {K : Type} [Field K] (n : ℕ) (term : Term K n) : Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) (fun (x : Fin 1) => linearForm term ^ (2 * n)) (CriticalLayerOrPower n) (Translation.scaleExpression term.scale)

The final shared-gadget scaling multiplication produces the charged Waring term.

def Algebraic.Fusion.SumOfTerms.Waring.Restriction.MultiplicationAtomProperty {K : Type} [Field K] (n : ℕ) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin (2 * n)) K)) : Prop

Atom-local packaging of the critical-layer property: it only constrains an atom when that atom is a multiplication.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedTermCircuit_multiplicationAtomProperty {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (term : Term K n) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin (2 * n)) K)) (present : atom ∈ circuitAtoms (Translation.sharedTermCircuit term) (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X) : MultiplicationAtomProperty n atom

Every multiplication atom in the shared-linear-form term gadget obeys the critical-layer restriction.

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

Every atom in an individual contextual Waring gadget satisfies the local critical-layer multiplication property.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedGadget_multiplicationAtomProperty {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (operation : SumOfTerms.Op (Term K n)) (sourceArguments : Fin (SumOfTerms.arity operation) → MvPolynomial (Fin (2 * n)) K) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin (2 * n)) K)) (present : atom ∈ circuitAtoms ((Translation.sharedTranslation n).operation operation) (Arithmetic.interpretation ⇑MvPolynomial.C) (ContextualTranslation.appendInputs MvPolynomial.X sourceArguments)) : MultiplicationAtomProperty n atom

Every atom in an optimized shared-linear-form contextual gadget satisfies the same local critical-layer property.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.compiled_criticalLayerOrPowerAtMultiplications {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) : Arithmetic.Interaction.Polynomial.Catalecticant.Degree.CriticalLayerOrPowerAtMultiplications id n ((Translation.translation n).compile circuit)

Contextual compilation of any Waring circuit satisfies the layer-exact rank-one restriction for ordinary arithmetic circuits.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedCompiled_criticalLayerOrPowerAtMultiplications {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) : Arithmetic.Interaction.Polynomial.Catalecticant.Degree.CriticalLayerOrPowerAtMultiplications id n ((Translation.sharedTranslation n).compile circuit)

Optimized shared-linear-form compilation also satisfies the layer-exact rank-one restriction.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.compiled_decompositionAtMultiplications_one {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) : Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.AtMultiplications id n ((Translation.translation n).compile circuit) 1

Compiled Waring circuits have a one-term decomposition of every critical multiplication layer.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedCompiled_decompositionAtMultiplications_one {K : Type} [Field K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) : Arithmetic.Interaction.Polynomial.Catalecticant.Decomposition.AtMultiplications id n ((Translation.sharedTranslation n).compile circuit) 1

Shared-linear-form compiled circuits also have a one-term decomposition of every critical multiplication layer.

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

Compilation transports construction of the squarefree Waring target to construction by an ordinary arithmetic circuit on the shared variables.

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

Shared-linear-form compilation transports construction of the squarefree Waring target to ordinary arithmetic circuits.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.compiled_multiplication_lowerBound {K : Type} [Field K] [CharZero K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ ((Translation.translation n).compile circuit).cost Arithmetic.multiplicationCost

The compiled ordinary circuit inherits the central-binomial multiplication lower bound from layer-exact catalecticant Fusion.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedCompiled_multiplication_lowerBound {K : Type} [Field K] [CharZero K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ ((Translation.sharedTranslation n).compile circuit).cost Arithmetic.multiplicationCost

The optimized compiled ordinary circuit inherits the same central-binomial multiplication lower bound.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.centralBinom_le_sharedTermCost_mul_sourceTermCost {K : Type} [Field K] [CharZero K] (n : ℕ) (positive : 0 < n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ Translation.sharedTermMultiplicationCount n * circuit.cost SumOfTerms.termCost

Rewriting the optimized compiled lower bound by its exact cost yields an explicit tradeoff with the source Waring term count.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.compiled_four_pow_lt_mul_size {K : Type} [Field K] [CharZero K] (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : 4 ^ n < n * ((Translation.translation n).compile circuit).size

Explicit exponential ordinary-circuit size bound for compiled Waring circuits constructing the squarefree target.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.sharedCompiled_four_pow_lt_mul_size {K : Type} [Field K] [CharZero K] (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : 4 ^ n < n * ((Translation.sharedTranslation n).compile circuit).size

Explicit exponential size bound for optimized shared-linear-form compiled Waring circuits.