Coefficient-one separated monomials

Raw support can have collision fibers under substitution. A target monomial whose coefficient is exactly one cannot: exact coefficient decomposition gives it a unique source origin, and that source monomial also has coefficient one. This file packages the resulting collision-rigid separation measure.

Product enrichment is discharged completely: every source monomial has one monomial-valued expansion, so the unique-origin map is injective. The only remaining input to measure is the genuinely additive score bound.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.IsUnitSeparated {Variable : Type u_1} (polynomial : MvPolynomial Variable ℕ) (selected : Finset (Variable →₀ ℕ)) : Prop

A separated support subset all of whose ambient coefficients are one.

Equations

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

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.separationNumber {Variable : Type u_1} (polynomial : MvPolynomial Variable ℕ) : ℕ

Maximum coefficient-one separation score of a polynomial.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.candidate_card_sub_one_le {Variable : Type u_1} {polynomial : MvPolynomial Variable ℕ} {selected : Finset (Variable →₀ ℕ)} (separated : IsUnitSeparated polynomial selected) : selected.card - 1 ≤ separationNumber polynomial

Every coefficient-one separated candidate lower-bounds the unit separation number.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.separationNumber_le_card_sub_one {Variable : Type u_1} (polynomial : MvPolynomial Variable ℕ) : separationNumber polynomial ≤ polynomial.support.card - 1

Unit separation number is at most support cardinality minus one.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.separationNumber_X {Variable : Type u_1} (coordinate : Variable) : separationNumber (MvPolynomial.X coordinate) = 0

A single variable has zero unit separation score.

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

Pull back coefficient-one separated candidates across one substitution.

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

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

Unit pullbacks imply the corresponding separation-number inequality.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.product_pullback {variableCount : ℕ} (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : Pullback polynomial ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) polynomial) 0

Product reverse substitution preserves the coefficient-one separation score.

structure Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.AdditionPullbacks : Prop

The only additional combinatorial input needed for the unit-separated measure: addition enrichment loses at most one unit-separated score.

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

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Unit.measure (additionPullbacks : AdditionPullbacks) : Measure Arithmetic.additionCost

Coefficient-one separated monomials form an addition-cost progress measure once the additive one-loss theorem is supplied; product enrichment is already proved internally.

Equations

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