Prove2Me

The displayed cloning-environment states commute

Proved
QAlgorithms.Papers.Independent.Intakethird100.P10.cloning_classical_environment

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

prove2quantum

Let m≥1m\ge1 be the number of clones, put Δm=m(m+1)/2\Delta_m=m(m+1)/2, and choose any orthonormal basis {∣ei⟩}i=0m−1\{|e_i\rangle\}_{i=0}^{m-1} of the environment. Construct the two displayed states

ρ0E=∑i=0m−1i+1Δm∣ei⟩⟨ei∣,ρ1E=∑i=0m−1i+1Δm∣em−1−i⟩⟨em−1−i∣.\rho_0^E=\sum_{i=0}^{m-1}{i+1\over\Delta_m}|e_i\rangle\langle e_i|,\qquad \rho_1^E=\sum_{i=0}^{m-1}{i+1\over\Delta_m}|e_{m-1-i}\rangle\langle e_{m-1-i}|.

Both are positive trace-one matrices and they commute. The source's cited covariance identifies these as the complementary outputs for any orthonormal qubit input basis, allowing the common environment basis to depend on that input basis. The formal statement verifies the explicit output formulas in any common environment basis; it does not reconstruct the full cloning channel from two outputs.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10
Formal statement
noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF p.11, Appendix B: the explicitly displayed outputs are states and commute
in every common environmental orthonormal basis. The cited covariance permits this
basis to depend on the chosen qubit input basis. m=0 is excluded; m=1 is allowed. -/
theorem cloning_classical_environment (m : ℕ) (hm : 0 < m)
    (basis : Matrix.unitaryGroup (Fin m) ℂ) :
    IsBinaryCQ (cloningEnvironment m basis) ∧
    Commute (cloningEnvironment m basis false) (cloningEnvironment m basis true) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end
Source
Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 11, Appendix B, unnumbered cloning-channel classical-environment example
Read-back

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

For every positive natural number mm and every unitary complex m×mm\times m matrix UU, write uiu_i for its columns and define

ρfalse=∑i=0m−1i+1m(m+1)/2 uiui†,ρtrue=∑i=0m−1i+1m(m+1)/2 um−1−ium−1−i†.\rho_{\mathrm{false}}=\sum_{i=0}^{m-1}\frac{i+1}{m(m+1)/2}\,u_i u_i^\dagger, \qquad \rho_{\mathrm{true}}=\sum_{i=0}^{m-1}\frac{i+1}{m(m+1)/2}\,u_{m-1-i}u_{m-1-i}^\dagger.

Both matrices are positive semidefinite and have trace one, and they commute: ρfalseρtrue=ρtrueρfalse\rho_{\mathrm{false}}\rho_{\mathrm{true}}=\rho_{\mathrm{true}}\rho_{\mathrm{false}}. This includes m=1m=1.

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