def
definition
dft8ModeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
38 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
39
40/-- DFT-8 harmonic scheduling: 8 = 2^D = 2^3 modes. -/
41def dft8ModeCount : ℕ := 8
42theorem dft8_eq_8 : dft8ModeCount = 8 := rfl
43
44structure QECCert where
45 five_codes : Fintype.card QECCodeType = 5
46 threshold_zero : Jcost 1 = 0
47 error_positive : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
48 dft8_count : dft8ModeCount = 8
49
50def qecCert : QECCert where
51 five_codes := qecCodeCount
52 threshold_zero := below_threshold_correct
53 error_positive := logical_error_positive
54 dft8_count := dft8_eq_8
55
56end IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost