Prove2Me

BH12 Protocol: logical ABasis Projector idempotent

Proved
QEC.Distillation.Triorthogonal.BH12Protocol.logicalABasisProjector_idempotent

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

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

The BH12 Protocol construction uses the logical ABasis Projector idempotent 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#L2684-L2692

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.logicalABasisProjector_idempotent {q : Nat} (a : OddRow q)
    (outcome : StabilizerOutcome) :
    logicalABasisProjector a outcome * logicalABasisProjector a outcome =
      logicalABasisProjector a outcome := by sorry
Source
https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/Triorthogonal/Protocol.lean#L2684-L2692

View graph