HH18 Parameterized: noisy Input to Operator

Proved

QEC.Distillation.HH18Parameterized.noisyInput_toOperator

by marwahaha · Nov 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-qecert-4a64933quantum-computingquantum-error-correction

The actual parameterized noisy input has the literal normalized product mixture over physical Pauli-Z error branches.

Source: https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/LowOverheadProtocol/Parameterized/Preparation.lean#L93-L101

Preamble

import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_Types
import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_Preparation
set_option autoImplicit false
noncomputable section
open QEC
open QEC.Distillation
open QEC.Distillation.HH18Parameterized
open Coding Semantics
open Semantics.Qubit
open scoped BigOperators
attribute [local instance 100] Fintype.ofFinite

Formal statement

theorem QEC.Distillation.HH18Parameterized.noisyInput_toOperator (epsilon : HH18NoisyInput.DiagonalErrorRate)
    (m w : Nat) :
    (noisyInput epsilon m w).toOperator =
      ∑ error : PhysicalErrorWord m w,
        (HH18NoisyInput.errorWordWeight epsilon error : Complex) •
          (HH18NoisyInput.errorWordDensity error).toOperator := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/LowOverheadProtocol/Parameterized/Preparation.lean#L93-L101

View graph