Exact factorization of the crossing-root dimension product

Proved

Cloning.YoungDimensionRatio.dimensionRatio_factorization

by JWang226 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-analysismixed-state-cloning-v1weyl-dimension-product

Let $r,k$ be nonnegative integers with $r>0$ , let $N>0$ be real, and let $\mathrm{row}:\mathrm{Fin}(r)\to\mathbb R$ be arbitrary. For $g_{i,j}=r+j-i$ , define $D_{r,k}(\mathrm{row})=\prod_{i<r,j<k}(\mathrm{row}_i+g_{i,j})/g_{i,j}$ and $c_{r,k}=\prod_{i<r,j<k}1/(r g_{i,j})$ . Then

D_{r,k}(\mathrm{row})=c_{r,k}N^{rk}\prod_{i<r,j<k}\frac{r(\mathrm{row}_i+g_{i,j})}{N}.

This is an exact algebraic identity for the explicit product. Its identification with representation dimensions is a separate theorem.

This is supporting analytic material for the paper.

Withdrawn from active publication at the submitter’s request. No replacement is being published.

Preamble

import Definitions.Def_Cloning_YoungDimensionRatio
import Mathlib.Analysis.SpecialFunctions.Log.Summable
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

/-!
# Concrete asymptotics of the crossing-root Weyl dimension product

For an `r`-row label in ambient dimension `r+k`, the manuscript's explicit
dimension-ratio expression is the product of `(rowᵢ+j-i)/(j-i)` over crossing
roots. This file defines that actual finite product and derives its uniform
relative-error bound directly from the row lengths. No dimension-ratio
convergence or product approximation is assumed.

The identification of this explicit Weyl product with dimensions of the
particular representation spaces is a separate representation-theoretic
statement. This file proves the analytic input once that formula is used.
-/


open scoped BigOperators Topology
open Filter

open Cloning.YoungDimensionRatio

Formal statement

theorem Cloning.YoungDimensionRatio.dimensionRatio_factorization (r k : ℕ) (row : Fin r → ℝ) (N : ℝ)
    (hr : 0 < r) (hN : 0 < N) :
    dimensionRatio r k row = leadingConstant r k * N ^ (r * k) *
      ∏ a : Fin r × Fin k, ((r : ℝ) * (row a.1 + crossingGap a) / N) := by sorry

Source

https://github.com/JWang226/Cloning/blob/cb7b0df616294bd0729dd1ad693421739f01fd0b/formalization/Cloning/YoungDimensionRatio.lean#L60-L76

View graph