Prove2Me

p. 2 — the unitary product operators T\mathcal T form a compact group

Proved
EastinKnill.Transversal.productUnitaries_compact_subgroup

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

compact-groupeastin-knillp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1tensor-productunitary-group

Let Q\mathcal Q be a composite system of finitely many subsystems of dimensions djd_j. The set of unitary product operators

T={⨂jUj:Uj∈U(dj)}\mathcal T = \Big\{ \bigotimes_j U_j : U_j \in \mathcal U(d_j) \Big\}

is a subgroup of the unitary group of Q\mathcal Q, and it is compact.

Being the image of the direct product of the compact groups U(dj)\mathcal U(d_j), T\mathcal T is the compact Lie group in which the logical product unitaries live; its compactness is what makes the set of logically distinct transversal actions finite.

Formalization Note "Compact Lie group" is stated as "compact subgroup" of Matrix.unitaryGroup; the Lie structure is not formalized.

Preamble
import Mathlib
import Definitions.Def_EastinKnill_Transversal_Setting

open scoped Matrix
Formal statement
namespace EastinKnill.Transversal

theorem productUnitaries_compact_subgroup {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ j, Fintype (α j)]
    [∀ j, DecidableEq (α j)] :
    ∃ T : Subgroup (Matrix.unitaryGroup (∀ j, α j) ℂ),
      (T : Set (Matrix.unitaryGroup (∀ j, α j) ℂ)) = productUnitaries α ∧
      IsCompact (T : Set (Matrix.unitaryGroup (∀ j, α j) ℂ)) := by sorry

end EastinKnill.Transversal
Source
Eastin & Knill, Restrictions on Transversal Encoded Quantum Gate Sets, arXiv:0811.4262v2, p. 2, paragraph defining 𝒯
Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph