Addition enrichment for weighted Schnorr closure

An observation in the weighted closure may send a wire to a zero monomial. If either input of the new addition has zero weight, the apparent addition collapses to one weighted monomial substitution and costs nothing. If both endpoint weights are positive, their coefficients do not affect support. Zero-weight prior variables are first pruned, after which the existing coefficient-one Schnorr shift theorem applies verbatim.

This proves the missing one-step addition law and packages weighted closure as an unconditional addition-cost measure for monotone arithmetic circuits with arbitrary natural constants, including zero.

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

Substitution seen after applying a weighted monomial observation to a reverse addition step.

Equations

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

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

Post-composing reverse addition with a weighted observation gives the observed substitution above.

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.endpointWeight {variableCount : ℕ} (weight : Fin variableCount → ℕ) (endpoint : Fin variableCount) : Fin (variableCount + 1) → ℕ

Lift a surviving endpoint's weight across the eliminated variable.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.endpointWeight weight endpoint i = Fin.lastCases (weight endpoint) weight i

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.transform_reverse_add_eq_right_of_left_zero {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) (leftZero : weight left = 0) : transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) = transform (endpointWeight weight right) (Addition.endpointBasis basis (basis right)) polynomial

If the left endpoint has zero weight, observed addition is exactly the right endpoint weighted monomial substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.transform_reverse_add_eq_left_of_right_zero {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) (rightZero : weight right = 0) : transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) = transform (endpointWeight weight left) (Addition.endpointBasis basis (basis left)) polynomial

If the right endpoint has zero weight, observed addition is exactly the left endpoint weighted monomial substitution.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.pruneSubstitution {variableCount : ℕ} (weight : Fin variableCount → ℕ) : Fin (variableCount + 1) → MvPolynomial (Fin (variableCount + 1)) ℕ

Delete zero-weight prior variables but retain the eliminated last variable for the classical binary enrichment argument.

Equations

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

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.prune {variableCount : ℕ} (weight : Fin variableCount → ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) : MvPolynomial (Fin (variableCount + 1)) ℕ

Polynomial obtained by pruning monomials that use zero-weight prior variables.

Equations

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

def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.pruneWeight {variableCount : ℕ} (weight : Fin variableCount → ℕ) : Fin (variableCount + 1) → ℕ

Unit-or-zero weights encoding the pruning substitution.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.pruneWeight weight i = Fin.lastCases 1 (fun (prior : Fin variableCount) => if weight prior = 0 then 0 else 1) i

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.transform_prune_endpoint_eq {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (endpoint : ℕ →₀ ℕ) : Closure.transform (Addition.endpointBasis basis endpoint) (prune weight polynomial) = transform (pruneWeight weight) (Addition.endpointBasis basis endpoint) polynomial

Transforming a pruned polynomial at one endpoint is exactly a weighted transform of the original polynomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.support_transform_reverse_add_eq_pruned {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) (leftPositive : 0 < weight left) (rightPositive : 0 < weight right) : (transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial)).support = ((MvPolynomial.bind₁ (Addition.substitution basis (basis left) (basis right))) (prune weight polynomial)).support

With positive endpoint weights, weighted observed enrichment has the same support as coefficient-one enrichment of the pruned polynomial.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.separationNumber_transform_reverse_add_le {variableCount : ℕ} (weight : Fin variableCount → ℕ) (basis : Fin variableCount → ℕ →₀ ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (left right : Fin variableCount) : separationNumber (transform weight basis ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial)).support ≤ separationClosure polynomial + 1

Every weighted observation of a reverse addition raises separation by at most one relative to the original weighted closure.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.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 weighted Schnorr closure by at most one.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.measure {K : Type u_1} (constant : K → ℕ) : General.Measure constant Arithmetic.additionCost

Weighted Schnorr closure is an unconditional addition-cost progress measure for every natural interpretation of named constants.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.circuit_addition_lowerBound {K : Type u_1} {n : ℕ} (constant : K → ℕ) (target : MvPolynomial (Fin n) ℕ) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : separationClosure target ≤ circuit.cost Arithmetic.additionCost

Weighted Schnorr closure lower-bounds additions with arbitrary natural constants, zero included.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.circuit_addition_lowerBound_of_separationNumber {K : Type u_1} {n : ℕ} (constant : K → ℕ) (target : MvPolynomial (Fin n) ℕ) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : separationNumber target.support ≤ circuit.cost Arithmetic.additionCost

Ordinary support separation remains a lower bound with arbitrary natural constants.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Closure.Weighted.Addition.circuit_addition_lowerBound_of_isSeparated {K : Type u_1} {n : ℕ} (constant : K → ℕ) (target : MvPolynomial (Fin n) ℕ) (targetSeparated : IsSeparated target.support target.support) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (General.polynomialInterpretation constant (Fin n))) : target.support.card - 1 ≤ circuit.cost Arithmetic.additionCost

Full-support Schnorr form with arbitrary natural constants.