`eccCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.ErrorCorrectionCodesFromJCost
domain: Information
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.ErrorCorrectionCodesFromJCost on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

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