  66
  67    Can correct up to ⌊(d-1)/2⌋ errors.
  68    Rate R = k/n. -/
  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. -/
  83theorem hamming_bound_8tick :
  84    2 ^ 1 * (Nat.choose 8 0 + Nat.choose 8 1 +
  85      Nat.choose 8 2 + Nat.choose 8 3)
  86    ≤ 2 ^ 8 := by
  87  native_decide
  88
  89/-- The Singleton bound: d ≤ n - k + 1.
  90
  91    Codes meeting this bound are MDS (Maximum Distance Separable).
  92
  93    Formalized for the 8-tick code: d=8 ≤ 8-1+1 = 8. -/
  94theorem singleton_bound_8tick :
  95    (8 : ℕ) ≤ 8 - 1 + 1 := by norm_num
  96
  97/-! ## 8-Tick Error Correction -/
  98
  99/-- In RS, the 8-tick structure provides natural error correction:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.