BDL26 Random Perturbation: counted Scan map pair

Proved

QEC.Coding.BDL26RandomPerturbation.countedScan_map_pair

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

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

The BDL26 Random Perturbation construction uses the counted Scan map pair 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/Coding/FiniteAlternatingConstruction/RandomPerturbation/CountedCostMeasurability.lean#L508-L516

Preamble

import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_JointExecution
import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_ActualExecutionCost
import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_CountedCostMeasurability
set_option autoImplicit false
noncomputable section
open QEC QEC.Coding QEC.Coding.BDL26RandomPerturbation
open BDL26FiniteTannerSquare
open QEC.Coding.ProbabilisticConstruction.SphericalCap
open QEC.Coding.ProbabilisticConstruction.Resampling
open MeasureTheory
open scoped ENNReal
attribute [local instance] QEC.Coding.BDL26RandomPerturbation.countedLabelListMeasurable
attribute [local instance] QEC.Coding.BDL26RandomPerturbation.countedLabelListSingleton

Formal statement

theorem QEC.Coding.BDL26RandomPerturbation.countedScan_map_pair {A B W : Type*} (encode : A → B)
    (q : A → W → Bool × ℕ) (q' : B → W → Bool × ℕ)
    (hq : ∀ a w, q' (encode a) w = q a w) (L : List A) (w : W) :
    scanQuery q' (L.map encode) w = ((scanQuery q L w).1.map encode, (scanQuery q L w).2) := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Coding/FiniteAlternatingConstruction/RandomPerturbation/CountedCostMeasurability.lean#L508-L516

View graph