ECCCert

formal source

  47    nlinarith
  48  exact one_div_lt_one_div_of_lt hpos_k h_growth
  49
  50structure ECCCert where
  51  five_families : Fintype.card ECCFamily = 5
  52  threshold_always_pos : ∀ k, 0 < thresholdGap k
  53  threshold_strictly_decreasing : ∀ k, thresholdGap (k + 1) < thresholdGap k
  54
  55noncomputable def eccCert : ECCCert where
  56  five_families := eccFamily_count
  57  threshold_always_pos := thresholdGap_pos
  58  threshold_strictly_decreasing := thresholdGap_strictDecr
  59
  60end IndisputableMonolith.Information.ErrorCorrectionCodesFromJCost