HH18 Protocol: raw Endpoints reconstruct

Proved

QEC.Distillation.HH18Protocol.rawEndpoints_reconstruct

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

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

The HH18 Protocol construction uses the raw Endpoints reconstruct 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/LowOverheadProtocol/Core/PhysicalEndpoint.lean#L61-L73

Preamble

import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Core_ResourceConsumer
import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Core_PhysicalEndpoint
set_option autoImplicit false
noncomputable section
open QEC
open QEC.Distillation
open QEC.Distillation.HH18Protocol
open Coding Semantics
open Coding.PauliSymplectic
open Semantics.Qubit
open scoped BigOperators
universe u
attribute [local instance 100] Fintype.ofFinite
attribute [local instance] QEC.Distillation.HH18Protocol.instEndpointClassicalDecidable
attribute [local instance] QEC.Distillation.HH18Protocol.instEndpointClassicalDecidable

Formal statement

theorem QEC.Distillation.HH18Protocol.rawEndpoints_reconstruct
    (inputs : ResourceInput resourceCount QubitSpace) :
    rawEndpoint inputs .accepted + rawEndpoint inputs .rejected =
      (physicalOperation.mapDensity (prepareMeasuredResources inputs)).toOperator := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/LowOverheadProtocol/Core/PhysicalEndpoint.lean#L61-L73

View graph