Two-shadow bounds for shifted pairwise products

Request all polynomials 1 + x_i y_j from two blocks of n variables. The quadratic coefficient or Hessian shadow forces n^2 multiplications. After a suitable affine one-variable specialization, the distinct linear factors of the same outputs give n^2 independent root-multiplicity shadows and force n^2 additions. The two component bounds add, giving 2 n^2 nonconstant gates.

The general theorem leaves the elementary choice of specialization parameters explicit. Its hypotheses say that the n^2 resulting roots are distinct and avoid the roots of the specialized free inputs. A second endpoint supplies such parameters over the rationals for every n.

The circuits here use addition, multiplication, and named constants, without division. The additive ingredient is the classical addition-rank method; this file records a checked two-shadow corollary, not a claim of historical priority.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.targets (K : Type) [Field K] (n : ℕ) : Fin (n * n) → MvPolynomial (Fin n ⊕ Fin n) K

Pairwise products with a constant term adjoined.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.targets K n output = 1 + Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.targets K n output

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.specialization {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) : MvPolynomial (Fin n ⊕ Fin n) K →+* Polynomial K

Specialize every left variable to a scalar and every right variable to an affine copy of the univariate indeterminate.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.specialization_C {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (scalar : K) : (specialization leftValue rightOffset) (MvPolynomial.C scalar) = Polynomial.C scalar

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.specialization_X_inl {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (left : Fin n) : (specialization leftValue rightOffset) (MvPolynomial.X (Sum.inl left)) = Polynomial.C (leftValue left)

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.specialization_X_inr {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (right : Fin n) : (specialization leftValue rightOffset) (MvPolynomial.X (Sum.inr right)) = Polynomial.X + Polynomial.C (rightOffset right)

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rootPoints {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (output : Fin (n * n)) : K

Root of the specialized shifted product indexed by output.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rootPoints leftValue rightOffset output = -(leftValue (finProdFinEquiv.symm output).1)⁻¹ - rightOffset (finProdFinEquiv.symm output).2

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rationalLeftValue (n : ℕ) (left : Fin n) : ℚ

Explicit rational specialization: the reciprocal of the left value is a positive block offset, while the right offset is its coordinate index.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rationalLeftValue n left = (↑(n * (↑left + 1)))⁻¹

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rationalRightOffset {n : ℕ} (right : Fin n) : ℚ

Right offsets for the explicit rational specialization.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rationalRightOffset right = ↑↑right

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rational_rootPoints (n : ℕ) (output : Fin (n * n)) : rootPoints (rationalLeftValue n) rationalRightOffset output = -↑(↑output + n)

The explicit root indexed by an output is just the negative of its one-based flattened index shifted by one full block.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rationalLeftValue_ne_zero {n : ℕ} (left : Fin n) : rationalLeftValue n left ≠ 0

All explicit rational left values are nonzero.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rational_rootPoints_injective (n : ℕ) : Function.Injective (rootPoints (rationalLeftValue n) rationalRightOffset)

Distinct outputs receive distinct explicit rational roots.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rational_rootPoints_avoidRight {n : ℕ} (output : Fin (n * n)) (right : Fin n) : rootPoints (rationalLeftValue n) rationalRightOffset output ≠ -rationalRightOffset right

Explicit target roots never hit a root of a specialized right input.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.specialization_target {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (output : Fin (n * n)) : (specialization leftValue rightOffset) (targets K n output) = Polynomial.C (leftValue (finProdFinEquiv.symm output).1) * (Polynomial.X - Polynomial.C (rootPoints leftValue rightOffset output))

The shifted product specializes to a nonzero scalar times its designated linear factor.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.input_rootMultiplicity_eq_zero {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (avoidRightRoots : ∀ (output : Fin (n * n)) (right : Fin n), rootPoints leftValue rightOffset output ≠ -rightOffset right) (input : Fin (2 * n)) (output : Fin (n * n)) : Polynomial.rootMultiplicity (rootPoints leftValue rightOffset output) ((specialization leftValue rightOffset) ((Interaction.Hessian.Pairwise.inputProblem K n).inputs input)) = 0

The specialized free inputs have no selected roots.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.additionCertificate {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (leftValue rightOffset : Fin n → K) (avoidRightRoots : ∀ (output : Fin (n * n)) (right : Fin n), rootPoints leftValue rightOffset output ≠ -rightOffset right) : Certificate (fun (scalar : C) => MvPolynomial.C (constant scalar)) (Interaction.Hessian.Pairwise.inputProblem K n)

Root-multiplicity shadow certificate on the original multivariate polynomial problem, obtained by pulling the univariate certificate back along the specialization.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.targetFeatures_eq_single {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (roots_injective : Function.Injective (rootPoints leftValue rightOffset)) (output : Fin (n * n)) : RootMultiplicity.rootMultiplicityFeature (rootPoints leftValue rightOffset) ((specialization leftValue rightOffset) (targets K n output)) = Pi.single output 1

The target root-multiplicity shadows are the standard basis vectors.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.targetFeatures_linearIndependent {K : Type} [Field K] {n : ℕ} (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (roots_injective : Function.Injective (rootPoints leftValue rightOffset)) : LinearIndependent K (RootMultiplicity.rootMultiplicityFeature (rootPoints leftValue rightOffset) ∘ ⇑(specialization leftValue rightOffset) ∘ targets K n)

The target divisor shadows are linearly independent.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.hessianFeatures_linearIndependent {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) : LinearIndependent K (Interaction.Hessian.linearMap point ∘ targets K n)

The Hessian shadows of shifted pairwise products are unchanged by the constant term and remain linearly independent.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.circuit_addition_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (roots_injective : Function.Injective (rootPoints leftValue rightOffset)) (avoidRightRoots : ∀ (output : Fin (n * n)) (right : Fin n), rootPoints leftValue rightOffset output ≠ -rightOffset right) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem K n) (targets K n) circuit) : n * n ≤ circuit.cost Arithmetic.additionCost

Computing all shifted pairwise products requires n^2 additions.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.circuit_multiplication_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem K n) (targets K n) circuit) : n * n ≤ circuit.cost Arithmetic.multiplicationCost

Computing all shifted pairwise products requires n^2 multiplications.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.circuit_gate_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (roots_injective : Function.Injective (rootPoints leftValue rightOffset)) (avoidRightRoots : ∀ (output : Fin (n * n)) (right : Fin n), rootPoints leftValue rightOffset output ≠ -rightOffset right) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem K n) (targets K n) circuit) : n * n + n * n ≤ circuit.cost Arithmetic.gateCost

The two independent shadows add to an exact-form 2 n^2 lower bound on nonconstant arithmetic gates.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.circuit_size_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (leftValue rightOffset : Fin n → K) (left_ne_zero : ∀ (left : Fin n), leftValue left ≠ 0) (roots_injective : Function.Injective (rootPoints leftValue rightOffset)) (avoidRightRoots : ∀ (output : Fin (n * n)) (right : Fin n), rootPoints leftValue rightOffset output ≠ -rightOffset right) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem K n) (targets K n) circuit) : n * n + n * n ≤ circuit.size

The raw circuit size obeys the same two-shadow lower bound.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rational_circuit_gate_lowerBound {C : Type u_1} (constant : C → ℚ) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem ℚ n) (targets ℚ n) circuit) : n * n + n * n ≤ circuit.cost Arithmetic.gateCost

Unconditional rational-field instance of the two-shadow gate bound.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Pairwise.rational_circuit_size_lowerBound {C : Type u_1} (constant : C → ℚ) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Interaction.Multiple.Constructs (Interaction.Hessian.Pairwise.inputProblem ℚ n) (targets ℚ n) circuit) : n * n + n * n ≤ circuit.size

Unconditional rational-field instance of the two-shadow size bound.