Rank certificates for sum-of-terms circuits

A catalecticant, partial-derivative matrix, tensor flattening, or evaluation matrix is a linear map from semantic values to linear maps. Rank is subadditive, so if every allowed term has rank at most r and the target has rank at least R, at least ceil(R / r) term gates are necessary.

This file proves that statement once for the fusion span model. Applications only supply the feature map and the two local rank estimates.

structure Algebraic.Fusion.SumOfTerms.RankCertificate {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] (termValue : T → V) (problem : Problem V) : Type (max (max v x) y)

A linear-map rank certificate for one sum-of-terms problem.

• feature : V →ₗ[K] A →ₗ[K] B

  Linear feature whose rank measures the target.

• targetRank : ℕ

  Natural lower bound on the feature rank of the target.

• termRank : ℕ

  Natural upper bound on the feature rank of each dictionary term.

• input_zero (input : Fin problem.inputCount) : self.feature (problem.inputs input) = 0

  Free inputs contribute no feature rank.

• term_rank_le (term : T) : (self.feature (termValue term)).rank ≤ ↑self.termRank

  Every permitted dictionary term has bounded feature rank.

• target_rank_ge : ↑self.targetRank ≤ (self.feature problem.target).rank

  The target realizes the claimed rank.

theorem Algebraic.Fusion.SumOfTerms.RankCertificate.targetFeature_mem_termSpan {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {termValue : T → V} {problem : Problem V} (certificate : RankCertificate termValue problem) (cover : Cover (spanModel termValue problem)) : certificate.feature problem.target ∈ Submodule.span K (Set.range fun (index : Fin (terms cover.atoms).length) => certificate.feature (termValue ((terms cover.atoms).get index)))

The feature of the target lies in the span of the features of the term atoms in a cover.

@[deprecated LinearMap.rank_smul_le (since := "2026-09-15")]

theorem Algebraic.Fusion.SumOfTerms.linearMap_rank_smul_le {K : Type u} {A : Type v} {B : Type w} [Field K] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] (scalar : K) (map : A →ₗ[K] B) : (scalar • map).rank ≤ map.rank

Compatibility name for LinearMap.rank_smul_le.

theorem Algebraic.Fusion.SumOfTerms.RankCertificate.target_rank_le_terms {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {termValue : T → V} {problem : Problem V} (certificate : RankCertificate termValue problem) (cover : Cover (spanModel termValue problem)) : (certificate.feature problem.target).rank ≤ ↑(terms cover.atoms).length * ↑certificate.termRank

The feature rank of the target is at most the number of terms times their individual rank bound.

theorem Algebraic.Fusion.SumOfTerms.RankCertificate.targetRank_le_mul_coverCost {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {termValue : T → V} {problem : Problem V} (certificate : RankCertificate termValue problem) (cover : Cover (spanModel termValue problem)) : certificate.targetRank ≤ cover.cost * certificate.termRank

A rank certificate gives the natural-number cover inequality targetRank ≤ cost * termRank.

theorem Algebraic.Fusion.SumOfTerms.RankCertificate.ceilDiv_targetRank_le_coverCost {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {termValue : T → V} {problem : Problem V} (certificate : RankCertificate termValue problem) (positive : 0 < certificate.termRank) (cover : Cover (spanModel termValue problem)) : certificate.targetRank ⌈/⌉ certificate.termRank ≤ cover.cost

Dividing by a positive per-term rank gives a cover-cost lower bound.

theorem Algebraic.Fusion.SumOfTerms.RankCertificate.circuit_lowerBound {K : Type u} {V : Type v} {T : Type w} {A : Type x} {B : Type y} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {termValue : T → V} {problem : Problem V} (certificate : RankCertificate termValue problem) (positive : 0 < certificate.termRank) (circuit : Circuit (SumOfTerms.signature T) problem.inputCount 1) (constructs : problem.Constructs circuit (SumOfTerms.interpretation termValue)) : certificate.targetRank ⌈/⌉ certificate.termRank ≤ circuit.cost SumOfTerms.termCost

Rank/partial-derivative lower bound transferred to sum-of-terms circuits.