Uniform relative error bound for the crossing-root dimension product

Proved

Cloning.YoungDimensionRatio.dimensionRatio_relative_error

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$ and $\delta$ be real, and let $\mathrm{row}:\mathrm{Fin}(r)\to\mathbb R$ satisfy $|\mathrm{row}_i/N-1/r|\le\delta$ for every $i<r$ . Define $D_{r,k}(\mathrm{row})=\prod_{i<r,j<k}(\mathrm{row}_i+r+j-i)/(r+j-i)$ and $c_{r,k}=\prod_{i<r,j<k}1/[r(r+j-i)]$ . Then

\left|\frac{D_{r,k}(\mathrm{row})}{c_{r,k}N^{rk}}-1\right|\le\exp\!\left(rk\left[r\delta+\frac{r(r+k)}{N}\right]\right)-1.

This bounds the explicit analytic product; no representation-dimension identification or cloning optimality is assumed or concluded.

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_relative_error (r k : ℕ) (row : Fin r → ℝ) (N δ : ℝ)
    (hr : 0 < r) (hN : 0 < N)
    (hclose : ∀ i, |row i / N - 1 / (r : ℝ)| ≤ δ) :
    |dimensionRatio r k row / (leadingConstant r k * N ^ (r * k)) - 1| ≤
      Real.exp ((r * k : ℕ) * ((r : ℝ) * δ + (r : ℝ) * ((r : ℝ) + k) / N)) - 1 := by sorry

Source

https://github.com/JWang226/Cloning/blob/cb7b0df616294bd0729dd1ad693421739f01fd0b/formalization/Cloning/YoungDimensionRatio.lean#L102-L126

View graph