Uniform error bound for one rescaled crossing-root factor

Proved

Cloning.YoungDimensionRatio.rescaled_factor_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$ . For every $i<r,j<k$ , with $g_{i,j}=r+j-i$ ,

\left|\frac{r(\mathrm{row}_i+g_{i,j})}{N}-1\right|\le r\delta+\frac{r(r+k)}{N}.

The estimate separates row-proportion error from the finite crossing-root gap.

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.rescaled_factor_error (r k : ℕ) (row : Fin r → ℝ) (N δ : ℝ)
    (hr : 0 < r) (hN : 0 < N)
    (hclose : ∀ i, |row i / N - 1 / (r : ℝ)| ≤ δ) (a : Fin r × Fin k) :
    |(r : ℝ) * (row a.1 + crossingGap a) / N - 1| ≤
      (r : ℝ) * δ + (r : ℝ) * ((r : ℝ) + k) / N := by sorry

Source

https://github.com/JWang226/Cloning/blob/cb7b0df616294bd0729dd1ad693421739f01fd0b/formalization/Cloning/YoungDimensionRatio.lean#L78-L100

View graph