Additive enrichment for Schnorr's substitution closure

After an arbitrary monomial substitution, eliminating a gate variable by a sum replaces its monomial image by the sum of two monomials. A source monomial with last-variable degree k consequently has neighbors indexed by splits a + b = k.

The key shift argument is Schnorr's original one. Fix a selected neighbor outside the all-left endpoint support. Any selected neighbor outside the all-right endpoint support must equal the monomial obtained by shifting one occurrence from right to left in the fixed neighbor. Hence the selected set loses at most one element on restriction to an endpoint support.

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

Exponent contributed by all source coordinates before the eliminated last variable.

Equations

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

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

Substitute the last source variable by the sum of two coefficient-one monomials and all prior variables according to basis.

Equations

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

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.endpointBasis {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (endpoint : ℕ →₀ ℕ) : Fin (variableCount + 1) → ℕ →₀ ℕ

Endpoint monomial substitution sending every eliminated occurrence to endpoint.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.endpointBasis basis endpoint i = Fin.lastCases endpoint basis i

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.binaryBasis (left right : ℕ →₀ ℕ) : Fin 2 → ℕ →₀ ℕ

Binary basis whose two variables denote the two endpoint monomials.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.binaryBasis left right i = Fin.cases left (fun (x : Fin 1) => right) i

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.binaryBasis_zero (left right : ℕ →₀ ℕ) : binaryBasis left right 0 = left

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.binaryBasis_one (left right : ℕ →₀ ℕ) : binaryBasis left right 1 = right

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.binaryExponentMap_eq (left right : ℕ →₀ ℕ) (exponent : Fin 2 →₀ ℕ) : (MonomialSubstitution.exponentMap (binaryBasis left right)) exponent = exponent 0 • left + exponent 1 • right

The induced binary exponent map is the expected linear combination of the two endpoint exponents.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.transform_binary_add_pow (left right : ℕ →₀ ℕ) (power : ℕ) : transform (binaryBasis left right) ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ power) = ((MvPolynomial.monomial left) 1 + (MvPolynomial.monomial right) 1) ^ power

Substituting the binary basis into a binary power gives the power of the two endpoint monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.exists_split_of_mem_support_add_pow (left right target : ℕ →₀ ℕ) (power : ℕ) (present : target ∈ (((MvPolynomial.monomial left) 1 + (MvPolynomial.monomial right) 1) ^ power).support) : ∃ (leftPower : ℕ) (rightPower : ℕ), leftPower + rightPower = power ∧ target = leftPower • left + rightPower • right

Every monomial in a power of two coefficient-one monomials comes from a split of the power between them.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.split_mem_support_add_pow (left right : ℕ →₀ ℕ) {leftPower rightPower power : ℕ} (sumPower : leftPower + rightPower = power) : leftPower • left + rightPower • right ∈ (((MvPolynomial.monomial left) 1 + (MvPolynomial.monomial right) 1) ^ power).support

Every numerical split of a binary power contributes its corresponding monomial to the support.

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

Exact binomial form of one source-monomial expansion under a sum of two monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.exists_split_of_neighbor {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (source : Fin (variableCount + 1) →₀ ℕ) (target : ℕ →₀ ℕ) (neighbor : Expansion.IsNeighbor (substitution basis left right) source target) : ∃ (leftPower : ℕ) (rightPower : ℕ), leftPower + rightPower = source (Fin.last variableCount) ∧ target = baseExponent basis source + (leftPower • left + rightPower • right)

Every neighbor of a source monomial has a split representation.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.neighbor_of_split {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (source : Fin (variableCount + 1) →₀ ℕ) {leftPower rightPower : ℕ} (sumPower : leftPower + rightPower = source (Fin.last variableCount)) : Expansion.IsNeighbor (substitution basis left right) source (baseExponent basis source + (leftPower • left + rightPower • right))

Every split representation is an actual expansion neighbor.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.endpointExponentMap_eq {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (endpoint : ℕ →₀ ℕ) (source : Fin (variableCount + 1) →₀ ℕ) : (MonomialSubstitution.exponentMap (endpointBasis basis endpoint)) source = baseExponent basis source + source (Fin.last variableCount) • endpoint

The exponent map of an endpoint substitution is the prior contribution plus the last-variable degree times the endpoint exponent.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.leftEndpoint_support_subset {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) : (transform (endpointBasis basis left) polynomial).support ⊆ ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support

The all-left endpoint support is contained in the enriched support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.rightEndpoint_support_subset {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) : (transform (endpointBasis basis right) polynomial).support ⊆ ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support

The all-right endpoint support is contained in the enriched support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.IsSeparated.inter_of_subset {Variable : Type u_1} [DecidableEq Variable] {ambient smaller selected : Finset (Variable →₀ ℕ)} (separated : IsSeparated ambient selected) (smallerSubset : smaller ⊆ ambient) : IsSeparated smaller (selected ∩ smaller)

Restricting a separated set to a smaller ambient support preserves separatedness.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftLeft (base left right : ℕ →₀ ℕ) (leftPower rightPower : ℕ) : ℕ →₀ ℕ

Shift one eliminated-variable occurrence from the right monomial to the left monomial.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftLeft base left right leftPower rightPower = base + ((leftPower + 1) • left + (rightPower - 1) • right)

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftRight (base left right : ℕ →₀ ℕ) (leftPower rightPower : ℕ) : ℕ →₀ ℕ

Shift one eliminated-variable occurrence from the left monomial to the right monomial.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftRight base left right leftPower rightPower = base + ((leftPower - 1) • left + (rightPower + 1) • right)

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftLeft_add_shiftRight (firstBase secondBase left right : ℕ →₀ ℕ) (firstLeft firstRight secondLeft secondRight : ℕ) (firstRightPositive : 0 < firstRight) (secondLeftPositive : 0 < secondLeft) : shiftLeft firstBase left right firstLeft firstRight + shiftRight secondBase left right secondLeft secondRight = firstBase + (firstLeft • left + firstRight • right) + (secondBase + (secondLeft • left + secondRight • right))

Opposite one-step shifts preserve the product exponent of the original two monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.shiftLeft_le_add (firstBase secondBase left right : ℕ →₀ ℕ) (firstLeft firstRight secondLeft secondRight : ℕ) (firstRightPositive : 0 < firstRight) (secondLeftPositive : 0 < secondLeft) : shiftLeft firstBase left right firstLeft firstRight ≤ firstBase + (firstLeft • left + firstRight • right) + (secondBase + (secondLeft • left + secondRight • right))

The left shift divides the product of the two original monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.leftEndpoint_eq_of_shiftLeft_eq (base left right : ℕ →₀ ℕ) (leftPower rightPower totalPower : ℕ) (rightPositive : 0 < rightPower) (sumPower : leftPower + rightPower = totalPower) (shiftEqual : shiftLeft base left right leftPower rightPower = base + (leftPower • left + rightPower • right)) : base + totalPower • left = base + (leftPower • left + rightPower • right)

If a nontrivial left shift does not change a monomial, then that monomial was already its all-left endpoint.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.rightPower_pos_of_not_mem_leftEndpoint {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (source : Fin (variableCount + 1) →₀ ℕ) (sourcePresent : source ∈ polynomial.support) (target : ℕ →₀ ℕ) (leftPower rightPower : ℕ) (sumPower : leftPower + rightPower = source (Fin.last variableCount)) (targetEqual : target = baseExponent basis source + (leftPower • left + rightPower • right)) (notLeftEndpoint : target ∉ (transform (endpointBasis basis left) polynomial).support) : 0 < rightPower

A representation outside the all-left endpoint support uses the right summand at least once.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.leftPower_pos_of_not_mem_rightEndpoint {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (source : Fin (variableCount + 1) →₀ ℕ) (sourcePresent : source ∈ polynomial.support) (target : ℕ →₀ ℕ) (leftPower rightPower : ℕ) (sumPower : leftPower + rightPower = source (Fin.last variableCount)) (targetEqual : target = baseExponent basis source + (leftPower • left + rightPower • right)) (notRightEndpoint : target ∉ (transform (endpointBasis basis right) polynomial).support) : 0 < leftPower

A representation outside the all-right endpoint support uses the left summand at least once.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.eq_shiftLeft_of_not_mem_endpoints {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) {selected : Finset (ℕ →₀ ℕ)} (separated : IsSeparated ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support selected) (fixed : ℕ →₀ ℕ) (fixedSelected : fixed ∈ selected) (fixedNotLeft : fixed ∉ (transform (endpointBasis basis left) polynomial).support) (fixedSource : Fin (variableCount + 1) →₀ ℕ) (fixedSourcePresent : fixedSource ∈ polynomial.support) (fixedLeft fixedRight : ℕ) (fixedSum : fixedLeft + fixedRight = fixedSource (Fin.last variableCount)) (fixedEqual : fixed = baseExponent basis fixedSource + (fixedLeft • left + fixedRight • right)) (other : ℕ →₀ ℕ) (otherSelected : other ∈ selected) (otherNotRight : other ∉ (transform (endpointBasis basis right) polynomial).support) : other = shiftLeft (baseExponent basis fixedSource) left right fixedLeft fixedRight

Schnorr's shift lemma: relative to one selected monomial outside the all-left endpoint support, every selected monomial outside the all-right endpoint support is the same fixed left shift.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.outside_right_subsingleton_of_not_subset_left {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) {selected : Finset (ℕ →₀ ℕ)} (separated : IsSeparated ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support selected) (notSubsetLeft : ¬selected ⊆ (transform (endpointBasis basis left) polynomial).support) : (selected \ (transform (endpointBasis basis right) polynomial).support).card ≤ 1

Once a selected monomial lies outside the left endpoint support, the selected complement of the right endpoint support is subsingleton.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.restrict_to_endpoint {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (selected : Finset (ℕ →₀ ℕ)) (separated : IsSeparated ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support selected) : IsSeparated (transform (endpointBasis basis left) polynomial).support (selected ∩ (transform (endpointBasis basis left) polynomial).support) ∧ selected.card - 1 ≤ (selected ∩ (transform (endpointBasis basis left) polynomial).support).card - 1 + 1 ∨ IsSeparated (transform (endpointBasis basis right) polynomial).support (selected ∩ (transform (endpointBasis basis right) polynomial).support) ∧ selected.card - 1 ≤ (selected ∩ (transform (endpointBasis basis right) polynomial).support).card - 1 + 1

Every separated enriched set restricts to one endpoint support while losing at most one element.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.separationNumber_bind_add_le {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (left right : ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) : separationNumber ((MvPolynomial.bind₁ (substitution basis left right)) polynomial).support ≤ max (separationNumber (transform (endpointBasis basis left) polynomial).support) (separationNumber (transform (endpointBasis basis right) polynomial).support) + 1

Separation after replacing one variable by a sum of two monomials is at most the larger endpoint separation plus one.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.transform_reverse_add_eq {variableCount : ℕ} (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : transform basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) = (MvPolynomial.bind₁ (substitution basis (basis left) (basis right))) polynomial

A post-composed monomial substitution turns ordinary reverse addition enrichment into substitution of the eliminated variable by the sum of the two corresponding monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.separationClosure_add_substitution_le {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : separationClosure ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) ≤ separationClosure polynomial + 1

Reverse addition substitution grows Schnorr's closed separation by at most one.

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

Schnorr's substitution-closed separation is an unconditional addition progress measure for constant-free monotone arithmetic circuits.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.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))) : separationClosure target ≤ circuit.cost Arithmetic.additionCost

Coefficient-insensitive Schnorr closure lower-bounds additions in every constant-free monotone arithmetic circuit.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.circuit_addition_lowerBound_of_separationNumber {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))) : separationNumber target.support ≤ circuit.cost Arithmetic.additionCost

Ordinary support separation is a coefficient-insensitive addition lower bound.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Addition.circuit_addition_lowerBound_of_isSeparated {n : ℕ} (target : MvPolynomial (Fin n) ℕ) (targetSeparated : IsSeparated target.support target.support) (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

Schnorr's classical theorem: if the full monomial support is separated, all but one support monomials must be paid for by additions, independently of their positive coefficients.