Reverse-substitution progress measures for constant-free arithmetic circuits

This module preserves the original constant-free API as a compatibility layer over Progress.General. The generic module contains the circuit-DAG telescoping argument; here the named-constant alphabet is specialized to PEmpty.

Keeping the specialization separate lets existing lower bounds continue to construct the four-field constant-free Measure, while new developments may use General.Measure and supply a local law for named constants.

def Algebraic.Fusion.Arithmetic.Progress.noConstants : PEmpty.{u_1} → ℕ

The unique interpretation of an empty constant alphabet.

Equations

• Algebraic.Fusion.Arithmetic.Progress.noConstants = PEmpty.elim

noncomputable def Algebraic.Fusion.Arithmetic.Progress.polynomialInterpretation (V : Type u) : Interpretation (Arithmetic.signature PEmpty.{u_1 + 1}) (MvPolynomial V ℕ)

Arithmetic interpretation on polynomials with no named constants.

Equations

• Algebraic.Fusion.Arithmetic.Progress.polynomialInterpretation V = Algebraic.Fusion.Arithmetic.Progress.General.polynomialInterpretation Algebraic.Fusion.Arithmetic.Progress.noConstants V

noncomputable def Algebraic.Fusion.Arithmetic.Progress.lineFormalResult {n g : ℕ} (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) : MvPolynomial (Fin (n + g)) ℕ

Formal polynomial computed by one constant-free arithmetic line.

Equations

• Algebraic.Fusion.Arithmetic.Progress.lineFormalResult line = Algebraic.Fusion.Arithmetic.Progress.General.lineFormalResult Algebraic.Fusion.Arithmetic.Progress.noConstants line

noncomputable def Algebraic.Fusion.Arithmetic.Progress.lineReverseSubstitution {n g : ℕ} (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) : MvPolynomial (Fin (n + g + 1)) ℕ →ₐ[ℕ] MvPolynomial (Fin (n + g)) ℕ

Eliminate the newest gate-variable by reverse substitution.

Equations

• Algebraic.Fusion.Arithmetic.Progress.lineReverseSubstitution line = Algebraic.Fusion.Arithmetic.Progress.General.lineReverseSubstitution Algebraic.Fusion.Arithmetic.Progress.noConstants line

theorem Algebraic.Fusion.Arithmetic.Progress.lineReverseSubstitution_X_last {n g : ℕ} (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) : (lineReverseSubstitution line) (MvPolynomial.X (Fin.last (n.add g))) = lineFormalResult line

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.lineReverseSubstitution_X_castSucc {n g : ℕ} (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) (wire : Wire n g) : (lineReverseSubstitution line) (MvPolynomial.X wire.castSucc.index) = MvPolynomial.X wire.index

noncomputable def Algebraic.Fusion.Arithmetic.Progress.programExpansionHom {n g : ℕ} (program : Program (Arithmetic.signature PEmpty.{u_1 + 1}) n g) : MvPolynomial (Fin (n + g)) ℕ →ₐ[ℕ] MvPolynomial (Fin n) ℕ

Expand all formal gate-variables into input variables.

Equations

• Algebraic.Fusion.Arithmetic.Progress.programExpansionHom program = Algebraic.Fusion.Arithmetic.Progress.General.programExpansionHom Algebraic.Fusion.Arithmetic.Progress.noConstants program

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.programExpansionHom_empty {n : ℕ} : programExpansionHom Program.empty = AlgHom.id ℕ (MvPolynomial (Fin (n + 0)) ℕ)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.programExpansionHom_gate {n g : ℕ} (program : Program (Arithmetic.signature PEmpty.{u_1 + 1}) n g) (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) : programExpansionHom (program.gate line) = (programExpansionHom program).comp (lineReverseSubstitution line)

theorem Algebraic.Fusion.Arithmetic.Progress.programExpansionHom_X {n g : ℕ} (program : Program (Arithmetic.signature PEmpty.{u_1 + 1}) n g) (wire : Wire n g) : (programExpansionHom program) (MvPolynomial.X wire.index) = program.trace (polynomialInterpretation (Fin n)) MvPolynomial.X wire

Expanding a wire-variable recovers the polynomial on that wire.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.circuitFormalOutput {n : ℕ} (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) : MvPolynomial (Fin (n + circuit.size)) ℕ

The formal output variable of a single-output circuit.

Equations

• Algebraic.Fusion.Arithmetic.Progress.circuitFormalOutput circuit = Algebraic.Fusion.Arithmetic.Progress.General.circuitFormalOutput circuit

noncomputable def Algebraic.Fusion.Arithmetic.Progress.circuitExpandedOutput {n : ℕ} (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) : MvPolynomial (Fin n) ℕ

Polynomial obtained after eliminating every gate-variable.

Equations

• Algebraic.Fusion.Arithmetic.Progress.circuitExpandedOutput circuit = Algebraic.Fusion.Arithmetic.Progress.General.circuitExpandedOutput Algebraic.Fusion.Arithmetic.Progress.noConstants circuit

theorem Algebraic.Fusion.Arithmetic.Progress.circuitExpandedOutput_eq_eval {n : ℕ} (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) : circuitExpandedOutput circuit = circuit.eval (polynomialInterpretation (Fin n)) MvPolynomial.X 0

Reverse substitution agrees with ordinary circuit evaluation.

structure Algebraic.Fusion.Arithmetic.Progress.Measure (operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})) : Type

The constant-free progress-measure interface retained for compatibility.

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

  Quantity assigned to polynomials over each finite variable set.

• variable_zero (variableCount : ℕ) (coordinate : Fin variableCount) : self.value variableCount (MvPolynomial.X coordinate) = 0
• add_substitution_le (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (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
• mul_substitution_le (variableCount : ℕ) (polynomial : MvPolynomial (Fin (variableCount + 1)) ℕ) (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

def Algebraic.Fusion.Arithmetic.Progress.Measure.toGeneral {operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})} (measure : Measure operationCost) : General.Measure noConstants operationCost

Extend a constant-free measure across the empty constant alphabet.

Equations

• measure.toGeneral = { value := measure.value, variable_zero := ⋯, add_substitution_le := ⋯, mul_substitution_le := ⋯, constant_substitution_le := ⋯ }

theorem Algebraic.Fusion.Arithmetic.Progress.Measure.reverseSubstitution_le {n g : ℕ} {operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})} (measure : Measure operationCost) (line : Line (Arithmetic.signature PEmpty.{u_1 + 1}) n g) (polynomial : MvPolynomial (Fin (n + g + 1)) ℕ) : measure.value (n + g) ((lineReverseSubstitution 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.Measure.expansionHom_le_cost {n g : ℕ} {operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})} (measure : Measure operationCost) (program : Program (Arithmetic.signature PEmpty.{u_1 + 1}) n g) (polynomial : MvPolynomial (Fin (n + g)) ℕ) : measure.value n ((programExpansionHom program) polynomial) ≤ measure.value (n + g) polynomial + Program.cost operationCost program

Local estimates telescope across the circuit DAG.

theorem Algebraic.Fusion.Arithmetic.Progress.Measure.expandedOutput_le_cost {n : ℕ} {operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})} (measure : Measure operationCost) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) : measure.value n (circuitExpandedOutput circuit) ≤ circuit.cost operationCost

The expanded output's measure is bounded by circuit cost.

theorem Algebraic.Fusion.Arithmetic.Progress.Measure.circuit_lowerBound {n : ℕ} {operationCost : OperationCost (Arithmetic.signature PEmpty.{u_1 + 1})} (measure : Measure operationCost) (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))) : measure.value n target ≤ circuit.cost operationCost

Every constant-free arithmetic circuit computing target pays its progress measure.