Minimum colour dimension and connection-rank growth

The total dimension of the reconstructed standard model is minimal among all mixed models of the parameter. Its value is the limit of the even roots of the actual connection ranks. The assembly is conditional on Deligne's theorem, discharged in RS/Summit.lean.

theorem RS.minimumColourDimension_le_of_represents {f : ClosedFragment → ℂ} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (hrep : h.Represents f) : minimumColourDimension f ≤ k + 2 * ℓ

A representing model bounds the minimum total colour dimension.

theorem RS.minimumColourDimension_attained {f : ClosedFragment → ℂ} (hf : IsMixedPartitionFunction f) : IsMixedPartitionFunctionTotalBounded f (minimumColourDimension f)

Every parameter admitting a mixed model admits one at the least total colour bound.

theorem RS.TotalBoundedMixedModel.dimension_eq_minimum {f : ClosedFragment → ℂ} (M : TotalBoundedMixedModel f (minimumColourDimension f)) : M.k + 2 * M.ℓ = minimumColourDimension f

A model at the least colour bound has exactly that total dimension, rather than merely a dimension bounded by it.

theorem RS.MixedFunctional.Represents.edgeRankBounded {f : ClosedFragment → ℂ} {k ℓ : ℕ} {h : MixedFunctional k ℓ} (hrep : h.Represents f) : EdgeRankBounded f (k + 2 * ℓ)

A represented parameter satisfies the rank bound with the representing model's exact total dimension.

theorem RS.stdModel_dimension_eq_minimum {R k ℓ : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e : stdSuperPair k ℓ ≅ strandImage f P) (h : MixedFunctional k ℓ) (hrep : h.Represents f.val) : k + 2 * ℓ = minimumColourDimension f.val

The standard model's dimension is the intrinsic minimum as soon as its graph evaluations agree with the parameter.

theorem RS.stdModel_connectionRank_growth {R k ℓ : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e : stdSuperPair k ℓ ≅ strandImage f P) (h : MixedFunctional k ℓ) (hrep : h.Represents f.val) : Filter.Tendsto (fun (n : ℕ) => ↑(connectionRank f.val (2 * n)) ^ (↑(2 * n))⁻¹) Filter.atTop (nhds ↑(k + 2 * ℓ))

The even roots of the connection ranks tend to the total dimension of the reconstructed standard model.

theorem RS.regts_sevenster_minimum_deligne_only (hDeligne : DeligneTheoremStatement) {R : ℕ} (f : EdgeRankParameter R) : IsMixedPartitionFunctionTotalBounded f.val (minimumColourDimension f.val)

Exponentially bounded connection rank admits a model attaining the minimum total colour dimension, conditional on Deligne alone.

theorem RS.regts_sevenster_rank_growth_deligne_only (hDeligne : DeligneTheoremStatement) {R : ℕ} (f : EdgeRankParameter R) : Filter.Tendsto (fun (n : ℕ) => ↑(connectionRank f.val (2 * n)) ^ (↑(2 * n))⁻¹) Filter.atTop (nhds ↑(minimumColourDimension f.val))

The even connection-rank growth rate exists and equals the minimum total colour dimension, conditional on Deligne alone.