Term-dependent weighted rank certificates

The ordinary sum-of-terms rank certificate uses one uniform rank bound and counts dictionary terms. This module allows each dictionary term to carry its own natural weight. If the feature rank of a term is at most that weight, then target rank lower-bounds the circuit's exact term-dependent cost.

This is the appropriate interface for supported matrix blocks, rectangles of different side lengths, and heterogeneous tensor pieces.

structure Algebraic.Fusion.SumOfTerms.WeightedRank.Certificate {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) (termWeight : T → ℕ) (problem : Problem V) : Type (max (max v x) y)

Rank certificate with a term-specific natural rank budget.

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

  Linear feature whose rank measures the target.

• targetRank : ℕ

  Natural lower bound on target feature rank.

• 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 ≤ ↑(termWeight term)

  Every dictionary term fits within its own charged weight.

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

  The target realizes the claimed rank.

theorem Algebraic.Fusion.SumOfTerms.WeightedRank.Certificate.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} {termWeight : T → ℕ} {problem : Problem V} (certificate : Certificate termValue termWeight 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 target feature is spanned by the features of dictionary-term occurrences in any Fusion cover.

theorem Algebraic.Fusion.SumOfTerms.WeightedRank.Certificate.target_rank_le_termWeights {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} {termWeight : T → ℕ} {problem : Problem V} (certificate : Certificate termValue termWeight problem) (cover : Cover (spanModel termValue problem)) : (certificate.feature problem.target).rank ≤ ∑ index : Fin (terms cover.atoms).length, ↑(termWeight ((terms cover.atoms).get index))

Target feature rank is at most the sum of the weights of dictionary-term occurrences in a cover.

theorem Algebraic.Fusion.SumOfTerms.WeightedRank.Certificate.targetRank_le_termWeights {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} {termWeight : T → ℕ} {problem : Problem V} (certificate : Certificate termValue termWeight problem) (cover : Cover (spanModel termValue problem)) : certificate.targetRank ≤ (List.map termWeight (terms cover.atoms)).sum

Natural-number weighted cover inequality.

theorem Algebraic.Fusion.SumOfTerms.WeightedRank.Certificate.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} {termWeight : T → ℕ} {problem : Problem V} (certificate : Certificate termValue termWeight problem) (circuit : Circuit (SumOfTerms.signature T) problem.inputCount 1) (constructs : problem.Constructs circuit (SumOfTerms.interpretation termValue)) : certificate.targetRank ≤ circuit.cost (SumOfTerms.dictionaryCost termWeight)

A weighted rank certificate lower-bounds exact term-dependent circuit cost.