Documentation

LeanPool.RegtsSevenster.RS.Classical.Interfaces.TotalDimension

The total dimension bound for the standard model #

The fibre action on colour words factors through the skein endomorphism algebra, whose dimension is at most R ^ (2 * n). The monomial word action has polynomial commutant dimension. Native block faithfulness therefore bounds (k + 2 * ℓ) ^ n by R ^ n times a fixed polynomial, forcing k + 2 * ℓ ≤ R.

theorem RS.stdModel_pow_le_connectionRank {R k ℓ : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e : stdSuperPair k ℓ ≅ strandImage f P) (n : ℕ) :
(k + 2 * ℓ) ^ (2 * n) ≤ connectionRank f.val (2 * n) * (n + 1) ^ (2 * (k + 2 * ℓ) ^ 2)

At every tensor power the standard model's squared dimension is bounded by connection rank times a fixed polynomial.

theorem RS.stdModel_total_dimension_le_of_rank_bound {R k ℓ B : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e : stdSuperPair k ℓ ≅ strandImage f P) (hB : EdgeRankBounded f.val B) :
k + 2 * ℓ ≤ B

The standard model's total dimension is bounded by every edge-rank base for the same parameter.

theorem RS.stdModel_total_dimension_le {R k ℓ : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e : stdSuperPair k ℓ ≅ strandImage f P) :
k + 2 * ℓ ≤ R

The standard model supplied by any Deligne package has total dimension at most the original edge-rank base.