Lemma 1, p. 2 — the logical unitary operators form a group

Proved

EastinKnill.Transversal.lemma_1

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

eastin-knillp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-error-correctionunitary-group

Let $P$ be the projector onto the code space of a quantum code on a finite-dimensional system. A unitary $U$ is logical if $(I-P)UP = 0$ (Eq. (1)). Then the set

\mathcal L = \{\, U \text{ unitary} : (I-P)\,U\,P = 0 \,\}

is a subgroup of the unitary group: it contains the identity and is closed under products and inverses.

This is the first structural fact behind the Eastin–Knill theorem: composing logical gates produces nothing beyond the group they already form.

Formalization Note The statement asserts the existence of a subgroup of Matrix.unitaryGroup whose carrier is exactly $\mathcal L$ .

Preamble

import Mathlib
import Definitions.Def_EastinKnill_Transversal_Setting

open scoped Matrix

Formal statement

namespace EastinKnill.Transversal

theorem lemma_1 {n : Type*} [Fintype n] [DecidableEq n] (P : Matrix n n ℂ)
    (hP : IsCodeProjector P) :
    ∃ L : Subgroup (Matrix.unitaryGroup n ℂ),
      (L : Set (Matrix.unitaryGroup n ℂ)) =
        {U : Matrix.unitaryGroup n ℂ | IsLogical P (U : Matrix n n ℂ)} := by sorry

end EastinKnill.Transversal

Source

Eastin & Knill, Restrictions on Transversal Encoded Quantum Gate Sets, arXiv:0811.4262v2, p. 2, Lemma 1

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