Exact monomial expansions under polynomial substitution

This file supplies the algebraic half of the separated-monomial enrichment argument. Over natural coefficients there is no cancellation: the support of bind₁ substitution polynomial is exactly the union, over source monomials, of their individual substitution expansions.

The key factor lemma is independent of the particular substitution. If a source monomial divides the product of two source monomials, then some monomial in its expansion divides the product of any chosen monomials in the two other expansions. This packages the divisibility step used when pulling separation certificates backward.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.monomialExpansion {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (exponent : SourceVar →₀ ℕ) : MvPolynomial TargetVar ℕ

The polynomial obtained by substituting into one coefficient-one source monomial.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.monomialExpansion substitution exponent = (MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) 1)

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_finset_sum {TargetVar : Type v} {Index : Type w} [DecidableEq TargetVar] (indices : Finset Index) (polynomial : Index → MvPolynomial TargetVar ℕ) : (∑ index ∈ indices, polynomial index).support = indices.biUnion fun (index : Index) => (polynomial index).support

Exact support of a finite sum over natural coefficients.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_C_mul_of_pos {TargetVar : Type v} [DecidableEq TargetVar] (coefficient : ℕ) (positive : 0 < coefficient) (polynomial : MvPolynomial TargetVar ℕ) : (MvPolynomial.C coefficient * polynomial).support = polynomial.support

Multiplication by a positive natural scalar does not change polynomial support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_bind₁_monomial_coeff {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (exponent : SourceVar →₀ ℕ) (present : exponent ∈ polynomial.support) : ((MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) (polynomial.coeff exponent))).support = (monomialExpansion substitution exponent).support

A supported source coefficient contributes the same support as the corresponding coefficient-one monomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_bind₁ {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) : ((MvPolynomial.bind₁ substitution) polynomial).support = polynomial.support.biUnion fun (exponent : SourceVar →₀ ℕ) => (monomialExpansion substitution exponent).support

Exact support decomposition of a monotone polynomial substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_pow_congr {TargetVar : Type v} [DecidableEq TargetVar] {left right : MvPolynomial TargetVar ℕ} (supportEqual : left.support = right.support) (power : ℕ) : (left ^ power).support = (right ^ power).support

Powers of two monotone polynomials with the same support again have the same support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_finset_prod_congr {TargetVar : Type v} {Index : Type w} [DecidableEq TargetVar] (indices : Finset Index) (left right : Index → MvPolynomial TargetVar ℕ) (supportEqual : ∀ index ∈ indices, (left index).support = (right index).support) : (∏ index ∈ indices, left index).support = (∏ index ∈ indices, right index).support

Pointwise support equality is preserved by a finite product of monotone polynomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_monomialExpansion_congr {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (left right : SourceVar → MvPolynomial TargetVar ℕ) (supportEqual : ∀ (source : SourceVar), (left source).support = (right source).support) (exponent : SourceVar →₀ ℕ) : (monomialExpansion left exponent).support = (monomialExpansion right exponent).support

The support of a substituted coefficient-one monomial depends only on the supports of the variable images, not their positive coefficients.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.support_bind₁_congr {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (left right : SourceVar → MvPolynomial TargetVar ℕ) (supportEqual : ∀ (source : SourceVar), (left source).support = (right source).support) (polynomial : MvPolynomial SourceVar ℕ) : ((MvPolynomial.bind₁ left) polynomial).support = ((MvPolynomial.bind₁ right) polynomial).support

Over natural coefficients, the support after substitution depends only on the pointwise supports of the substituted variable polynomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.bind₁_eq_sum {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (MvPolynomial.bind₁ substitution) polynomial = ∑ exponent ∈ polynomial.support, (MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) (polynomial.coeff exponent))

Expand a substituted polynomial as the finite sum of the contributions of its supported source monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.coeff_bind₁_eq_sum {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (target : TargetVar →₀ ℕ) : ((MvPolynomial.bind₁ substitution) polynomial).coeff target = ∑ exponent ∈ polynomial.support, ((MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial exponent) (polynomial.coeff exponent))).coeff target

Coefficients after substitution are sums of the coefficients contributed by the supported source monomials.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.IsNeighbor {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (source : SourceVar →₀ ℕ) (target : TargetVar →₀ ℕ) : Prop

Membership in one source-monomial expansion.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.exists_source_of_mem_support_bind₁ {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (target : TargetVar →₀ ℕ) (present : target ∈ ((MvPolynomial.bind₁ substitution) polynomial).support) : ∃ source ∈ polynomial.support, IsNeighbor substitution source target

Every monomial after substitution has a source neighbor.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.mem_support_bind₁_of_neighbor {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (source : SourceVar →₀ ℕ) (sourcePresent : source ∈ polynomial.support) (target : TargetVar →₀ ℕ) (neighbor : IsNeighbor substitution source target) : target ∈ ((MvPolynomial.bind₁ substitution) polynomial).support

Every neighbor of a supported source monomial survives in the whole substituted polynomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.coeff_bind₁_monomial_coeff {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (source : SourceVar →₀ ℕ) (target : TargetVar →₀ ℕ) : ((MvPolynomial.bind₁ substitution) ((MvPolynomial.monomial source) (polynomial.coeff source))).coeff target = polynomial.coeff source * (monomialExpansion substitution source).coeff target

The coefficient contributed by one source monomial factors as its source coefficient times the coefficient in its coefficient-one expansion.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.exists_unique_source_of_coeff_eq_one {SourceVar : Type u} {TargetVar : Type v} [DecidableEq SourceVar] [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (target : TargetVar →₀ ℕ) (coefficientOne : ((MvPolynomial.bind₁ substitution) polynomial).coeff target = 1) : ∃ source ∈ polynomial.support, polynomial.coeff source = 1 ∧ (monomialExpansion substitution source).coeff target = 1 ∧ IsNeighbor substitution source target ∧ ∀ other ∈ polynomial.support, IsNeighbor substitution other target → other = source

A coefficient-one target monomial has a unique source origin. This is the collision-rigidity fact needed by coefficient-sensitive versions of the separation method.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.monomialExpansion_add {SourceVar : Type u} {TargetVar : Type v} (substitution : SourceVar → MvPolynomial TargetVar ℕ) (left right : SourceVar →₀ ℕ) : monomialExpansion substitution (left + right) = monomialExpansion substitution left * monomialExpansion substitution right

Expansion turns addition of exponent vectors into multiplication of their expansion polynomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.exists_neighbor_le_add {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (left right middle : SourceVar →₀ ℕ) (middleLe : middle ≤ left + right) (leftTarget rightTarget : TargetVar →₀ ℕ) (leftNeighbor : IsNeighbor substitution left leftTarget) (rightNeighbor : IsNeighbor substitution right rightTarget) : ∃ (middleTarget : TargetVar →₀ ℕ), IsNeighbor substitution middle middleTarget ∧ middleTarget ≤ leftTarget + rightTarget

If middle divides left * right, every chosen pair of expansion neighbors contains some expansion neighbor of middle.

structure Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.OriginSelection {SourceVar : Type u} {TargetVar : Type v} [DecidableEq SourceVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (selected : Finset (TargetVar →₀ ℕ)) (loss : ℕ) : Type (max u v)

Origins chosen for one separated target set. Rigidity says that a chosen target monomial has exactly the selected source origin among the ambient source support. The score field records the permitted loss after identifying the chosen origins.

• origin : ↥selected → SourceVar →₀ ℕ

  Source origin selected for each target monomial.

• origin_mem (target : ↥selected) : self.origin target ∈ polynomial.support

  Every selected origin belongs to the source support.

• neighbor (target : ↥selected) : IsNeighbor substitution (self.origin target) ↑target

  Each selected target is a neighbor of its selected origin.

• rigid (target : ↥selected) (other : SourceVar →₀ ℕ) : other ∈ polynomial.support → IsNeighbor substitution other ↑target → other = self.origin target

  No other ambient source monomial produces the selected target.

• score : selected.card - 1 ≤ (Finset.image self.origin selected.attach).card - 1 + loss

  Identifying origins loses at most the allowed separation score.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.OriginSelection.prior_isSeparated {SourceVar : Type u} {TargetVar : Type v} [DecidableEq SourceVar] [DecidableEq TargetVar] {substitution : SourceVar → MvPolynomial TargetVar ℕ} {polynomial : MvPolynomial SourceVar ℕ} {selected : Finset (TargetVar →₀ ℕ)} {loss : ℕ} (selection : OriginSelection substitution polynomial selected loss) (separated : IsSeparated ((MvPolynomial.bind₁ substitution) polynomial).support selected) : IsSeparated polynomial.support (Finset.image selection.origin selected.attach)

Rigid origins pull a separated target set back to a separated source set.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Expansion.pullback_of_originSelections {SourceVar : Type u} {TargetVar : Type v} [DecidableEq SourceVar] [DecidableEq TargetVar] (substitution : SourceVar → MvPolynomial TargetVar ℕ) (polynomial : MvPolynomial SourceVar ℕ) (loss : ℕ) (selections : (selected : Finset (Exponent TargetVar)) → IsSeparated ((MvPolynomial.bind₁ substitution) polynomial).support selected → OriginSelection substitution polynomial selected loss) : Pullback polynomial.support ((MvPolynomial.bind₁ substitution) polynomial).support loss

If every separated target set admits rigid origins with a fixed loss, then the substitution supplies the abstract separation pullback certificate.