HH18 Parameterized: code Distance semantic Distance

Proved

QEC.Distillation.HH18Parameterized.codeDistance_semanticDistance

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

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

The named distance is attained by the actual source-valid parameterized HH18 CSS stabilizer, rather than carried as detached protocol metadata.

Source: https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/LowOverheadProtocol/Parameterized/Types.lean#L69-L72

Preamble

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

Formal statement

theorem QEC.Distillation.HH18Parameterized.codeDistance_semanticDistance {w r m : Nat} (h : Admissible w r m) :
    StabilizerCode.SemanticStabilizerDistance
      (HH18PuncturedReedMuller.sourceValidStabilizer h) (codeDistance r w) := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Distillation/LowOverheadProtocol/Parameterized/Types.lean#L69-L72

View graph