Reverse-substitution progress measures over a commutative semiring

This is the constant-alphabet-generic core of arithmetic reverse substitution. Every input and gate wire receives a formal variable, and gates are eliminated in reverse topological order. Addition and multiplication substitute the last variable by the corresponding expression in prior wire variables; a named constant substitutes its constant polynomial.

Measure exposes one local law for each operation. These laws telescope over the circuit DAG, so shared gates are charged exactly once.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.General.polynomialInterpretation {R : Type u_1} {K : Type u_2} [CommSemiring R] (constant : K → R) (V : Type v) : Interpretation (Arithmetic.signature K) (MvPolynomial V R)

Arithmetic interpretation on semiring-coefficient polynomials, with named constants interpreted by constant.

Equations

• Algebraic.Fusion.Arithmetic.Progress.General.polynomialInterpretation constant V = Algebraic.Arithmetic.interpretation fun (scalar : K) => MvPolynomial.C (constant scalar)

theorem Algebraic.Fusion.Arithmetic.Progress.General.wire_index_castSucc {n g : ℕ} (wire : Wire n g) : wire.castSucc.index = wire.index.castSucc

Extending the wire namespace by one gate commutes with the positional numbering of wires.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.General.lineFormalResult {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (line : Line (Arithmetic.signature K) n g) : MvPolynomial (Fin (n + g)) R

Formal polynomial computed by one arithmetic line from variables naming all wires in its prefix, each wire named by its position Wire.index.

Equations

• Algebraic.Fusion.Arithmetic.Progress.General.lineFormalResult constant { op := Algebraic.Arithmetic.Op.add, wires := wires } = MvPolynomial.X (wires 0).index + MvPolynomial.X (wires 1).index
• Algebraic.Fusion.Arithmetic.Progress.General.lineFormalResult constant { op := Algebraic.Arithmetic.Op.mul, wires := wires } = MvPolynomial.X (wires 0).index * MvPolynomial.X (wires 1).index
• Algebraic.Fusion.Arithmetic.Progress.General.lineFormalResult constant { op := Algebraic.Arithmetic.Op.constant scalar, wires := wires } = MvPolynomial.C (constant scalar)

noncomputable def Algebraic.Fusion.Arithmetic.Progress.General.lineReverseSubstitution {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (line : Line (Arithmetic.signature K) n g) : MvPolynomial (Fin (n + g + 1)) R →ₐ[R] MvPolynomial (Fin (n + g)) R

Eliminate the new last gate-variable by substituting its formal result.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.General.lineReverseSubstitution_X_last {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (line : Line (Arithmetic.signature K) n g) : (lineReverseSubstitution constant line) (MvPolynomial.X (Fin.last (n.add g))) = lineFormalResult constant line

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.General.lineReverseSubstitution_X_castSucc {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (line : Line (Arithmetic.signature K) n g) (wire : Wire n g) : (lineReverseSubstitution constant line) (MvPolynomial.X wire.castSucc.index) = MvPolynomial.X wire.index

def Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (program : Program (Arithmetic.signature K) n g) : MvPolynomial (Fin (n + g)) R →ₐ[R] MvPolynomial (Fin n) R

Expand every formal gate-variable by eliminating gates in reverse topological order.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom constant Cslib.Circuits.Program.empty = AlgHom.id R (MvPolynomial (Fin (n + 0)) R)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom_empty {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] (constant : K → R) : programExpansionHom constant Program.empty = AlgHom.id R (MvPolynomial (Fin (n + 0)) R)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom_gate {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (program : Program (Arithmetic.signature K) n g) (line : Line (Arithmetic.signature K) n g) : programExpansionHom constant (program.gate line) = (programExpansionHom constant program).comp (lineReverseSubstitution constant line)

theorem Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom_X {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] (constant : K → R) (program : Program (Arithmetic.signature K) n g) (wire : Wire n g) : (programExpansionHom constant program) (MvPolynomial.X wire.index) = program.trace (polynomialInterpretation constant (Fin n)) MvPolynomial.X wire

Expanding a formal wire-variable gives the polynomial carried by that wire in the original program.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.General.circuitFormalOutput {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] (circuit : Circuit (Arithmetic.signature K) n 1) : MvPolynomial (Fin (n + circuit.size)) R

The formal output variable of a single-output circuit.

Equations

• Algebraic.Fusion.Arithmetic.Progress.General.circuitFormalOutput circuit = MvPolynomial.X (circuit.outputs 0).index

noncomputable def Algebraic.Fusion.Arithmetic.Progress.General.circuitExpandedOutput {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] (constant : K → R) (circuit : Circuit (Arithmetic.signature K) n 1) : MvPolynomial (Fin n) R

Polynomial obtained by reverse-substituting every gate into the formal output variable.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Progress.General.circuitExpandedOutput_eq_eval {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] (constant : K → R) (circuit : Circuit (Arithmetic.signature K) n 1) : circuitExpandedOutput constant circuit = circuit.eval (polynomialInterpretation constant (Fin n)) MvPolynomial.X 0

Reverse substitution recovers ordinary polynomial evaluation.

structure Algebraic.Fusion.Arithmetic.Progress.General.Measure {R : Type u_1} {K : Type u_2} [CommSemiring R] (constant : K → R) (operationCost : OperationCost (Arithmetic.signature K)) : Type u_1

A polymorphic polynomial progress measure compatible with all three reverse substitutions.

• value (variableCount : ℕ) : MvPolynomial (Fin variableCount) R → ℕ

  Quantity assigned to polynomials over each finite variable set.

• variable_zero (variableCount : ℕ) (coordinate : Fin variableCount) : self.value variableCount (MvPolynomial.X coordinate) = 0

  A single formal variable has zero progress.

• add_substitution_le (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (left right : Fin variableCount) : self.value variableCount ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left + MvPolynomial.X right) MvPolynomial.X i) polynomial) ≤ self.value (variableCount + 1) polynomial + operationCost Arithmetic.Op.add

  Substituting the last variable by a sum obeys the addition charge.

• mul_substitution_le (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (left right : Fin variableCount) : self.value variableCount ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.X left * MvPolynomial.X right) MvPolynomial.X i) polynomial) ≤ self.value (variableCount + 1) polynomial + operationCost Arithmetic.Op.mul

  Substituting the last variable by a product obeys the multiplication charge.

• constant_substitution_le (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) R) (scalar : K) : self.value variableCount ((MvPolynomial.bind₁ fun (i : Fin (variableCount + 1)) => Fin.lastCases (MvPolynomial.C (constant scalar)) MvPolynomial.X i) polynomial) ≤ self.value (variableCount + 1) polynomial + operationCost (Arithmetic.Op.constant scalar)

  Substituting the last variable by a named constant obeys its operation charge.

theorem Algebraic.Fusion.Arithmetic.Progress.General.Measure.reverseSubstitution_le {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] {constant : K → R} {operationCost : OperationCost (Arithmetic.signature K)} (measure : Measure constant operationCost) (line : Line (Arithmetic.signature K) n g) (polynomial : MvPolynomial (Fin (n + g + 1)) R) : measure.value (n + g) ((lineReverseSubstitution constant line) polynomial) ≤ measure.value (n + g + 1) polynomial + operationCost line.op

One reverse gate substitution obeys the local progress estimate.

theorem Algebraic.Fusion.Arithmetic.Progress.General.Measure.expansionHom_le_cost {R : Type u_1} {K : Type u_2} {n g : ℕ} [CommSemiring R] {constant : K → R} {operationCost : OperationCost (Arithmetic.signature K)} (measure : Measure constant operationCost) (program : Program (Arithmetic.signature K) n g) (polynomial : MvPolynomial (Fin (n + g)) R) : measure.value n ((programExpansionHom constant program) polynomial) ≤ measure.value (n + g) polynomial + Program.cost operationCost program

Reverse substitution telescopes local progress across a whole program.

theorem Algebraic.Fusion.Arithmetic.Progress.General.Measure.expandedOutput_le_cost {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] {constant : K → R} {operationCost : OperationCost (Arithmetic.signature K)} (measure : Measure constant operationCost) (circuit : Circuit (Arithmetic.signature K) n 1) : measure.value n (circuitExpandedOutput constant circuit) ≤ circuit.cost operationCost

The measure of the expanded output is bounded by circuit cost.

theorem Algebraic.Fusion.Arithmetic.Progress.General.Measure.circuit_lowerBound {R : Type u_1} {K : Type u_2} {n : ℕ} [CommSemiring R] {constant : K → R} {operationCost : OperationCost (Arithmetic.signature K)} (measure : Measure constant operationCost) (target : MvPolynomial (Fin n) R) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (polynomialInterpretation constant (Fin n))) : measure.value n target ≤ circuit.cost operationCost

Any arithmetic circuit producing a target polynomial pays its progress measure.