Addition enrichment of coefficient-one monomials

This file develops the binomial half of the unit-separated enrichment proof. After eliminating the last variable by X left + X right, a source monomial expands as its prior-variable monomial times a binomial power. A monomial of coefficient one in that expansion must be one of the two endpoints: all occurrences of the eliminated variable went left, or all went right.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.dropLast {variableCount : ℕ} (exponent : Fin (variableCount + 1) →₀ ℕ) : Fin variableCount →₀ ℕ

Restrict an exponent vector to all coordinates before the last one.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.dropLast exponent = Finsupp.comapDomain Fin.castSucc exponent ⋯

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.dropLast_apply {variableCount : ℕ} (exponent : Fin (variableCount + 1) →₀ ℕ) (coordinate : Fin variableCount) : (dropLast exponent) coordinate = exponent coordinate.castSucc

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.substitution {variableCount : ℕ} (left right : Fin variableCount) : Fin (variableCount + 1) → MvPolynomial (Fin variableCount) ℕ

Reverse substitution of the last variable by a sum.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.substitution left right i = Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.endpoint {variableCount : ℕ} (coordinate : Fin variableCount) (source : Fin (variableCount + 1) →₀ ℕ) : Fin variableCount →₀ ℕ

Endpoint obtained by sending every occurrence of the eliminated variable to coordinate.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.monomialExpansion_eq {variableCount : ℕ} (left right : Fin variableCount) (exponent : Fin (variableCount + 1) →₀ ℕ) : Expansion.monomialExpansion (substitution left right) exponent = (MvPolynomial.monomial (dropLast exponent)) 1 * (MvPolynomial.X left + MvPolynomial.X right) ^ exponent (Fin.last variableCount)

Exact binomial form of one source-monomial expansion.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.pairEmbedding {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) : Fin 2 ↪ Fin variableCount

Embed two distinct target coordinates as the two binary coordinates.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.pairEmbedding left right distinct = { toFun := fun (i : Fin (1 + 1)) => Fin.cases left (fun (x : Fin 1) => right) i, inj' := ⋯ }

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.pairEmbedding_zero {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) : (pairEmbedding left right distinct) 0 = left

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.pairEmbedding_one {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) : (pairEmbedding left right distinct) 1 = right

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.rename_binary_add_pow {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) (power : ℕ) : (MvPolynomial.rename ⇑(pairEmbedding left right distinct)) ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ power) = (MvPolynomial.X left + MvPolynomial.X right) ^ power

Rename the binary binomial power to any two distinct coordinates.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.coeff_add_pow_eq_one {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) (power : ℕ) (exponent : Fin variableCount →₀ ℕ) (coefficientOne : ((MvPolynomial.X left + MvPolynomial.X right) ^ power).coeff exponent = 1) : exponent = Finsupp.single left power ∨ exponent = Finsupp.single right power

A coefficient-one monomial of a binomial power on distinct variables is one of its two endpoints.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.coeff_monomialExpansion_eq_one {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) (source : Fin (variableCount + 1) →₀ ℕ) (target : Fin variableCount →₀ ℕ) (coefficientOne : (Expansion.monomialExpansion (substitution left right) source).coeff target = 1) : target = endpoint left source ∨ target = endpoint right source

For distinct summands, a coefficient-one neighbor of a source monomial is one of the two all-left/all-right expansion endpoints.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.endpoint_le_cross {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) (first second : Fin (variableCount + 1) →₀ ℕ) : endpoint left second ≤ endpoint left first + endpoint right second ∨ endpoint right first ≤ endpoint left first + endpoint right second

The cross product of an all-left endpoint from first and an all-right endpoint from second contains another endpoint from one of the sources.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.not_isSeparated_of_endpoint_pairs {variableCount : ℕ} (left right : Fin variableCount) (distinct : left ≠ right) {ambient selected : Finset (Fin variableCount →₀ ℕ)} (separated : IsSeparated ambient selected) (firstSource secondSource : Fin (variableCount + 1) →₀ ℕ) (firstLeft firstRight secondLeft secondRight : ↥selected) (firstLeftValue : ↑firstLeft = endpoint left firstSource) (firstRightValue : ↑firstRight = endpoint right firstSource) (secondLeftValue : ↑secondLeft = endpoint left secondSource) (secondRightValue : ↑secondRight = endpoint right secondSource) (firstDistinct : firstLeft ≠ firstRight) (secondDistinct : secondLeft ≠ secondRight) (sourcesDistinctLeft : firstLeft ≠ secondLeft) (sourcesDistinctRight : firstRight ≠ secondRight) : False

Two distinct selected endpoint pairs from two sources contradict separation.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.support_add_self_pow {variableCount : ℕ} (coordinate : Fin variableCount) (power : ℕ) : ((MvPolynomial.X coordinate + MvPolynomial.X coordinate) ^ power).support = {Finsupp.single coordinate power}

Repeating the same summand gives a singleton binomial-power support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.support_monomialExpansion_same {variableCount : ℕ} (coordinate : Fin variableCount) (source : Fin (variableCount + 1) →₀ ℕ) : (Expansion.monomialExpansion (substitution coordinate coordinate) source).support = {endpoint coordinate source}

When both addition inputs are the same, every source monomial has one expansion neighbor.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.coeff_monomialExpansion_eq_one_same {variableCount : ℕ} (coordinate : Fin variableCount) (source : Fin (variableCount + 1) →₀ ℕ) (target : Fin variableCount →₀ ℕ) (coefficientOne : (Expansion.monomialExpansion (substitution coordinate coordinate) source).coeff target = 1) : target = endpoint coordinate source

A coefficient-one neighbor in the repeated-input case is the unique endpoint.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.pullback {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : Unit.Pullback polynomial ((MvPolynomial.bind₁ (substitution left right)) polynomial) 1

Reverse substitution by an addition loses at most one unit-separated monomial. Coefficient-one targets have rigid source origins; each origin has at most two endpoint targets, and separation allows at most one such two-element fiber.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.additionPullbacks : Unit.AdditionPullbacks

The fully discharged addition-pullback package for the coefficient-one separation measure.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.measure : Measure Arithmetic.additionCost

Coefficient-one separation is an unconditional progress measure for constant-free monotone arithmetic addition cost.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.circuit_addition_lowerBound {n : ℕ} (target : MvPolynomial (Fin n) ℕ) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (polynomialInterpretation (Fin n))) : Unit.separationNumber target ≤ circuit.cost Arithmetic.additionCost

Every constant-free monotone arithmetic circuit pays at least the coefficient-one separation number of its output polynomial in addition gates.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Addition.circuit_addition_lowerBound_of_unitSeparated {n : ℕ} (target : MvPolynomial (Fin n) ℕ) (targetSeparated : IsSeparated target.support target.support) (coefficientsOne : ∀ exponent ∈ target.support, target.coeff exponent = 1) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (polynomialInterpretation (Fin n))) : target.support.card - 1 ≤ circuit.cost Arithmetic.additionCost

If the full target support is separated and all of its coefficients are one, every target monomial except one must be paid for by an addition gate.