Detected-jump complement has commuting basis outputs

Proved

QAlgorithms.Papers.Independent.Intakethird100.P10.detectedJump_classical_environment

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

prove2quantum

For $0\le\gamma\le1$ , use the photon-detected-jump complementary map printed in Appendix B, extended linearly as $\rho\mapsto\operatorname{diag}(\operatorname{Tr}\rho-\gamma\rho_{11},\gamma\rho_{11})$ . Its computational-basis outputs satisfy

W^*(|0\rangle\langle0|)=|0\rangle\langle0|,\qquad W^*(|1\rangle\langle1|)=(1-\gamma)|0\rangle\langle0|+\gamma|1\rangle\langle1|,

and therefore commute. This verifies the stated basis criterion using the cited complement, with no full-Fock or capacity assertion.

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: computational-basis outputs of the printed detected-jump
complement commute. The map does not describe a full-Fock photonic protocol. -/
theorem detectedJump_classical_environment (gamma : ℝ) (hlo : 0 ≤ gamma) (hhi : gamma ≤ 1) :
    detectedJumpComplement gamma (basisDensity false) = basisDensity false ∧
    detectedJumpComplement gamma (basisDensity true) =
      ((1 - gamma : ℝ) : ℂ) • basisDensity false + (gamma : ℂ) • basisDensity true ∧
    Commute (detectedJumpComplement gamma (basisDensity false))
      (detectedJumpComplement gamma (basisDensity 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 photon-detected-jump classical-environment example

Read-back

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

For every real $\gamma$ satisfying $0\le\gamma\le1$ , let $E_0=\operatorname{diag}(1,0)$ , $E_1=\operatorname{diag}(0,1)$ , and define $\mathcal J_\gamma(\rho)=\operatorname{diag}(\operatorname{tr}\rho-\gamma\rho_{11},\,\gamma\rho_{11})$ . Then

\mathcal J_\gamma(E_0)=E_0,\qquad \mathcal J_\gamma(E_1)=(1-\gamma)E_0+\gamma E_1,

and the two output matrices commute, meaning their products in the two orders are equal. Both endpoints $\gamma=0$ and $\gamma=1$ are included.

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