Lower bounds by parameterizing the original inputs #
Constructing the tuple (rho y, supplied (rho y)) and then applying a
conditional circuit computes the restricted target. The source tuple is
charged jointly, so any sharing in its implementation is retained.
theorem
Cslib.Circuits.Circuit.costComplexity_precomp_le_conditional_add
{σ : Signature}
{U : Type u_2}
{n m k d : ℕ}
(interpretation : Interpretation σ U)
(operationCost : Algebraic.OperationCost σ)
(target : Algebraic.Target U n m)
(supplied : Algebraic.Target U n k)
(map : Algebraic.Target U d n)
:
costComplexity interpretation operationCost (target ∘ map) ≤ conditionalCostComplexity interpretation operationCost target supplied + costComplexity interpretation operationCost fun (input : Fin d → U) => Fin.append (map input) (supplied (map input))
Build all restricted source values jointly, then run the conditional circuit.
theorem
Cslib.Circuits.Circuit.conditionalCostComplexity_lowerBound_of_precomp
{σ : Signature}
{U : Type u_2}
{n m k d : ℕ}
(interpretation : Interpretation σ U)
(operationCost : Algebraic.OperationCost σ)
(target : Algebraic.Target U n m)
(supplied : Algebraic.Target U n k)
(map : Algebraic.Target U d n)
(lower budget : ℕ)
(hard : ↑lower ≤ costComplexity interpretation operationCost (target ∘ map))
(cheap :
(costComplexity interpretation operationCost fun (input : Fin d → U) =>
Fin.append (map input) (supplied (map input))) ≤ ↑budget)
:
A hard restricted target and a cheap joint source tuple give a lower bound on conditional complexity. Natural subtraction truncates at zero.