BDL26 Random Perturbation: event Universe Budget polynomial

Proved

QEC.Coding.BDL26RandomPerturbation.eventUniverseBudget_polynomial

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

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

A fixed exponent and coefficient, independent of presentation size and depth.

Source: https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Coding/FiniteAlternatingConstruction/RandomPerturbation/EventPreprocessingCost.lean#L61-L69

Preamble

import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_EventUniverse
import Definitions.Def_QEC_Coding_FiniteAlternatingConstruction_RandomPerturbation_EventPreprocessingCost
set_option autoImplicit false
open QEC QEC.Coding QEC.Coding.BDL26RandomPerturbation
open BDL26FiniteTannerSquare
open QEC.Coding.ProbabilisticConstruction.SphericalCap

Formal statement

theorem QEC.Coding.BDL26RandomPerturbation.eventUniverseBudget_polynomial (n : ℕ) : eventUniverseBudget n ≤ 1000000*(n+1)^10 := by sorry

Source

https://github.com/QudeLeap/Lean-QECert/blob/4a64933303628b4f94c4567347e86636853f64a4/QEC/Coding/FiniteAlternatingConstruction/RandomPerturbation/EventPreprocessingCost.lean#L61-L69

View graph