Schnorr closure under monomial substitutions

Schnorr's original progress measure is not merely separation of the displayed support. It is the maximum separation obtainable after replacing every variable by an arbitrary coefficient-one monomial. This closure is what makes the argument stable under the later identification of fresh gate variables with old wires (and under their replacement by constants).

This file builds that closure over a fixed countable target variable type, proves its finite bound, shows that it dominates ordinary separation, and discharges the zero-cost product reverse substitution. The additive enrichment theorem is developed separately.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.transform {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : MvPolynomial ℕ ℕ

Apply a coefficient-one monomial substitution into countably many target variables.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.support_transform {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (transform basis polynomial).support = Finset.image (⇑(MonomialSubstitution.exponentMap basis)) polynomial.support

Exact support of a monomial substitution: it is the image of the source support under the induced linear exponent map.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.card_support_transform_le {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (transform basis polynomial).support.card ≤ polynomial.support.card

Monomial substitution cannot increase the number of support monomials.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationNumber_transform_le_card_sub_one {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : separationNumber (transform basis polynomial).support ≤ polynomial.support.card - 1

Every substituted separation score is bounded by the original support cardinality minus one.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Achievable {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) (score : ℕ) : Prop

A score witnessed after some monomial substitution.

Equations

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

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationClosure {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) : ℕ

Schnorr's substitution-closed separation number. findGreatest is bounded by support cardinality, so the definition remains a concrete natural number despite quantifying over infinitely many monomial substitutions.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationNumber_transform_le_closure {SourceVar : Type u} (basis : SourceVar → ℕ →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : separationNumber (transform basis polynomial).support ≤ separationClosure polynomial

Every particular monomial substitution lower-bounds the closed measure.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationClosure_le_card_sub_one {SourceVar : Type u} (polynomial : MvPolynomial SourceVar ℕ) : separationClosure polynomial ≤ polynomial.support.card - 1

The closed measure retains the same finite support-cardinality bound.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.achievable_separationClosure_of_pos {SourceVar : Type u} {polynomial : MvPolynomial SourceVar ℕ} (positive : 0 < separationClosure polynomial) : Achievable polynomial (separationClosure polynomial)

A positive closed score is witnessed by an actual monomial substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.IsSeparated.image_mapDomain {TargetVar : Type u_1} {Variable : Type u_2} [DecidableEq TargetVar] (embedding : Variable → TargetVar) (injective : Function.Injective embedding) {ambient selected : Finset (Variable →₀ ℕ)} (separated : IsSeparated ambient selected) : IsSeparated (Finset.image (Finsupp.mapDomain embedding) ambient) (Finset.image (Finsupp.mapDomain embedding) selected)

Injective renaming of exponent coordinates preserves separatedness.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationNumber_le_image_mapDomain {TargetVar : Type u_1} {Variable : Type u_2} [DecidableEq TargetVar] (embedding : Variable → TargetVar) (injective : Function.Injective embedding) (ambient : Finset (Variable →₀ ℕ)) : separationNumber ambient ≤ separationNumber (Finset.image (Finsupp.mapDomain embedding) ambient)

Separation number cannot decrease under an injective coordinate renaming.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.finiteBasis (variableCount : ℕ) : Fin variableCount → ℕ →₀ ℕ

Canonical injection of a finite circuit-variable set into the countable substitution universe.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.finiteBasis variableCount coordinate = Finsupp.single (↑coordinate) 1

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.transform_finiteBasis_eq_rename {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) ℕ) : transform (finiteBasis variableCount) polynomial = (MvPolynomial.rename Fin.val) polynomial

The canonical monomial substitution is ordinary injective renaming into Nat.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationNumber_le_closure {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) ℕ) : separationNumber polynomial.support ≤ separationClosure polynomial

Schnorr closure dominates ordinary separation of the displayed support.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.separationClosure_X {variableCount : ℕ} (coordinate : Fin variableCount) : separationClosure (MvPolynomial.X coordinate) = 0

A single variable has zero substitution-closed separation.

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

Lift a target monomial substitution across reverse product enrichment.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.productLift basis left right i = Fin.lastCases (basis left + basis right) basis i

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.transform_product_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) = transform (productLift basis left right) polynomial

Monomial substitution commutes with reverse product enrichment after lifting the eliminated variable to the product exponent.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.product_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

Product reverse substitution cannot increase Schnorr's closed measure.