Real dimensions of tensor-factor quotients

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.tensor_quotient_dimensions

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $0\le\mu\le m$ be integers. Write $\mathfrak{su}(d)$ for the real vector space of skew-Hermitian traceless complex $d\times d$ matrices. For $a=2^{m-\mu}$ and $b=2^\mu$ , the one-factor subgroup has tangent image $\{A\otimes I_b:A\in\mathfrak{su}(a)\}$ ; the two-factor subgroup has tangent image consisting of sums $A\otimes I_b+I_a\otimes B$ . The real dimensions are

\dim SU(2^m)=4^m-1,

\dim\frac{SU(2^m)}{SU(a)\otimes I_b}=4^{m-\mu}(4^\mu-1),

\dim\frac{SU(2^m)}{SU(a)\otimes SU(b)}=(4^{m-\mu}-1)(4^\mu-1).

These count actual real tangent dimensions. Finite central kernels of the tensor-product subgroup do not alter these dimensions. The formal statement uses the corresponding quotient vector spaces, with subgroup images defined independently of the displayed answers.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.4, Eqs. (4)-(6): real group and homogeneous-space dimensions,
computed from their tangent spaces rather than defined by the answer. -/
theorem tensor_quotient_dimensions (m mu : ℕ) (hmu : mu ≤ m) :
    Module.finrank ℝ (specialUnitaryTangent (Fin (2 ^ m))) = 4 ^ m - 1 ∧
    Module.finrank ℝ (OneFactorQuotient (2 ^ (m - mu)) (2 ^ mu)) =
      4 ^ (m - mu) * (4 ^ mu - 1) ∧
    Module.finrank ℝ (TwoFactorQuotient (2 ^ (m - mu)) (2 ^ mu)) =
      (4 ^ (m - mu) - 1) * (4 ^ mu - 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 4, Real dimensions of block groups and tensor-factor quotients, Eqs. (4)–(6)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For natural numbers $m,\mu$ satisfying $\mu\le m$ , put $a=2^{m-\mu}$ and $b=2^\mu$ . For any finite index set $J$ , write $S_J=\{X\in\mathbb C^{J\times J}:X^\ast=-X,\ \operatorname{tr}(X)=0\}$ , regarded as a real vector space, and write $S_d$ when $J=\{0,\ldots,d-1\}$ . On the product index set $J=\{0,\ldots,a-1\}\times\{0,\ldots,b-1\}$ , let $L=\operatorname{span}_{\mathbb R}\{A\otimes I_b:A\in S_a\}$ and $R=\operatorname{span}_{\mathbb R}\{I_a\otimes B:B\in S_b\}$ , where $\ast$ is conjugate transpose and $\otimes$ is the Kronecker product. All three real-dimension equalities hold:

\dim_{\mathbb R}S_{2^m}=4^m-1, \qquad \dim_{\mathbb R}\bigl(S_J/(S_J\cap L)\bigr) =4^{m-\mu}(4^\mu-1), \qquad \dim_{\mathbb R}\bigl(S_J/(S_J\cap(L+R))\bigr) =(4^{m-\mu}-1)(4^\mu-1).

The arithmetic on the right is natural-number arithmetic, with subtraction truncated at zero; the hypothesis ensures $m-\mu$ is ordinary nonnegative subtraction. The endpoints $\mu=0$ and $\mu=m$ are included: for $\mu=0$ both quotient dimensions are zero, while for $\mu=m$ they are respectively $4^m-1$ and zero. In particular, $m=0$ forces $\mu=0$ and all three dimensions are zero.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph