Separated-monomial progress measures

Schnorr's additive-complexity measure is the largest size, minus one, of a set of target monomials separated inside the entire polynomial support. A set is separated when no support monomial other than the chosen pair divides the product of two chosen monomials.

This file separates the finite combinatorics from polynomial substitution. Pullback is the exact interface needed from one enrichment step: a separated set after substitution can be pulled back to a separated set before substitution, losing at most loss elements. SubstitutionPullbacks then turns addition pullbacks of loss one and multiplication pullbacks of loss zero into the generic reverse-substitution Progress.Measure.

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.Progress.Separated.Exponent (Variable : Type u) : Type u

Exponent vectors for monomials over an arbitrary variable type.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Exponent Variable = (Variable →₀ ℕ)

def Algebraic.Fusion.Arithmetic.Progress.Separated.IsSeparated {Variable : Type u_1} (ambient selected : Finset (Exponent Variable)) : Prop

selected is separated inside ambient: whenever an ambient monomial divides the product of two selected monomials, it is one of that pair.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.IsSeparated.subset {Variable : Type u_1} {ambient selected : Finset (Exponent Variable)} (separated : IsSeparated ambient selected) : selected ⊆ ambient

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.separationNumber {Variable : Type u_1} (ambient : Finset (Exponent Variable)) : ℕ

Schnorr's separation number for a finite monomial support.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.candidate_card_sub_one_le {Variable : Type u_1} {ambient selected : Finset (Exponent Variable)} (separated : IsSeparated ambient selected) : selected.card - 1 ≤ separationNumber ambient

Every separated candidate supplies a lower bound on the separation number.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.separationNumber_le_card_sub_one {Variable : Type u_1} (ambient : Finset (Exponent Variable)) : separationNumber ambient ≤ ambient.card - 1

The separation number never exceeds support cardinality minus one.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.separationNumber_eq_card_sub_one {Variable : Type u_1} {ambient : Finset (Exponent Variable)} (separated : IsSeparated ambient ambient) : separationNumber ambient = ambient.card - 1

If the entire support is separated, its separation number is exactly its cardinality minus one.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.isSeparated_singleton {Variable : Type u_1} (exponent : Exponent Variable) : IsSeparated {exponent} {exponent}

A singleton support is separated.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.separationNumber_singleton {Variable : Type u_1} (exponent : Exponent Variable) : separationNumber {exponent} = 0

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.polynomialValue {variableCount : ℕ} (polynomial : MvPolynomial (Fin variableCount) ℕ) : ℕ

Separation number of a natural-coefficient polynomial. Coefficients are irrelevant; only exact support matters.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.polynomialValue polynomial = Algebraic.Fusion.Arithmetic.Progress.Separated.separationNumber polynomial.support

@[simp]

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

structure Algebraic.Fusion.Arithmetic.Progress.Separated.Pullback {SourceVar : Type u_1} {TargetVar : Type u_2} (source : Finset (Exponent SourceVar)) (target : Finset (Exponent TargetVar)) (loss : ℕ) : Prop

A certificate that separated sets can be pulled back across one support transformation with a bounded loss in cardinality.

• pullback (selected : Finset (Exponent TargetVar)) : IsSeparated target selected → ∃ (prior : Finset (Exponent SourceVar)), IsSeparated source prior ∧ selected.card - 1 ≤ prior.card - 1 + loss

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Pullback.separationNumber_le {SourceVar : Type u_1} {TargetVar : Type u_2} {source : Finset (Exponent SourceVar)} {target : Finset (Exponent TargetVar)} {loss : ℕ} (pullback : Pullback source target loss) : separationNumber target ≤ separationNumber source + loss

A pullback certificate implies the corresponding separation-number inequality.

structure Algebraic.Fusion.Arithmetic.Progress.Separated.SubstitutionPullbacks : Prop

Exact support pullbacks required for the two reverse substitutions. This is the polynomial-specific seam in Schnorr's argument; the circuit telescope does not depend on how these certificates are established.

• add (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : Pullback polynomial.support ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial).support 1
• mul (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : Pullback polynomial.support ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) polynomial).support 0

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.measure (pullbacks : SubstitutionPullbacks) : Measure Arithmetic.additionCost

The separated-monomial measure obtained from exact enrichment pullbacks. Addition costs one and multiplication is free.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.circuit_addition_lowerBound {n : ℕ} (pullbacks : SubstitutionPullbacks) (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))) : polynomialValue target ≤ circuit.cost Arithmetic.additionCost

Schnorr's separation number lower-bounds the number of additions once the two exact support-pullback lemmas have been supplied.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.circuit_addition_lowerBound_of_isSeparated {n : ℕ} (pullbacks : SubstitutionPullbacks) (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

If the entire target support is separated, all but one target monomials must be paid for by additions.