Rank bounds for sums of dictionary terms

A linear feature whose dictionary values have bounded rank gives a lower bound on the total weighted dictionary cost. Each shared gate is charged once. Supplied inputs are permitted when their features vanish. The signature and its costs are re-exported from SumOfTerms.Basic.

Main results

• Cslib.Circuits.SumOfTerms.rank_trace_le: every wire's feature rank is bounded by program cost.

References

• Adapted from LowerBound/Fusion/SumOfTerms/Rank.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

theorem Cslib.Circuits.SumOfTerms.rank_trace_le {T : Type u_1} {K : Type u_2} {V : Type u_3} {A : Type u_4} {B : Type u_5} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {n g : ℕ} (p : Program (signature T) n g) (value : T → V) (feature : V →ₗ[K] A →ₗ[K] B) (weight : T → ℕ) (hterm : ∀ (t : T), (feature (value t)).rank ≤ ↑(weight t)) (input : Fin n → V) (hinput : ∀ (i : Fin n), feature (input i) = 0) (w : Wire n g) : (feature (p.trace (interpretation value) input w)).rank ≤ ↑(p.cost (dictionaryCost weight))

A rank budget for each dictionary term bounds every wire's feature rank. The span argument counts shared gates once, even when additions reuse them.