§V B: required elementary operations and free-unitary symmetry

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.resource_operations

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

prove2quantum

Suppose all system and sample registers carry the same unitary group representation $R(g)$ or the same intrinsic Hermitian Hamiltonian $H$ , while ancillary controls carry the trivial representation or zero Hamiltonian. Let $S^{cc}$ be the full-register SWAP controlled by two ancillary qubits. Then

[S^{cc},R(g)\otimes R(g)\otimes I_{\rm anc}]=0,\qquad[S^{cc},(H\otimes I+I\otimes H)\otimes I_{\rm anc}]=0.

Ancillary unitaries commute with the extended symmetry action, and every ancillary density is invariant under the trivial ancillary symmetry. Thus the required register operations are symmetric or energy conserving under the stated extension. This operational observation does not assert that pure zero-Hamiltonian states are thermodynamically free, nor does it supply a symmetry-sector or Lie-algebra decomposition.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF p.11, Section V B: all required full-register SWAPs and ancillary unitaries
commute with identical on-site symmetry actions or the total intrinsic Hamiltonian.
This asserts no thermodynamic freeness for arbitrary pure auxiliary states. -/
theorem resource_operations {G : Type*} [Group G] (R : G →* Matrix.unitaryGroup I ℂ)
    (H : Matrix I I ℂ) (hH : H.IsHermitian) :
    (∀ g : G, doubleControlledSwap * Matrix.kronecker
      (Matrix.kronecker (R g : Matrix I I ℂ) (R g : Matrix I I ℂ)) (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) =
      Matrix.kronecker (Matrix.kronecker (R g : Matrix I I ℂ) (R g : Matrix I I ℂ))
        (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) * doubleControlledSwap) ∧
    (doubleControlledSwap * Matrix.kronecker
      (Matrix.kronecker H (1 : Matrix I I ℂ) + Matrix.kronecker (1 : Matrix I I ℂ) H) (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) =
      Matrix.kronecker (Matrix.kronecker H (1 : Matrix I I ℂ) + Matrix.kronecker (1 : Matrix I I ℂ) H)
        (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) * doubleControlledSwap) ∧
    (∀ (V : Matrix.unitaryGroup (Bool × Bool) ℂ) (g : G),
      Matrix.kronecker (1 : Matrix (I × I) (I × I) ℂ) (V : Matrix (Bool × Bool) (Bool × Bool) ℂ) *
        Matrix.kronecker (Matrix.kronecker (R g : Matrix I I ℂ) (R g : Matrix I I ℂ)) (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) =
      Matrix.kronecker (Matrix.kronecker (R g : Matrix I I ℂ) (R g : Matrix I I ℂ)) (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) *
        Matrix.kronecker (1 : Matrix (I × I) (I × I) ℂ) (V : Matrix (Bool × Bool) (Bool × Bool) ℂ)) ∧
    (∀ V : Matrix.unitaryGroup (Bool × Bool) ℂ,
      Matrix.kronecker (1 : Matrix (I × I) (I × I) ℂ) (V : Matrix (Bool × Bool) (Bool × Bool) ℂ) *
        Matrix.kronecker (Matrix.kronecker H (1 : Matrix I I ℂ) + Matrix.kronecker (1 : Matrix I I ℂ) H)
          (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) =
      Matrix.kronecker (Matrix.kronecker H (1 : Matrix I I ℂ) + Matrix.kronecker (1 : Matrix I I ℂ) H)
        (1 : Matrix (Bool × Bool) (Bool × Bool) ℂ) * Matrix.kronecker (1 : Matrix (I × I) (I × I) ℂ) (V : Matrix (Bool × Bool) (Bool × Bool) ℂ)) ∧
    (∀ sigma : Matrix (Bool × Bool) (Bool × Bool) ℂ, IsDensityMatrix sigma → densityConjugation 1 sigma = sigma) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 11, §V B: required elementary operations and free-unitary symmetry

Read-back

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

Let $I$ be a finite index type with decidable equality, possibly empty, let $G$ be a group, let $R:G\to U(\mathbb C^I)$ be a group homomorphism, and let $H$ be a Hermitian complex matrix indexed by $I$ . Write $D$ for the operator on two copies of $\mathbb C^I$ and two Boolean registers that swaps the two $I$ -registers when both Boolean registers are true, and otherwise acts as the identity. With identities on the indicated registers, the declaration asserts all of the following:

\begin{aligned} D\bigl((R(g)\otimes R(g))\otimes 1\bigr) &=\bigl((R(g)\otimes R(g))\otimes 1\bigr)D &&\text{for every }g\in G,\\ D\bigl((H\otimes 1+1\otimes H)\otimes 1\bigr) &=\bigl((H\otimes 1+1\otimes H)\otimes 1\bigr)D,\\ (1\otimes V)\bigl((R(g)\otimes R(g))\otimes 1\bigr) &=\bigl((R(g)\otimes R(g))\otimes 1\bigr)(1\otimes V) &&\text{for every }V\in U(\mathbb C^{\mathrm{Bool}\times\mathrm{Bool}}),\ g\in G,\\ (1\otimes V)\bigl((H\otimes 1+1\otimes H)\otimes 1\bigr) &=\bigl((H\otimes 1+1\otimes H)\otimes 1\bigr)(1\otimes V) &&\text{for every such }V. \end{aligned}

It also asserts that every positive semidefinite complex matrix $\sigma$ on the two Boolean registers with $\operatorname{tr}\sigma=1$ satisfies $1\sigma1^\dagger=\sigma$ .

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