BH12 Protocol: logical Error Density zero eq bh12 Ideal Output

Proved

QEC.Distillation.Triorthogonal.BH12Protocol.logicalErrorDensity_zero_eq_bh12IdealOutput

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

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

The BH12 Protocol construction uses the logical Error Density zero eq bh12 Ideal Output property established by this source lemma. The formal statement records the complete hypotheses and conclusion.

Source: https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/Triorthogonal/Protocol.lean#L2999-L3004

Preamble

import Definitions.Def_QEC_Distillation_Triorthogonal_EvenFamily
import Definitions.Def_QEC_Distillation_Triorthogonal_NoisyInjection
import Definitions.Def_QEC_Coding_Stabilizer_JointMeasurement
import Definitions.Def_QEC_Semantics_Core_Subsystem
import Definitions.Def_QEC_Semantics_Entropy_Purification
import Definitions.Def_QEC_Distillation_Triorthogonal_Protocol
set_option autoImplicit false
noncomputable section
open QEC
open QEC.Distillation
open QEC.Distillation.Triorthogonal
open QEC.Distillation.Triorthogonal.BH12Protocol
open Semantics
open Coding
open Coding.PauliSymplectic
open BH12EvenFamily
open BH12NoisyInjection
open scoped BigOperators
attribute [local instance 100] Fintype.ofFinite
universe u

Formal statement

theorem QEC.Distillation.Triorthogonal.BH12Protocol.logicalErrorDensity_zero_eq_bh12IdealOutput (q : Nat) :
    logicalErrorDensity (0 : Word (ZMod 2) (OddRow q)) =
      bh12IdealOutput q := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/Triorthogonal/Protocol.lean#L2999-L3004

View graph