Fusion bounds for binary-compiled Waring circuits

Lift the binary-power atom invariant through the Waring term gadget and the contextual compiler. The resulting ordinary arithmetic circuit satisfies the same critical-layer rank-one restriction as the earlier compilers, while its exact per-term multiplication overhead is smaller.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.termCircuit_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.Binary.termCircuit term) (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X) : MultiplicationAtomProperty n atom

Every multiplication in one complete binary Waring-term gadget satisfies the critical-layer restriction.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).operation operation) (Arithmetic.interpretation ⇑MvPolynomial.C) (ContextualTranslation.appendInputs MvPolynomial.X sourceArguments)) : MultiplicationAtomProperty n atom

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).compile circuit)

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).compile circuit) 1

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).compile circuit) (Arithmetic.interpretation ⇑MvPolynomial.C)

Binary compilation transports construction of the squarefree Waring target to an ordinary arithmetic circuit.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).compile circuit).cost Arithmetic.multiplicationCost

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.centralBinom_le_termCost_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.Binary.termMultiplicationCount n * circuit.cost SumOfTerms.termCost

Rewriting the compiled lower bound by exact cost yields a source-term tradeoff with binary-power overhead.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.centralBinom_le_linearLogCost_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 ≤ (2 * n + 2 * (2 * n).log2 + 1) * circuit.cost SumOfTerms.termCost

Replacing the exact binary count by its logarithmic upper bound gives a closed source-term tradeoff.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.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.Binary.translation n).compile circuit).size

Explicit exponential ordinary-circuit size bound for binary-compiled Waring circuits.