theorem proved term proof

`hamming_bound_8tick`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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

proof body

Term-mode proof.

  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. -/

depends on (3)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use