Unital matrix representations have divisible block sizes

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.representation_block_divisibility

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

prove2quantum

Let $d\ge1$ and let $n_\mu\ge1$ be positive integers indexed by a finite set. If $\Phi:M_d(\mathbb C)\to\bigoplus_\mu M_{n_\mu}(\mathbb C)$ is a complex-linear star homomorphism preserving the identity, then

d\mid n_\mu\qquad\text{for every }\mu.

The target index set may be empty, in which case the conclusion is vacuous. Unitality is essential to the representation dimension constraint.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P96

Formal statement

noncomputable section

open scoped TensorProduct Kronecker BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P96

open QAlgorithms.Papers.Independent.Information100.P26 (Mat)

/-- Proposition 12, PDF p.18: unital representation block sizes are divisible by `d`. -/
theorem representation_block_divisibility (d : ℕ) (hd : 0 < d)
    (count : ℕ) (n : Fin count → ℕ) (hn : ∀ i, 0 < n i)
    (Phi : Mat d →⋆ₐ[ℂ] ((i : Fin count) → Mat (n i))) :
    ∀ i, d ∣ n i := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 18, Proposition 12: divisibility of dimensions of matrix representations

Read-back

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

For every natural number $d>0$ , every natural number $c$ , every family of positive natural numbers $(n_i)_{i<c}$ , and every unital complex star algebra homomorphism

\Phi:M_d(\mathbb C)\longrightarrow\prod_{i<c}M_{n_i}(\mathbb C),

the integer $d$ divides $n_i$ for every $i<c$ . Here $M_s(\mathbb C)$ denotes the algebra of $s\times s$ complex matrices, and $\Phi$ preserves addition, multiplication, the identity, complex scalars, and conjugate transpose; injectivity is not assumed. The case $c=0$ is included, and its conclusion has no indices to check.

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