BDL26 Random Perturbation: refresh State Row Query cost le

Proved

QEC.Coding.BDL26RandomPerturbation.refreshStateRowQuery_cost_le

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

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

The BDL26 Random Perturbation construction uses the refresh State Row Query cost le 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/StateRows.lean#L95-L101

Preamble

import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_ExecutionPrimitiveQueries
import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_StateRows
set_option autoImplicit false
open QEC QEC.Coding QEC.Coding.BDL26RandomPerturbation
open BDL26FiniteTannerSquare
open QEC.Coding.ProbabilisticConstruction.SphericalCap
open QEC.Coding.ProbabilisticConstruction.Resampling
variable {P : TannerSquarePresentation}

Formal statement

theorem QEC.Coding.BDL26RandomPerturbation.refreshStateRowQuery_cost_le (support : List (Vertex P))
    (T : Table (X := fun _ : Vertex P => Space)) (row : Vertex P × ℕ × Space)
    (hlen : support.length ≤ 12) : (refreshStateRowQuery support T row).2 ≤ 30 := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Coding/FiniteAlternatingConstruction/RandomPerturbation/StateRows.lean#L95-L101

View graph