Rank bounds from arithmetic interaction spans

When an interaction certificate takes values in a space of linear maps, rank turns its span theorem into a multiplication lower bound. If every product interaction has rank at most r, a target feature of rank at least R requires at least ceil(R / r) multiplication gates.

This result is agnostic about the source of the feature. Matrix flattenings, shifted Hessians, and derivative spaces can share the same circuit argument.

structure Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] (constant : C → U) (problem : Problem U) extends Algebraic.Fusion.Arithmetic.Interaction.Certificate constant problem : Type (max (max w x) y)

An interaction certificate equipped with target and local rank bounds.

• feature : U → A →ₗ[K] B
• interaction : U → U → A →ₗ[K] B
• input_zero (input : Fin problem.inputCount) : self.feature (problem.inputs input) = 0
• feature_add (left right : U) : self.feature (left + right) = self.feature left + self.feature right
• constant_zero (scalar : C) : self.feature (constant scalar) = 0
• feature_mul (left right : U) : ∃ (leftScalar : K) (rightScalar : K), self.feature (left * right) = leftScalar • self.feature left + rightScalar • self.feature right + self.interaction left right
• targetRank : ℕ

  Natural lower bound on the target feature rank.

• interactionRank : ℕ

  Natural upper bound on each multiplication interaction rank.

• interaction_rank_le (left right : U) : (self.interaction left right).rank ≤ ↑self.interactionRank

  Every multiplication creates a feature interaction of bounded rank.

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

  The target realizes the claimed rank.

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.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.

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.linearMap_rank_le_sum_of_mem_span {K : Type u} {A : Type v} {B : Type w} [Field K] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {ι : Type z} [Fintype ι] (target : A →ₗ[K] B) (family : ι → A →ₗ[K] B) (budget : ι → ℕ) (targetMem : target ∈ Submodule.span K (Set.range family)) (localBound : ∀ (index : ι), (family index).rank ≤ ↑(budget index)) : target.rank ≤ ∑ index : ι, ↑(budget index)

Compatibility name for LinearMap.rank_le_sum_of_mem_span.

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate.rank_le_of_mem_interactions {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atoms : List (Atom (Arithmetic.signature C) U)) (interaction : A →ₗ[K] B) (present : interaction ∈ interactions certificate.toCertificate atoms) : interaction.rank ≤ ↑certificate.interactionRank

Every interaction retained from an atom list satisfies the certificate's local rank bound.

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate.target_rank_le_interactions {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (cover : Cover (model certificate.toCertificate)) : (certificate.feature problem.target).rank ≤ ↑(interactions certificate.toCertificate cover.atoms).length * ↑certificate.interactionRank

Rank of the target feature is at most the number of interactions times their individual rank bound.

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate.targetRank_le_mul_coverCost {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (cover : Cover (model certificate.toCertificate)) : certificate.targetRank ≤ cover.cost * certificate.interactionRank

Natural-number form of the rank-versus-interaction inequality.

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate.ceilDiv_targetRank_le_coverCost {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (positive : 0 < certificate.interactionRank) (cover : Cover (model certificate.toCertificate)) : certificate.targetRank ⌈/⌉ certificate.interactionRank ≤ cover.cost

Dividing by a positive local interaction-rank bound gives a cover lower bound.

theorem Algebraic.Fusion.Arithmetic.Interaction.Rank.Certificate.circuit_lowerBound {K : Type u} {C : Type v} {U : Type w} {A : Type x} {B : Type y} [Field K] [Add U] [Mul U] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (positive : 0 < certificate.interactionRank) (circuit : Circuit (Arithmetic.signature C) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation constant)) : certificate.targetRank ⌈/⌉ certificate.interactionRank ≤ circuit.cost Arithmetic.multiplicationCost

Interaction rank gives a multiplication lower bound for every arithmetic circuit constructing the target.