Combining arithmetic gate lower bounds

Arithmetic Fusion arguments often expose independent certificates for addition and multiplication gates. This module supplies the small reusable cost algebra needed to combine such certificates into one lower bound for the total number of nonconstant arithmetic gates.

The underlying statement is signature-generic: cost is additive in the operation-cost function. The arithmetic specialization then observes that gateCost is the pointwise sum of additionCost and multiplicationCost.

theorem Cslib.Circuits.Program.cost_add {sigma : Signature} {n g : ℕ} (program : Program sigma n g) (left right : Algebraic.OperationCost sigma) : cost (fun (op : sigma.Op) => left op + right op) program = cost left program + cost right program

Program cost is additive in the operation-cost function.

theorem Cslib.Circuits.Circuit.cost_add {sigma : Signature} {n m : ℕ} (circuit : Circuit sigma n m) (left right : Algebraic.OperationCost sigma) : (circuit.cost fun (op : sigma.Op) => left op + right op) = circuit.cost left + circuit.cost right

Circuit cost is additive in the operation-cost function.

theorem Cslib.Circuits.Program.cost_mono {sigma : Signature} {n g : ℕ} (program : Program sigma n g) (left right : Algebraic.OperationCost sigma) (bounded : ∀ (op : sigma.Op), left op ≤ right op) : cost left program ≤ cost right program

Pointwise domination of operation costs implies domination of program costs.

theorem Cslib.Circuits.Circuit.cost_mono {sigma : Signature} {n m : ℕ} (circuit : Circuit sigma n m) (left right : Algebraic.OperationCost sigma) (bounded : ∀ (op : sigma.Op), left op ≤ right op) : circuit.cost left ≤ circuit.cost right

Pointwise domination of operation costs implies domination of circuit costs.

theorem Algebraic.Fusion.Arithmetic.Combined.gateCost_eq_additionCost_add_multiplicationCost (K : Type u) : Arithmetic.gateCost = fun (op : (Arithmetic.signature K).Op) => Arithmetic.additionCost op + Arithmetic.multiplicationCost op

Standard arithmetic gate cost is the pointwise sum of the addition-only and multiplication-only costs.

theorem Algebraic.Fusion.Arithmetic.Combined.circuit_gateCost_eq_additionCost_add_multiplicationCost {K : Type u_1} {n m : ℕ} (circuit : Circuit (Arithmetic.signature K) n m) : circuit.cost Arithmetic.gateCost = circuit.cost Arithmetic.additionCost + circuit.cost Arithmetic.multiplicationCost

The total nonconstant arithmetic-gate cost is exactly additive complexity plus multiplicative complexity.

theorem Algebraic.Fusion.Arithmetic.Combined.circuit_additionCost_le_gateCost {K : Type u_1} {n m : ℕ} (circuit : Circuit (Arithmetic.signature K) n m) : circuit.cost Arithmetic.additionCost ≤ circuit.cost Arithmetic.gateCost

Addition-only cost is bounded by total arithmetic-gate cost.

theorem Algebraic.Fusion.Arithmetic.Combined.circuit_multiplicationCost_le_gateCost {K : Type u_1} {n m : ℕ} (circuit : Circuit (Arithmetic.signature K) n m) : circuit.cost Arithmetic.multiplicationCost ≤ circuit.cost Arithmetic.gateCost

Multiplication-only cost is bounded by total arithmetic-gate cost.

theorem Algebraic.Fusion.Arithmetic.Combined.circuit_gateCost_le_size {K : Type u_1} {n m : ℕ} (circuit : Circuit (Arithmetic.signature K) n m) : circuit.cost Arithmetic.gateCost ≤ circuit.size

Total nonconstant arithmetic-gate cost is bounded by circuit size; constant gates account for the possible gap.

theorem Algebraic.Fusion.Arithmetic.Combined.circuit_gate_lowerBound_of_components {K : Type u_1} {n m : ℕ} (circuit : Circuit (Arithmetic.signature K) n m) (additionBound multiplicationBound : ℕ) (additionLowerBound : additionBound ≤ circuit.cost Arithmetic.additionCost) (multiplicationLowerBound : multiplicationBound ≤ circuit.cost Arithmetic.multiplicationCost) : additionBound + multiplicationBound ≤ circuit.cost Arithmetic.gateCost

Independent lower bounds for additions and multiplications add to a lower bound for all nonconstant arithmetic gates.