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)
69structure ErrorCode where
70 n : ℕ -- codeword length
71 k : ℕ -- message length
72 d : ℕ -- minimum distance
73
74/-- The Hamming bound (sphere-packing bound):
75
76 For t-error-correcting code:
77 2^k × Σᵢ₌₀ᵗ C(n,i) ≤ 2ⁿ
78
79 Codes meeting this bound are "perfect" (e.g., Hamming codes).
80
81 Formalized as: for our 8-tick code with d=8, t=3,
82 the volume of radius-3 balls around 2^1 codewords fits inside {0,1}^8. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
eightTickCode
in IndisputableMonolith.Information.ErrorCorrectionBounds
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
radius
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
volume
in IndisputableMonolith.Papers.GCIC.BrainHolography
decl_use