No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
125def repetitionCode3 : ClassicalCode := {
proof body
Definition body.
126 n := 3,
127 k := 1,
128 d := 3,
129 k_le_n := by norm_num,
130 d_pos := by norm_num
131}
132
133/-! ## CSS Codes -/
134
135/-- CSS (Calderbank-Shor-Steane) codes are built from two classical codes.
136
137 C₁ ⊇ C₂ (C₂ is a subcode of C₁)
138
139 - C₁ corrects bit-flip errors
140 - C₂⊥ corrects phase-flip errors -/
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
ClassicalCode
in IndisputableMonolith.Information.QuantumErrorCorrection
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
two
in IndisputableMonolith.QFT.SpinStatistics
decl_use